Perron's method: the Perron solution is harmonic

Let Ω be a bounded open subset of a finite-dimensional real inner product space E, and let g : E → ℝ be boundary data, bounded above on frontier Ω. The Perron family of g consists of the functions v, continuous on closure Ω and subharmonic on Ω, with v ≤ g on frontier Ω. Its pointwise supremum is the Perron solution

u x = sup {v x | v in the Perron family}.

This file proves Perron's theorem: if the Perron family is nonempty (for instance, if g is bounded on frontier Ω), then u is harmonic in Ω, for any bounded open Ω, with no regularity of frontier Ω and no continuity of g. Whether u attains the boundary values g is a separate question, decided at each boundary point by the existence of a barrier.

The argument

By the comparison principle every member of the Perron family is bounded by an upper bound M of g on frontier Ω. The family is closed under pointwise maxima, and under harmonic lifting in a ball B with closure B ⊆ Ω: replacing v inside B by the solution of the Dirichlet problem on B with boundary values v gives a member of the family that is harmonic in B and lies above v.

Fix a ball B centred at c. Choose members v n of the family with v n c → u c, replace them by their running maxima, and lift each in B. The lifts increase, so by Harnack's convergence theorem they converge in B to a harmonic function W ≤ u with W c = u c. If W z < u z at some z ∈ B, a member v of the family with W z < v z can be added to the running maxima; the resulting harmonic limit W' ≥ W agrees with W at the centre, so by the strong maximum principle W' = W on B, contradicting W' z ≥ v z > W z. Hence u = W is harmonic in B.

Main declarations

• TauCeti.perronFamily: the Perron family of subharmonic functions below the boundary data.
• TauCeti.perronFamily_nonempty: the Perron family is nonempty when the boundary data is bounded below.
• TauCeti.sup_mem_perronFamily: the Perron family is closed under pointwise maxima.
• TauCeti.perronSolution: the Perron solution, the pointwise supremum of the Perron family.
• TauCeti.le_perronSolution, TauCeti.perronSolution_le: the Perron solution lies above every member of the Perron family and below every upper bound of the boundary data.
• TauCeti.perronSolution_le_of_forall_le: the Perron solution at x is at most every common upper bound of the values at x of the members of a nonempty Perron family.
• TauCeti.harmonicOnNhd_perronSolution: Perron's theorem, the Perron solution of a nonempty Perron family is harmonic in Ω.

References

• O. Perron, Eine neue Behandlung der ersten Randwertaufgabe für Δu = 0, Math. Z. 18 (1923).
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Section 2.8, Theorem 2.12.

Harmonic lifting in a ball

def TauCeti.perronFamily {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (Ω : Set E) (g : E → ℝ) : Set (E → ℝ)

The Perron family of the boundary data g on Ω: the functions that are subharmonic on Ω, continuous on closure Ω, and at most g on frontier Ω.

Equations

• TauCeti.perronFamily Ω g = {v : E → ℝ | TauCeti.SubharmonicOn v Ω ∧ ContinuousOn v (closure Ω) ∧ ∀ x ∈ frontier Ω, v x ≤ g x}

@[simp]

theorem TauCeti.mem_perronFamily {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : Set E} {g v : E → ℝ} [MeasurableSpace E] [BorelSpace E] : v ∈ perronFamily Ω g ↔ SubharmonicOn v Ω ∧ ContinuousOn v (closure Ω) ∧ ∀ x ∈ frontier Ω, v x ≤ g x

theorem TauCeti.perronFamily_nonempty {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : Set E} {g : E → ℝ} [MeasurableSpace E] [BorelSpace E] (hg : BddBelow (g '' frontier Ω)) : (perronFamily Ω g).Nonempty

If the boundary data is bounded below on frontier Ω, the Perron family is nonempty: it contains the constant function at any lower bound of g on frontier Ω.

noncomputable def TauCeti.perronSolution {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (Ω : Set E) (g : E → ℝ) (x : E) : ℝ

The Perron solution of the Dirichlet problem on Ω with boundary data g: the pointwise supremum of the Perron family TauCeti.perronFamily Ω g. It is harmonic in Ω when Ω is bounded and open, g is bounded above on frontier Ω and the Perron family is nonempty (TauCeti.harmonicOnNhd_perronSolution); the family is nonempty when g is also bounded below on frontier Ω (TauCeti.perronFamily_nonempty).

If the family is empty, the supremum is the junk value sSup ∅ = 0; no result here is stated for that case.

Equations

• TauCeti.perronSolution Ω g x = sSup ((fun (v : E → ℝ) => v x) '' TauCeti.perronFamily Ω g)

theorem TauCeti.perronSolution_def {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : Set E} {g : E → ℝ} {x : E} [MeasurableSpace E] [BorelSpace E] : perronSolution Ω g x = sSup ((fun (v : E → ℝ) => v x) '' perronFamily Ω g)

theorem TauCeti.sup_mem_perronFamily {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : Set E} {g v w : E → ℝ} [MeasurableSpace E] [BorelSpace E] (hΩ : IsOpen Ω) (hv : v ∈ perronFamily Ω g) (hw : w ∈ perronFamily Ω g) : v ⊔ w ∈ perronFamily Ω g

The Perron family is closed under pointwise maxima.

theorem TauCeti.perronSolution_le_of_forall_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : Set E} {g : E → ℝ} {x : E} {M : ℝ} [MeasurableSpace E] [BorelSpace E] (hne : (perronFamily Ω g).Nonempty) (h : ∀ v ∈ perronFamily Ω g, v x ≤ M) : perronSolution Ω g x ≤ M

If the Perron family is nonempty, the Perron solution at x is at most any common upper bound of the values at x of the members of the family.

theorem TauCeti.le_perronSolution {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : Set E} {g v : E → ℝ} {x : E} [MeasurableSpace E] [BorelSpace E] [Nontrivial E] (hΩ : IsOpen Ω) (hb : Bornology.IsBounded Ω) (hg : BddAbove (g '' frontier Ω)) (hv : v ∈ perronFamily Ω g) (hx : x ∈ closure Ω) : v x ≤ perronSolution Ω g x

The Perron solution lies above every member of the Perron family on closure Ω.

theorem TauCeti.perronSolution_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : Set E} {g : E → ℝ} {x : E} {M : ℝ} [MeasurableSpace E] [BorelSpace E] [Nontrivial E] (hΩ : IsOpen Ω) (hb : Bornology.IsBounded Ω) (hne : (perronFamily Ω g).Nonempty) (hM : ∀ x ∈ frontier Ω, g x ≤ M) (hx : x ∈ closure Ω) : perronSolution Ω g x ≤ M

If the Perron family is nonempty, the Perron solution is bounded on closure Ω by every upper bound of the boundary data.

Perron's theorem

theorem TauCeti.harmonicOnNhd_perronSolution {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : Set E} {g : E → ℝ} [MeasurableSpace E] [BorelSpace E] (hΩ : IsOpen Ω) (hb : Bornology.IsBounded Ω) (hg : BddAbove (g '' frontier Ω)) (hne : (perronFamily Ω g).Nonempty) : InnerProductSpace.HarmonicOnNhd (perronSolution Ω g) Ω

Perron's theorem. Let Ω be a bounded open set, let g be bounded above on frontier Ω, and suppose the Perron family of g is nonempty. Then the Perron solution TauCeti.perronSolution Ω g is harmonic in Ω.

In Perron's setting of bounded boundary data the family is nonempty by TauCeti.perronFamily_nonempty.