The weak maximum principle for subharmonic functions

TauCeti.Analysis.InnerProductSpace.Laplacian.MaximumPrinciple proves the strict boundary maximum principle: a C² function with 0 < Δ f on the interior of a compact set attains its maximum on the frontier. That strict hypothesis is only a warm-up; the theorem PDE theory actually uses is the weak maximum principle, which relaxes 0 < Δ f to the borderline 0 ≤ Δ f (subharmonic). This file supplies it, in bound form and in the extremum (∃) form.

Main declarations

• TauCeti.le_of_laplacian_nonneg_le_frontier: weak maximum principle. A continuous function on a compact set that is C² and subharmonic (0 ≤ Δ f) on the interior is bounded on all of K by any bound it satisfies on frontier K.
• TauCeti.ge_of_laplacian_nonpos_ge_frontier: the dual weak minimum principle for superharmonic functions (Δ f ≤ 0).
• TauCeti.exists_mem_frontier_isMaxOn_of_laplacian_nonneg / TauCeti.exists_mem_frontier_isMinOn_of_laplacian_nonpos: on a nonempty compact set in a nontrivial finite-dimensional real inner product space, a subharmonic (resp. superharmonic) function attains a maximum (resp. minimum) on the frontier.

theorem TauCeti.le_of_forall_pos_mul_le {a m C : ℝ} (hC : 0 ≤ C) (h : ∀ (ε : ℝ), 0 < ε → a ≤ m + ε * C) : a ≤ m

The ε → 0 limit of a perturbation estimate: if a ≤ m + ε * C for every ε > 0, with a nonnegative constant C, then a ≤ m. This packages the endgame of the perturbation arguments in the weak maximum principles.

theorem TauCeti.exists_mem_frontier_isMaxOn_of_le_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K : Set E} (hK : IsCompact K) [Nontrivial E] (hne : K.Nonempty) {f : E → ℝ} (hcont : ContinuousOn f K) (hbound : ∀ {m : ℝ}, (∀ ⦃x : E⦄, x ∈ frontier K → f x ≤ m) → ∀ ⦃x : E⦄, x ∈ K → f x ≤ m) : ∃ x ∈ frontier K, IsMaxOn f K x

If every upper bound for a continuous function on the frontier of a nonempty compact set is also an upper bound on the whole set, then the function attains a maximum on the frontier.

theorem TauCeti.laplacian_add_const_smul_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (ε : ℝ) (hf : ContDiffAt ℝ 2 f x) : Laplacian.laplacian (fun (y : E) => f y + ε • ‖y‖ ^ 2) x = Laplacian.laplacian f x + ε * (2 * ↑(Module.finrank ℝ E))

The Laplacian of the perturbation f + ε‖·‖² at a point where f is C²: it exceeds Δ f by the contribution ε * (2 * dim E) of the strictly convex term ε‖·‖². This is the computation the bare-Laplacian and the -Δ + c weak maximum principles both run on the perturbed function.

theorem TauCeti.le_of_forall_pos_exists_isMaxOn_perturbation {E : Type u_1} [NormedAddCommGroup E] {K : Set E} (hK : Bornology.IsBounded K) {f : E → ℝ} {m : ℝ} {x : E} (hxK : x ∈ K) (H : ∀ (ε : ℝ), 0 < ε → ∃ z ∈ K, IsMaxOn (fun (y : E) => f y + ε • ‖y‖ ^ 2) K z ∧ f z ≤ m) : f x ≤ m

The ε → 0 perturbation engine of the weak maximum principles. To bound f x ≤ m on a bounded set K, it suffices to produce, for every ε > 0, a point z ∈ K at which the perturbation f + ε‖·‖² attains its maximum over K and where f z ≤ m: bounding ‖·‖² by a constant on the bounded K and letting ε → 0 then gives f x ≤ m. The bare-Laplacian and -Δ + c weak maximum principles differ only in how they produce such a maximizer, so this lemma packages everything they share.

theorem TauCeti.le_of_laplacian_nonneg_le_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {K : Set E} (hK : IsCompact K) {f : E → ℝ} {m : ℝ} (hcont : ContinuousOn f K) (hcd : ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 f x) (hlap : ∀ ⦃x : E⦄, x ∈ interior K → 0 ≤ Laplacian.laplacian f x) (hbdry : ∀ ⦃x : E⦄, x ∈ frontier K → f x ≤ m) ⦃x : E⦄ : x ∈ K → f x ≤ m

Weak maximum principle for subharmonic functions.

Let K be compact. If f is continuous on K, is C² on interior K, and is subharmonic there (0 ≤ Δ f), then any bound m that f respects on frontier K bounds f on all of K.

theorem TauCeti.ge_of_laplacian_nonpos_ge_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {K : Set E} (hK : IsCompact K) {f : E → ℝ} {m : ℝ} (hcont : ContinuousOn f K) (hcd : ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 f x) (hlap : ∀ ⦃x : E⦄, x ∈ interior K → Laplacian.laplacian f x ≤ 0) (hbdry : ∀ ⦃x : E⦄, x ∈ frontier K → m ≤ f x) ⦃x : E⦄ : x ∈ K → m ≤ f x

Weak minimum principle for superharmonic functions.

The dual of le_of_laplacian_nonneg_le_frontier: a continuous, C², superharmonic (Δ f ≤ 0) function on a compact set is bounded below on K by any lower bound it respects on frontier K.

theorem TauCeti.exists_mem_frontier_isMaxOn_of_laplacian_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {K : Set E} (hK : IsCompact K) (hne : K.Nonempty) {f : E → ℝ} (hcont : ContinuousOn f K) (hcd : ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 f x) (hlap : ∀ ⦃x : E⦄, x ∈ interior K → 0 ≤ Laplacian.laplacian f x) : ∃ x ∈ frontier K, IsMaxOn f K x

A subharmonic (0 ≤ Δ f) continuous function on a nonempty compact set in a nontrivial finite-dimensional real inner product space attains a maximum on the frontier. This is the ∃-form of the weak maximum principle, mirroring exists_mem_frontier_isMaxOn_of_laplacian_pos for the strict case.

theorem TauCeti.exists_mem_frontier_isMinOn_of_laplacian_nonpos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {K : Set E} (hK : IsCompact K) (hne : K.Nonempty) {f : E → ℝ} (hcont : ContinuousOn f K) (hcd : ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 f x) (hlap : ∀ ⦃x : E⦄, x ∈ interior K → Laplacian.laplacian f x ≤ 0) : ∃ x ∈ frontier K, IsMinOn f K x

A superharmonic (Δ f ≤ 0) continuous function on a nonempty compact set in a nontrivial finite-dimensional real inner product space attains a minimum on the frontier.