Perron's method: barriers and boundary values

Let Ω be a bounded open subset of a finite-dimensional real inner product space E, and let g be bounded on frontier Ω. Perron's theorem (TauCeti.harmonicOnNhd_perronSolution) makes the Perron solution u = TauCeti.perronSolution Ω g harmonic in Ω, but says nothing about its boundary values. This file shows that u takes the value g ξ continuously at every point ξ where g is continuous along frontier Ω and a barrier exists: a superharmonic function w, continuous on closure Ω, vanishing at ξ and positive on the rest of closure Ω. A boundary point admitting a barrier is called regular.

If every boundary point is regular, the Perron solution of continuous boundary data is therefore continuous on closure Ω and equal to g on frontier Ω, and so solves the Dirichlet problem Δu = 0 in Ω, u = g on frontier Ω.

Exterior sphere condition

If a closed ball closedBall y R meets closure Ω only at ξ, the function G(ξ - y) - G(x - y), built from the Newtonian kernel G = TauCeti.newtonianKernel n with pole at y, is a barrier at ξ in ℝⁿ for n ≠ 2. In a two-dimensional space the logarithmic function log ‖x - y‖ - log ‖ξ - y‖ plays the same role. In every dimension n, the Dirichlet problem in ℝⁿ is therefore solvable on every bounded open set satisfying this exterior sphere condition at each boundary point.

Main declarations

• TauCeti.IsBarrier: a barrier at a point relative to Ω.
• TauCeti.tendsto_perronSolution_of_isBarrier: at a point with a barrier where the boundary data is continuous, the Perron solution tends to the boundary value.
• TauCeti.perronSolution_eq_of_isBarrier: there the Perron solution equals the boundary value.
• TauCeti.continuousOn_perronSolution: if every boundary point admits a barrier, the Perron solution of continuous boundary data is continuous on closure Ω.
• TauCeti.exists_harmonicOnNhd_continuousOn_closure_eqOn_frontier: the Dirichlet problem is solvable when every boundary point admits a barrier.
• TauCeti.isBarrier_newtonianKernel_sub: the exterior sphere barrier in ℝⁿ, n ≠ 2.
• TauCeti.isBarrier_log_norm_sub: the logarithmic exterior sphere barrier in two dimensions.
• TauCeti.exists_harmonicOnNhd_continuousOn_closure_eqOn_frontier_of_exterior_sphere: the Dirichlet problem is solvable on bounded open subsets of ℝⁿ satisfying the exterior sphere condition.

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, Lemma 2.13 and Theorem 2.14, and the exterior sphere barrier following it.

structure TauCeti.IsBarrier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (Ω : Set E) (ξ : E) (w : E → ℝ) : Prop

A barrier at the point ξ relative to Ω: a function w that is superharmonic on Ω (-w is subharmonic), continuous on closure Ω, zero at ξ and positive at every other point of closure Ω. A point of frontier Ω admitting a barrier is a regular boundary point.

• subharmonicOn_neg : SubharmonicOn (-w) Ω

  A barrier is superharmonic on Ω.

• continuousOn : ContinuousOn w (closure Ω)

  A barrier is continuous on closure Ω.

• apply_self : w ξ = 0

  A barrier vanishes at its point.

• pos (x : E) : x ∈ closure Ω → x ≠ ξ → 0 < w x

  A barrier is positive on closure Ω away from its point.

theorem TauCeti.tendsto_perronSolution_of_isBarrier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : Set E} {g w : E → ℝ} {ξ : E} [MeasurableSpace E] [BorelSpace E] [Nontrivial E] (hΩ : IsOpen Ω) (hb : Bornology.IsBounded Ω) (hg : Bornology.IsBounded (g '' frontier Ω)) (hw : IsBarrier Ω ξ w) (hgξ : ContinuousWithinAt g (frontier Ω) ξ) : Filter.Tendsto (perronSolution Ω g) (nhdsWithin ξ (closure Ω)) (nhds (g ξ))

Boundary values of the Perron solution. Let Ω be a bounded open set and g bounded on frontier Ω. At a point ξ admitting a barrier, where g is continuous along frontier Ω, the Perron solution tends to g ξ as its argument tends to ξ within closure Ω.

theorem TauCeti.perronSolution_eq_of_isBarrier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : Set E} {g w : E → ℝ} {ξ : E} [MeasurableSpace E] [BorelSpace E] [Nontrivial E] (hΩ : IsOpen Ω) (hb : Bornology.IsBounded Ω) (hg : Bornology.IsBounded (g '' frontier Ω)) (hw : IsBarrier Ω ξ w) (hgξ : ContinuousWithinAt g (frontier Ω) ξ) (hξ : ξ ∈ closure Ω) : perronSolution Ω g ξ = g ξ

