Potential theory

Harmonic and subharmonic functions in the plane and in R^n, harmonic conjugates, the Newton and logarithmic potentials and fundamental solutions of the Laplacian.

• Equilibrium points of logarithmic potentials
• Fundamental solutions of the Laplacian
• Harmonic extension to a half-space
• Harmonic functions vanishing on the edges of a cube
• Subharmonic functions

TheoremA harmonic function vanishing on a set of positive measure is zero#●ready to prove

Let \(\Omega \subseteq \mathbb{C}\) be a nonempty connected open set and let \(h : \mathbb{C} \to \mathbb{R}\) be harmonic on \(\Omega\). If \(h\) vanishes on some subset \(s \subseteq \Omega\) of positive (outer) Lebesgue measure, then \(h(z) = 0\) for all \(z \in \Omega\).

public theorem_wanted eq_zero_of_harmonicOnNhd_of_vanishing_on_pos_volume
  (Ω : Set ℂ) (h : ℂ → ℝ) (hΩ_open : IsOpen Ω) (hΩ_connected : IsConnected Ω)
  (hh_harmonic : InnerProductSpace.HarmonicOnNhd h Ω)
  (h_zero_on_pos_meas :
    ∃ s : Set ℂ, s ⊆ Ω ∧ 0 < MeasureTheory.volume s ∧ ∀ z ∈ s, h z = 0) :
  ∀ z ∈ Ω, h z = 0

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functions of a complex variable; Miscellaneous topics of analysis in the complex plane), problem ma_proofbench_l2_88.

TheoremHarmonic functions on simply connected domains are real parts#●ready to prove

Let \(\Omega \subseteq \mathbb{C}\) be a simply connected open set and let \(u : \mathbb{C} \to \mathbb{R}\) be harmonic on \(\Omega\). Then there is a function \(f\) holomorphic on \(\Omega\) with \(\operatorname{Re} f(z) = u(z)\) for all \(z \in \Omega\), and \(f\) is unique up to an additive constant: if \(f\) and \(g\) are holomorphic on \(\Omega\) with \(\operatorname{Re} f(z) = u(z)\) and \(\operatorname{Re} g(z) = u(z)\) for all \(z \in \Omega\), then there is \(c \in \mathbb{C}\) with \(f(z) = g(z) + c\) for all \(z \in \Omega\).

public theorem_wanted exists_differentiableOn_re_eq_of_harmonicOnNhd_of_isSimplyConnected
  (Ω : Set ℂ)
  (u : ℂ → ℝ)
  (hΩ_open : IsOpen Ω)
  (hΩ : IsSimplyConnected Ω)
  (hu : InnerProductSpace.HarmonicOnNhd u Ω) :
  (∃ f : ℂ → ℂ, DifferentiableOn ℂ f Ω ∧ ∀ z : ℂ, z ∈ Ω → Complex.re (f z) = u z) ∧
    (∀ f g : ℂ → ℂ,
      DifferentiableOn ℂ f Ω →
      DifferentiableOn ℂ g Ω →
      (∀ z : ℂ, z ∈ Ω → Complex.re (f z) = u z) →
      (∀ z : ℂ, z ∈ Ω → Complex.re (g z) = u z) →
      ∃ c : ℂ, ∀ z : ℂ, z ∈ Ω → f z = g z + c)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functions of a complex variable; General properties of functions of one complex variable), problem ma_proofbench_l2_69.

TheoremNonnegative harmonic functions on the upper half-plane integrable along the imaginary axis vanish#●ready to prove

Nonnegative harmonic functions on the upper half-plane integrable along the imaginary axis vanish. Let \(\mathbb{C}_{+}=\{z\in\mathbb{C}:\Im z>0\}\) be the upper half-plane. Suppose \(f:\mathbb{C}_{+}\to\mathbb{R}\) is harmonic and non-negative, and satisfies [ \int_{0}^{\infty}\lvert f(iy)\rvert\,dy\lt \infty. ] Then \(f(z)=0\) for every \(z\in\mathbb{C}_{+}\).

public theorem_wanted eq_zero_of_harmonicOnNhd_upperHalfPlane_of_nonneg_of_integrableOn_imagAxis
  (f : ℂ → ℝ)
  (hharm : InnerProductSpace.HarmonicOnNhd f UpperHalfPlane.upperHalfPlaneSet)
  (hnonneg : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, 0 ≤ f z)
  (hint :
    MeasureTheory.IntegrableOn
      (fun y : ℝ => |f (Complex.I * (y : ℂ))|)
      (Set.Ioi (0 : ℝ))) :
  ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, f z = 0

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functions of a complex variable; General properties of functions of one complex variable), problem ma_proofbench_l2_20.

3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.