The strong maximum principle for planar harmonic functions

This file globalizes the zero case of the planar Harnack inequality from a disk to a preconnected set containing a neighborhood of the distinguished point. The local disk result gives vanishing on a neighborhood, and Mathlib's AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq propagates that equality throughout the preconnected set.

Applying this zero-propagation result to differences gives the strong comparison principle and the strong maximum and minimum principles: two ordered harmonic functions that meet at an interior point agree everywhere, and a harmonic function with a local extremum there is constant on the preconnected set. For the latter, the comparison principle first gives constancy on a disk.

This is the planar harmonic case of Lane C, item 13 in the PDE roadmap. The local vanishing input is the zero case of Harnack's inequality; see Evans, Partial Differential Equations, Chapter 2, Section 2.2.

Main declarations

• TauCeti.eq_zero_on_of_harmonicOnNhd_of_nonneg_of_eq_zero: a nonnegative harmonic function on a preconnected set that vanishes at an interior point vanishes everywhere on the set.
• TauCeti.eqOn_of_harmonicOnNhd_of_le_of_eq: the strong comparison principle for planar harmonic functions.
• TauCeti.eqOn_const_of_harmonicOnNhd_of_isLocalMax: the local strong maximum principle.
• TauCeti.eqOn_const_of_harmonicOnNhd_of_isLocalMin: the local strong minimum principle.
• TauCeti.eqOn_const_of_harmonicOnNhd_of_isLocalMaxOn: the domain-relative local strong maximum principle.
• TauCeti.eqOn_const_of_harmonicOnNhd_of_isLocalMinOn: the domain-relative local strong minimum principle.
• TauCeti.eqOn_const_of_harmonicOnNhd_of_isMaxOn: the strong maximum principle.
• TauCeti.eqOn_const_of_harmonicOnNhd_of_isMinOn: the strong minimum principle.

For direct use on open domains, each local-extremum theorem also has an _of_isOpen consumer form accepting IsOpen Ω and a ∈ Ω in place of the more general hypothesis Ω ∈ 𝓝 a. The open-domain forms of the vanishing, comparison and global-extremum theorems hold in every finite-dimensional real inner product space, and are proved from Hopf's lemma in TauCeti.Analysis.InnerProductSpace.Laplacian.StrongMaximumPrinciple.

theorem TauCeti.eq_zero_on_of_harmonicOnNhd_of_nonneg_of_eq_zero {f : ℂ → ℝ} {Ω : Set ℂ} {a : ℂ} (hΩa : Ω ∈ nhds a) (hΩconn : IsPreconnected Ω) (hf : InnerProductSpace.HarmonicOnNhd f Ω) (hnonneg : ∀ z ∈ Ω, 0 ≤ f z) (hfa : f a = 0) : Set.EqOn f 0 Ω

A nonnegative harmonic function on a preconnected planar set that vanishes at an interior point vanishes throughout the set.

The neighborhood hypothesis places a disk around the vanishing point. The conclusion can fail on a disconnected set, where a harmonic function may vanish on one component and be positive on another.

theorem TauCeti.eqOn_of_harmonicOnNhd_of_le_of_eq {f g : ℂ → ℝ} {Ω : Set ℂ} {a : ℂ} (hΩa : Ω ∈ nhds a) (hΩconn : IsPreconnected Ω) (hf : InnerProductSpace.HarmonicOnNhd f Ω) (hg : InnerProductSpace.HarmonicOnNhd g Ω) (hfg : ∀ z ∈ Ω, f z ≤ g z) (hfg_a : f a = g a) : Set.EqOn f g Ω

Strong comparison principle for planar harmonic functions.

Let f and g be harmonic on a preconnected set that is a neighborhood of a. If f ≤ g throughout the set and they agree at a, then they agree throughout the set.

theorem TauCeti.eqOn_const_of_harmonicOnNhd_of_isLocalMax {f : ℂ → ℝ} {Ω : Set ℂ} {a : ℂ} (hΩa : Ω ∈ nhds a) (hΩconn : IsPreconnected Ω) (hf : InnerProductSpace.HarmonicOnNhd f Ω) (hmax : IsLocalMax f a) : Set.EqOn f (Function.const ℂ (f a)) Ω

Local strong maximum principle for planar harmonic functions.

A real-valued harmonic function on a preconnected planar set that contains a neighborhood of a local maximum point is constant throughout the set.

theorem TauCeti.eqOn_const_of_harmonicOnNhd_of_isLocalMax_of_isOpen {f : ℂ → ℝ} {Ω : Set ℂ} {a : ℂ} (hΩopen : IsOpen Ω) (ha : a ∈ Ω) (hΩconn : IsPreconnected Ω) (hf : InnerProductSpace.HarmonicOnNhd f Ω) (hmax : IsLocalMax f a) : Set.EqOn f (Function.const ℂ (f a)) Ω

Open-domain form of eqOn_const_of_harmonicOnNhd_of_isLocalMax.

