Maximum principles for subharmonic functions

The Laplacian is the non-divergence operator with the identity as coefficient matrix and no lower-order terms, up to sign. The classical weak and strong maximum principles and the uniqueness of the Dirichlet problem specialise to subharmonic, superharmonic and harmonic functions, in the sense of the sum of the second coordinate partials.

Main declarations

• EllipticPdes.Classical.laplacianSum: the sum of the second coordinate partials.
• EllipticPdes.Classical.nondivOp_laplace: the Laplacian as a non-divergence operator.
• EllipticPdes.Classical.weak_maximum_principle_subharmonic: the weak maximum principle.
• EllipticPdes.Classical.strong_maximum_principle_subharmonic: the strong maximum principle.
• EllipticPdes.Classical.strong_minimum_principle_superharmonic: the strong minimum principle.
• EllipticPdes.Classical.harmonic_const_of_max, harmonic_const_of_min: a harmonic function attaining its supremum or infimum in the interior is constant.
• EllipticPdes.Classical.dirichlet_unique_harmonic: uniqueness for the Dirichlet problem.

References

James Guo, Partial Differential Equations (Course Lecture Notes), Lemma XI.1.5, Corollary XI.1.6, Lemma XI.1.7 (p. 92) and Lemma XI.2.4 (p. 95).

noncomputable def EllipticPdes.Classical.laplacianSum {d : ℕ} (u : EuclideanSpace ℝ (Fin d) → ℝ) (x : EuclideanSpace ℝ (Fin d)) : ℝ

The sum of the second coordinate partials.

Equations

• EllipticPdes.Classical.laplacianSum u x = ∑ i : Fin d, EllipticPdes.Sobolev.partialD i (EllipticPdes.Sobolev.partialD i u) x

def EllipticPdes.Classical.idCoeff {d : ℕ} (i j : Fin d) : ℝ

The identity coefficient matrix.

Equations

• EllipticPdes.Classical.idCoeff i j = if i = j then 1 else 0

theorem EllipticPdes.Classical.nondivOp_laplace {d : ℕ} (u : EuclideanSpace ℝ (Fin d) → ℝ) (x : EuclideanSpace ℝ (Fin d)) : nondivOp (fun (x : EuclideanSpace ℝ (Fin d)) => idCoeff) (fun (x : EuclideanSpace ℝ (Fin d)) (x_1 : Fin d) => 0) (fun (x : EuclideanSpace ℝ (Fin d)) => 0) u x = -laplacianSum u x

The Laplacian is the negative of the non-divergence operator with the identity as coefficient matrix and no lower-order terms.

theorem EllipticPdes.Classical.idCoeff_symm {d : ℕ} (i j : Fin d) : idCoeff i j = idCoeff j i

The identity matrix is symmetric.

theorem EllipticPdes.Classical.idCoeff_ell {d : ℕ} (ξ : Fin d → ℝ) : 1 * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, idCoeff i j * ξ i * ξ j

The identity matrix is elliptic with constant one.

theorem EllipticPdes.Classical.idCoeff_bdd {d : ℕ} (i j : Fin d) : |idCoeff i j| ≤ 1

The identity matrix is bounded by one.

theorem EllipticPdes.Classical.laplacianSum_neg {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) {x : EuclideanSpace ℝ (Fin d)} (hx : x ∈ U) : laplacianSum (fun (y : EuclideanSpace ℝ (Fin d)) => -u y) x = -laplacianSum u x

The Laplacian of a negative.

theorem EllipticPdes.Classical.weak_maximum_principle_subharmonic {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hUne : U.Nonempty) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (huc : ContinuousOn u (closure U)) (hsub : ∀ x ∈ U, 0 ≤ laplacianSum u x) : ∃ y ∈ frontier U, ∀ x ∈ closure U, u x ≤ u y

Weak maximum principle for subharmonic functions (Guo Lemma XI.1.7). A function C² on a bounded open set, continuous on its closure, with nonnegative Laplacian on the set, attains its maximum over the closure on the boundary.

theorem EllipticPdes.Classical.strong_maximum_principle_subharmonic {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUc : IsPreconnected U) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (hsub : ∀ x ∈ U, 0 ≤ laplacianSum u x) {x₀ : EuclideanSpace ℝ (Fin d)} (hx₀ : x₀ ∈ U) (hmax : ∀ x ∈ U, u x ≤ u x₀) (x : EuclideanSpace ℝ (Fin d)) : x ∈ U → u x = u x₀

Strong maximum principle for subharmonic functions (Guo Lemma XI.1.5). A function C² on a connected open set with nonnegative Laplacian that attains its supremum over the set at an interior point is constant.

theorem EllipticPdes.Classical.strong_minimum_principle_superharmonic {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUc : IsPreconnected U) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (hsup : ∀ x ∈ U, laplacianSum u x ≤ 0) {x₀ : EuclideanSpace ℝ (Fin d)} (hx₀ : x₀ ∈ U) (hmin : ∀ x ∈ U, u x₀ ≤ u x) (x : EuclideanSpace ℝ (Fin d)) : x ∈ U → u x = u x₀

Strong minimum principle for superharmonic functions (Guo Corollary XI.1.6). A function C² on a connected open set with nonpositive Laplacian that attains its infimum over the set at an interior point is constant.

theorem EllipticPdes.Classical.harmonic_const_of_max {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUc : IsPreconnected U) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (hharm : ∀ x ∈ U, laplacianSum u x = 0) {x₀ : EuclideanSpace ℝ (Fin d)} (hx₀ : x₀ ∈ U) (hmax : ∀ x ∈ U, u x ≤ u x₀) (x : EuclideanSpace ℝ (Fin d)) : x ∈ U → u x = u x₀

Harmonic functions attaining their supremum are constant (Guo Corollary XI.1.6).

theorem EllipticPdes.Classical.harmonic_const_of_min {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUc : IsPreconnected U) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (hharm : ∀ x ∈ U, laplacianSum u x = 0) {x₀ : EuclideanSpace ℝ (Fin d)} (hx₀ : x₀ ∈ U) (hmin : ∀ x ∈ U, u x₀ ≤ u x) (x : EuclideanSpace ℝ (Fin d)) : x ∈ U → u x = u x₀

Harmonic functions attaining their infimum are constant (Guo Corollary XI.1.6).

theorem EllipticPdes.Classical.dirichlet_unique_harmonic {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hUne : U.Nonempty) {u v : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (hv : ContDiffOn ℝ 2 v U) (huc : ContinuousOn u (closure U)) (hvc : ContinuousOn v (closure U)) (hL : ∀ x ∈ U, laplacianSum u x = laplacianSum v x) (hbd : ∀ x ∈ frontier U, u x = v x) (x : EuclideanSpace ℝ (Fin d)) : x ∈ closure U → u x = v x

Uniqueness for the Dirichlet problem for the Laplacian (Guo Lemma XI.2.4, the uniqueness clause). Two functions C² on a bounded open set and continuous on its closure, with the same Laplacian on the set and the same boundary values, agree on the closure.