The weak maximum principle for -Δ + c with a nonnegative zeroth-order term

TauCeti.Analysis.InnerProductSpace.Laplacian.WeakMaximumPrinciple proves the weak maximum principle for the bare Laplacian: a subharmonic (0 ≤ Δ f) function on a compact set is bounded on all of K by any bound it satisfies on frontier K. The next step of the PDE roadmap (Lane C, item 13, "then for general elliptic L (sign condition c ≥ 0)") is to restore the zeroth-order term, i.e. to allow the operator L u = -Δ u + c u with a nonnegative coefficient c.

The sign condition c ≥ 0 is load-bearing: it is exactly what lets the maximum principle survive the extra term. A subsolution of L, L f ≤ 0, is a function with c · f ≤ Δ f on the interior, and the conclusion is one-sided in the standard sup u ≤ sup_{∂} u⁺ shape: a subsolution bounded by a nonnegative m on the frontier is bounded by m throughout. (The nonnegativity of m is needed once c ≠ 0; on the set where f ≤ 0 ≤ m the estimate is automatic, and the argument only has to control the set where f is positive, where c · f ≥ 0 makes f subharmonic.)

The proof reuses the perturbation f + ε‖·‖² of the bare-Laplacian file, but replaces the strictly-subharmonic boundary principle by the maximizer step TauCeti.le_of_isMaxOn_add_smul of TauCeti.Analysis.InnerProductSpace.Laplacian.BarrierMaximizer, run here with no drift and the quadratic barrier. At a maximizer of the perturbation the bound f z ≤ m either holds already, or m < f z puts f z above the nonnegative m, which forces Δ(f + ε‖·‖²) > 0 and so contradicts local maximality. Letting ε → 0 gives the bound.

Main declarations

• TauCeti.le_of_mul_le_laplacian_le_frontier: weak maximum principle for -Δ + c, c ≥ 0. A continuous function that is C² on the interior with c · f ≤ Δ f (a subsolution of -Δ + c) and c ≥ 0 there is bounded by any nonnegative m it respects on frontier K.
• TauCeti.le_of_mul_le_laplacian_le_of_le_frontier: comparison principle for -Δ + c, c ≥ 0. A subsolution f and a supersolution g ordered by f ≤ g on frontier K stay ordered f ≤ g on all of K.
• TauCeti.ge_of_laplacian_le_mul_ge_frontier: the dual weak minimum principle for supersolutions (Δ f ≤ c · f), bounded below by any nonpositive lower bound on the frontier.
• TauCeti.abs_le_of_laplacian_eq_mul_abs_le_frontier: a solution of -Δ u + c u = 0 (Δ f = c · f) is bounded on K by any bound its absolute value respects on frontier K.
• TauCeti.eqOn_of_laplacian_sub_mul_eq_of_eqOn_frontier: uniqueness for the Dirichlet problem for -Δ + c. Two functions with the same Δ · - c · · on the interior and the same boundary values agree on K.

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

Weak maximum principle for the operator -Δ + c with c ≥ 0.

Let K be compact. If f is continuous on K, is C² on interior K, and is a subsolution of -Δ + c there (c x * f x ≤ Δ f x) with a nonnegative coefficient (0 ≤ c x), then any nonnegative bound m that f respects on frontier K bounds f on all of K.

The nonnegativity of m cannot be dropped once c ≠ 0; it encodes the sup u ≤ sup_{∂} u⁺ shape of the estimate.

theorem TauCeti.le_of_mul_le_laplacian_le_of_le_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {K : Set E} (hK : IsCompact K) {c f g : E → ℝ} (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) (hc : ∀ ⦃x : E⦄, x ∈ interior K → 0 ≤ c x) (hsub : ∀ ⦃x : E⦄, x ∈ interior K → c x * f x ≤ Laplacian.laplacian f x) (hsuper : ∀ ⦃x : E⦄, x ∈ interior K → Laplacian.laplacian g x ≤ c x * g x) (hbdry : ∀ ⦃x : E⦄, x ∈ frontier K → f x ≤ g x) ⦃x : E⦄ : x ∈ K → f x ≤ g x

Comparison principle for -Δ + c with c ≥ 0.

Let K be compact and let f, g be continuous on K and C² on interior K, with a nonnegative coefficient c there. If f is a subsolution and g a supersolution of -Δ + c (c · f ≤ Δ f and Δ g ≤ c · g) and f ≤ g on frontier K, then f ≤ g on all of K. This is the two-function form of le_of_mul_le_laplacian_le_frontier.

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

Weak minimum principle for supersolutions of -Δ + c with c ≥ 0.

The dual of le_of_mul_le_laplacian_le_frontier: a continuous, C², supersolution (Δ f x ≤ c x * f x) with a nonnegative coefficient is bounded below on K by any nonpositive lower bound it respects on frontier K.

theorem TauCeti.abs_le_of_laplacian_eq_mul_abs_le_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {K : Set E} (hK : IsCompact K) {c f : E → ℝ} {M : ℝ} (hM : 0 ≤ M) (hcont : ContinuousOn f K) (hcd : ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 f x) (hc : ∀ ⦃x : E⦄, x ∈ interior K → 0 ≤ c x) (hsol : ∀ ⦃x : E⦄, x ∈ interior K → Laplacian.laplacian f x = c x * f x) (hbdry : ∀ ⦃x : E⦄, x ∈ frontier K → |f x| ≤ M) ⦃x : E⦄ : x ∈ K → |f x| ≤ M

A solution of -Δ u + c u = 0 (Δ f = c · f) with c ≥ 0, continuous on a compact set K and C² on its interior, is bounded on K by any bound M its absolute value respects on frontier K.

theorem TauCeti.eqOn_of_laplacian_sub_mul_eq_of_eqOn_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {K : Set E} (hK : IsCompact K) {c f g : E → ℝ} (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) (hc : ∀ ⦃x : E⦄, x ∈ interior K → 0 ≤ c x) (hlap : ∀ ⦃x : E⦄, x ∈ interior K → Laplacian.laplacian f x - c x * f x = Laplacian.laplacian g x - c x * g x) (hbdry : ∀ ⦃x : E⦄, x ∈ frontier K → f x = g x) : Set.EqOn f g K

Uniqueness for the Dirichlet problem for -Δ + c with c ≥ 0.

If f and g are continuous on a compact set K, C² on interior K with the same source term Δ · - c · · there (so both solve -Δ u + c u = h for one h), and agree on frontier K, then they agree on all of K.