theorem TauCeti.eqOn_const_of_harmonicOnNhd_of_isLocalMin {f : ℂ → ℝ} {Ω : Set ℂ} {a : ℂ} (hΩa : Ω ∈ nhds a) (hΩconn : IsPreconnected Ω) (hf : InnerProductSpace.HarmonicOnNhd f Ω) (hmin : IsLocalMin f a) : Set.EqOn f (Function.const ℂ (f a)) Ω

Local strong minimum principle for planar harmonic functions.

A real-valued harmonic function on a preconnected planar set that contains a neighborhood of a local minimum point is constant throughout the set.

theorem TauCeti.eqOn_const_of_harmonicOnNhd_of_isLocalMin_of_isOpen {f : ℂ → ℝ} {Ω : Set ℂ} {a : ℂ} (hΩopen : IsOpen Ω) (ha : a ∈ Ω) (hΩconn : IsPreconnected Ω) (hf : InnerProductSpace.HarmonicOnNhd f Ω) (hmin : IsLocalMin f a) : Set.EqOn f (Function.const ℂ (f a)) Ω

Open-domain form of eqOn_const_of_harmonicOnNhd_of_isLocalMin.

theorem TauCeti.eqOn_const_of_harmonicOnNhd_of_isLocalMaxOn {f : ℂ → ℝ} {Ω : Set ℂ} {a : ℂ} (hΩa : Ω ∈ nhds a) (hΩconn : IsPreconnected Ω) (hf : InnerProductSpace.HarmonicOnNhd f Ω) (hmax : IsLocalMaxOn f Ω a) : Set.EqOn f (Function.const ℂ (f a)) Ω

Domain-relative local strong maximum principle for planar harmonic functions.

A real-valued harmonic function on a preconnected planar set that contains a neighborhood of a relative local maximum point is constant throughout the set.

theorem TauCeti.eqOn_const_of_harmonicOnNhd_of_isLocalMaxOn_of_isOpen {f : ℂ → ℝ} {Ω : Set ℂ} {a : ℂ} (hΩopen : IsOpen Ω) (ha : a ∈ Ω) (hΩconn : IsPreconnected Ω) (hf : InnerProductSpace.HarmonicOnNhd f Ω) (hmax : IsLocalMaxOn f Ω a) : Set.EqOn f (Function.const ℂ (f a)) Ω

Open-domain form of eqOn_const_of_harmonicOnNhd_of_isLocalMaxOn.

theorem TauCeti.eqOn_const_of_harmonicOnNhd_of_isLocalMinOn {f : ℂ → ℝ} {Ω : Set ℂ} {a : ℂ} (hΩa : Ω ∈ nhds a) (hΩconn : IsPreconnected Ω) (hf : InnerProductSpace.HarmonicOnNhd f Ω) (hmin : IsLocalMinOn f Ω a) : Set.EqOn f (Function.const ℂ (f a)) Ω

Domain-relative local strong minimum principle for planar harmonic functions.

A real-valued harmonic function on a preconnected planar set that contains a neighborhood of a relative local minimum point is constant throughout the set.

theorem TauCeti.eqOn_const_of_harmonicOnNhd_of_isLocalMinOn_of_isOpen {f : ℂ → ℝ} {Ω : Set ℂ} {a : ℂ} (hΩopen : IsOpen Ω) (ha : a ∈ Ω) (hΩconn : IsPreconnected Ω) (hf : InnerProductSpace.HarmonicOnNhd f Ω) (hmin : IsLocalMinOn f Ω a) : Set.EqOn f (Function.const ℂ (f a)) Ω

Open-domain form of eqOn_const_of_harmonicOnNhd_of_isLocalMinOn.

theorem TauCeti.eqOn_const_of_harmonicOnNhd_of_isMaxOn {f : ℂ → ℝ} {Ω : Set ℂ} {a : ℂ} (hΩa : Ω ∈ nhds a) (hΩconn : IsPreconnected Ω) (hf : InnerProductSpace.HarmonicOnNhd f Ω) (hmax : IsMaxOn f Ω a) : Set.EqOn f (Function.const ℂ (f a)) Ω

Strong maximum principle for planar harmonic functions, global-extremum form.

A real-valued harmonic function on a preconnected planar set that contains a neighborhood of an attained maximum point is constant throughout the set.

theorem TauCeti.eqOn_const_of_harmonicOnNhd_of_isMinOn {f : ℂ → ℝ} {Ω : Set ℂ} {a : ℂ} (hΩa : Ω ∈ nhds a) (hΩconn : IsPreconnected Ω) (hf : InnerProductSpace.HarmonicOnNhd f Ω) (hmin : IsMinOn f Ω a) : Set.EqOn f (Function.const ℂ (f a)) Ω

Strong minimum principle for planar harmonic functions, global-extremum form.

A real-valued harmonic function on a preconnected planar set that contains a neighborhood of an attained minimum point is constant throughout the set.