Harnack's convergence theorem

Let E be a finite-dimensional real inner product space. This file proves Harnack's convergence theorem: a monotone family of harmonic functions E → ℝ on a preconnected open set U that is bounded above at one point of U converges locally uniformly on U, and its limit is harmonic. For F m ≤ F n the difference F n - F m is harmonic and nonnegative, so Harnack's inequality (IsCompact.harnack_inequality) bounds it on a compact set K ⊆ U by a multiple of its value at the base point, which tends to zero. Harmonicity of the limit then follows from TauCeti.harmonicOnNhd_of_tendstoLocallyUniformlyOn: a locally uniform limit of harmonic functions is harmonic.

This is the compactness input of Perron's method for the Dirichlet problem, which takes the limit of increasing sequences of harmonic functions on a ball.

Main declarations

• TauCeti.tendstoLocallyUniformlyOn_iSup_of_monotone: Harnack's convergence theorem, the locally uniform convergence of a monotone family of harmonic functions.
• TauCeti.harmonicOnNhd_iSup_of_monotone: the limit of such a family is harmonic.

References

• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 2.9.
• L. C. Evans, Partial Differential Equations, Section 2.2.3.

theorem TauCeti.tendstoLocallyUniformlyOn_iSup_of_monotone {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} [SemilatticeSup ι] [Nonempty ι] {F : ι → E → ℝ} {U : Set E} (hU : IsOpen U) (hUc : IsPreconnected U) (hF : ∀ (i : ι), InnerProductSpace.HarmonicOnNhd (F i) U) (hmono : ∀ x ∈ U, Monotone fun (i : ι) => F i x) {x₀ : E} (hx₀ : x₀ ∈ U) (hbdd : BddAbove (Set.range fun (i : ι) => F i x₀)) : TendstoLocallyUniformlyOn F (fun (x : E) => ⨆ (i : ι), F i x) Filter.atTop U

Harnack's convergence theorem. Let F be a family of functions harmonic on a preconnected open set U, monotone at each point of U and bounded above at some point x₀ ∈ U. Then F converges locally uniformly on U to its pointwise supremum.

theorem TauCeti.harmonicOnNhd_iSup_of_monotone {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} [SemilatticeSup ι] [Nonempty ι] {F : ι → E → ℝ} {U : Set E} (hU : IsOpen U) (hUc : IsPreconnected U) (hF : ∀ (i : ι), InnerProductSpace.HarmonicOnNhd (F i) U) (hmono : ∀ x ∈ U, Monotone fun (i : ι) => F i x) {x₀ : E} (hx₀ : x₀ ∈ U) (hbdd : BddAbove (Set.range fun (i : ι) => F i x₀)) : InnerProductSpace.HarmonicOnNhd (fun (x : E) => ⨆ (i : ι), F i x) U

The limit in Harnack's convergence theorem is harmonic. Let F be a family of functions harmonic on a preconnected open set U, monotone at each point of U and bounded above at some point x₀ ∈ U. Then its pointwise supremum is harmonic on U.