At a point ξ ∈ closure Ω admitting a barrier, where the boundary data g (bounded on frontier Ω) is continuous along frontier Ω, the Perron solution equals g ξ.

theorem TauCeti.continuousOn_perronSolution {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : Set E} {g : E → ℝ} [MeasurableSpace E] [BorelSpace E] [Nontrivial E] (hΩ : IsOpen Ω) (hb : Bornology.IsBounded Ω) (hreg : ∀ ξ ∈ frontier Ω, ∃ (w : E → ℝ), IsBarrier Ω ξ w) (hg : ContinuousOn g (frontier Ω)) : ContinuousOn (perronSolution Ω g) (closure Ω)

If every boundary point of the bounded open set Ω admits a barrier, the Perron solution of boundary data g continuous on frontier Ω is continuous on closure Ω.

theorem TauCeti.exists_harmonicOnNhd_continuousOn_closure_eqOn_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : Set E} {g : E → ℝ} [MeasurableSpace E] [BorelSpace E] (hΩ : IsOpen Ω) (hb : Bornology.IsBounded Ω) (hreg : ∀ ξ ∈ frontier Ω, ∃ (w : E → ℝ), IsBarrier Ω ξ w) (hg : ContinuousOn g (frontier Ω)) : ∃ (u : E → ℝ), InnerProductSpace.HarmonicOnNhd u Ω ∧ ContinuousOn u (closure Ω) ∧ Set.EqOn u g (frontier Ω)

Perron's solution of the Dirichlet problem. Let Ω be a bounded open set every boundary point of which admits a barrier. For boundary data g continuous on frontier Ω, there is a function harmonic in Ω, continuous on closure Ω and equal to g on frontier Ω. In a nontrivial space it is the Perron solution TauCeti.perronSolution Ω g.

The exterior sphere condition

theorem TauCeti.isBarrier_newtonianKernel_sub {n : ℕ} (hn : n ≠ 2) {Ω : Set (EuclideanSpace ℝ (Fin n))} {ξ y : EuclideanSpace ℝ (Fin n)} (hξy : ξ ≠ y) (h : ∀ x ∈ closure Ω, x ≠ ξ → dist ξ y < dist x y) : IsBarrier Ω ξ fun (x : EuclideanSpace ℝ (Fin n)) => newtonianKernel n (ξ - y) - newtonianKernel n (x - y)

The exterior sphere barrier. In ℝⁿ with n ≠ 2, suppose a closed ball centred at y ≠ ξ meets closure Ω only at ξ, that is, every other point of closure Ω is farther from y than ξ. Then x ↦ G(ξ - y) - G(x - y), with G = TauCeti.newtonianKernel n, is a barrier at ξ relative to Ω.

theorem TauCeti.isBarrier_log_norm_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : Set E} {ξ : E} [MeasurableSpace E] [BorelSpace E] (hE : Module.finrank ℝ E = 2) {y : E} (hξy : ξ ≠ y) (h : ∀ x ∈ closure Ω, x ≠ ξ → dist ξ y < dist x y) : IsBarrier Ω ξ fun (x : E) => Real.log ‖x - y‖ - Real.log ‖ξ - y‖

The planar exterior sphere barrier. In a two-dimensional space, suppose a closed ball centred at y ≠ ξ meets closure Ω only at ξ, that is, every other point of closure Ω is farther from y than ξ. Then x ↦ log ‖x - y‖ - log ‖ξ - y‖ is a barrier at ξ relative to Ω.

theorem TauCeti.exists_harmonicOnNhd_continuousOn_closure_eqOn_frontier_of_exterior_sphere {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} (hΩ : IsOpen Ω) (hb : Bornology.IsBounded Ω) (hext : ∀ ξ ∈ frontier Ω, ∃ (y : EuclideanSpace ℝ (Fin n)), y ≠ ξ ∧ ∀ x ∈ closure Ω, x ≠ ξ → dist ξ y < dist x y) {g : EuclideanSpace ℝ (Fin n) → ℝ} (hg : ContinuousOn g (frontier Ω)) : ∃ (u : EuclideanSpace ℝ (Fin n) → ℝ), InnerProductSpace.HarmonicOnNhd u Ω ∧ ContinuousOn u (closure Ω) ∧ Set.EqOn u g (frontier Ω)

The Dirichlet problem under the exterior sphere condition. Let Ω be a bounded open subset of ℝⁿ such that at every boundary point ξ some closed ball centred at a point y ≠ ξ meets closure Ω only at ξ. For boundary data g continuous on frontier Ω, there is a function harmonic in Ω, continuous on closure Ω and equal to g on frontier Ω.