The comparison principle and Dirichlet uniqueness for the Laplacian

TauCeti.Analysis.InnerProductSpace.Laplacian.WeakMaximumPrinciple proves the weak maximum principle: a continuous, C², subharmonic (0 ≤ Δ f) function on a compact set is bounded on all of K by any bound it respects on frontier K. This file turns that one-sided statement into the two-function comparison principle and its consequence, uniqueness for the Dirichlet problem (PDE roadmap, Lane C, item 13, "the comparison principle").

Applied to the difference f - g, the weak maximum principle says: if Δ g ≤ Δ f on the interior and f ≤ g on the frontier, then f ≤ g throughout K. Comparing in both directions gives that a solution of the Poisson equation Δ u = h in interior K is determined on all of K by its boundary values on frontier K; specialized to h = 0 this is uniqueness of the Dirichlet problem for the Laplace equation. The maximum and minimum of a harmonic function are attained on the frontier, so a harmonic function is bounded by the supremum of |·| over frontier K.

Main declarations

• TauCeti.le_of_laplacian_le_of_le_frontier: comparison principle. If Δ g ≤ Δ f on the interior of a compact set and f ≤ g on its frontier, then f ≤ g on all of K.
• TauCeti.eqOn_of_laplacian_eqOn_of_eqOn_frontier: uniqueness for the Poisson equation. Two functions with the same Laplacian on the interior and the same boundary values agree on K.
• TauCeti.eqOn_of_harmonicOnNhd_of_eqOn_frontier: uniqueness of the Dirichlet problem for the Laplace equation: two harmonic functions with the same boundary values agree on K.
• TauCeti.exists_mem_frontier_isMaxOn_of_harmonicOnNhd / TauCeti.exists_mem_frontier_isMinOn_of_harmonicOnNhd: a harmonic function attains its maximum and its minimum on the frontier.
• TauCeti.abs_le_of_harmonicOnNhd_of_abs_le_frontier: a harmonic function is bounded on K by any bound its absolute value respects on frontier K.

theorem TauCeti.le_of_laplacian_le_of_le_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {K : Set E} {f g : E → ℝ} (hK : IsCompact K) (hfcont : ContinuousOn f K) (hgcont : ContinuousOn g K) (hfcd : ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 f x) (hgcd : ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 g x) (hlap : ∀ ⦃x : E⦄, x ∈ interior K → Laplacian.laplacian g x ≤ Laplacian.laplacian f x) (hbdry : ∀ ⦃x : E⦄, x ∈ frontier K → f x ≤ g x) ⦃x : E⦄ : x ∈ K → f x ≤ g x

Comparison principle for the Laplacian.

Let K be compact, and let f, g be continuous on K and C² on interior K. If f is at least as subharmonic as g there (Δ g ≤ Δ f) and f ≤ g on frontier K, then f ≤ g on all of K. This is the two-function form of the weak maximum principle le_of_laplacian_nonneg_le_frontier, applied to the difference f - g.

theorem TauCeti.eqOn_of_laplacian_eqOn_of_eqOn_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {K : Set E} {f g : E → ℝ} (hK : IsCompact K) (hfcont : ContinuousOn f K) (hgcont : ContinuousOn g K) (hfcd : ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 f x) (hgcd : ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 g x) (hlap : ∀ ⦃x : E⦄, x ∈ interior K → Laplacian.laplacian f x = Laplacian.laplacian g x) (hbdry : ∀ ⦃x : E⦄, x ∈ frontier K → f x = g x) : Set.EqOn f g K

Uniqueness for the Poisson equation.

If f and g are continuous on a compact set K, C² on interior K with the same Laplacian there, and agree on frontier K, then they agree on all of K. A solution of Δ u = h in interior K is thus determined by its boundary values.

theorem TauCeti.eqOn_of_harmonicOnNhd_of_eqOn_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {K : Set E} {f g : E → ℝ} (hK : IsCompact K) (hfcont : ContinuousOn f K) (hgcont : ContinuousOn g K) (hf : InnerProductSpace.HarmonicOnNhd f (interior K)) (hg : InnerProductSpace.HarmonicOnNhd g (interior K)) (hbdry : ∀ ⦃x : E⦄, x ∈ frontier K → f x = g x) : Set.EqOn f g K

Uniqueness of the Dirichlet problem for the Laplace equation.

Two functions that are harmonic on the interior of a compact set K, continuous on K, and equal on frontier K are equal on all of K.

theorem TauCeti.exists_mem_frontier_isMaxOn_of_harmonicOnNhd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {K : Set E} {f : E → ℝ} (hK : IsCompact K) (hne : K.Nonempty) (hcont : ContinuousOn f K) (hf : InnerProductSpace.HarmonicOnNhd f (interior K)) : ∃ x ∈ frontier K, IsMaxOn f K x

A function harmonic on the interior of a nonempty compact set and continuous on K attains its maximum on frontier K.

theorem TauCeti.exists_mem_frontier_isMinOn_of_harmonicOnNhd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {K : Set E} {f : E → ℝ} (hK : IsCompact K) (hne : K.Nonempty) (hcont : ContinuousOn f K) (hf : InnerProductSpace.HarmonicOnNhd f (interior K)) : ∃ x ∈ frontier K, IsMinOn f K x

A function harmonic on the interior of a nonempty compact set and continuous on K attains its minimum on frontier K.

theorem TauCeti.abs_le_of_harmonicOnNhd_of_abs_le_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {K : Set E} {f : E → ℝ} {M : ℝ} (hK : IsCompact K) (hcont : ContinuousOn f K) (hf : InnerProductSpace.HarmonicOnNhd f (interior K)) (hbdry : ∀ ⦃x : E⦄, x ∈ frontier K → |f x| ≤ M) ⦃x : E⦄ : x ∈ K → |f x| ≤ M

A function harmonic on the interior of a compact set K and continuous on K is bounded on all of K by any bound M its absolute value respects on frontier K. This is the two-sided consequence of the maximum principle for harmonic functions.