Maximum principles with drift and a nonnegative zeroth-order term

This file combines the two lower-order extensions of the Laplacian maximum principle. For the operator -Δ - b·∇ + c, a nonnegative zeroth-order coefficient and a bounded drift preserve the weak maximum principle. The sign condition on c and the nonnegativity of the frontier bound are explicit, as required for the standard estimate sup u ≤ sup (u⁺|∂Ω).

Following Gilbarg--Trudinger, Elliptic Partial Differential Equations of Second Order, Chapter 3, the proof adapts the weak-principle argument from DriftMaximumPrinciple: it perturbs a subsolution by the same positive exponential barrier. At a positive interior maximum, its derivative vanishes and its Laplacian is nonpositive, while the subsolution inequality, c ≥ 0, and strict positivity of the barrier give the opposite strict inequality.

Main declarations

• TauCeti.le_of_mul_le_laplacian_add_fderiv_le_frontier: the weak maximum principle for -Δ - b·∇ + c.
• TauCeti.ge_of_laplacian_add_fderiv_le_mul_ge_frontier and TauCeti.abs_le_of_laplacian_add_fderiv_eq_mul_abs_le_frontier: its lower and two-sided forms.
• TauCeti.le_of_laplacian_add_fderiv_sub_mul_le_laplacian_add_fderiv_sub_mul_of_le_frontier: the corresponding comparison principle.
• TauCeti.eqOn_of_laplacian_add_fderiv_sub_mul_eq_of_eqOn_frontier: Dirichlet uniqueness for equal operator values.

theorem TauCeti.le_of_mul_le_laplacian_add_fderiv_le_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {K : Set E} (hK : IsCompact K) {c f : E → ℝ} {b : E → 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) (hb : ∀ ⦃x : E⦄, x ∈ interior K → ‖b x‖ ≤ β) (hsub : ∀ ⦃x : E⦄, x ∈ interior K → c x * f x ≤ Laplacian.laplacian f x + (fderiv ℝ f x) (b x)) (hbdry : ∀ ⦃x : E⦄, x ∈ frontier K → f x ≤ m) ⦃x : E⦄ : x ∈ K → f x ≤ m

Weak maximum principle for -Δ - b·∇ + c.

If c is nonnegative, b has norm at most β on the interior of a compact set, and c x * f x ≤ Δ f x + fderiv ℝ f x (b x), then every nonnegative frontier bound for f is a bound on the whole set.

theorem TauCeti.ge_of_laplacian_add_fderiv_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 → ℝ} {b : E → 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) (hb : ∀ ⦃x : E⦄, x ∈ interior K → ‖b x‖ ≤ β) (hsuper : ∀ ⦃x : E⦄, x ∈ interior K → Laplacian.laplacian f x + (fderiv ℝ f x) (b 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 -Δ - b·∇ + c. This is the negation-dual of le_of_mul_le_laplacian_add_fderiv_le_frontier.

theorem TauCeti.abs_le_of_laplacian_add_fderiv_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 → ℝ} {b : E → 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) (hb : ∀ ⦃x : E⦄, x ∈ interior K → ‖b x‖ ≤ β) (hsol : ∀ ⦃x : E⦄, x ∈ interior K → Laplacian.laplacian f x + (fderiv ℝ f x) (b x) = c x * f x) (hbdry : ∀ ⦃x : E⦄, x ∈ frontier K → |f x| ≤ M) ⦃x : E⦄ : x ∈ K → |f x| ≤ M

A solution of -Δ f - b·∇f + c f = 0 is bounded in absolute value by every nonnegative bound for its absolute value on the frontier.

theorem TauCeti.le_of_laplacian_add_fderiv_sub_mul_le_laplacian_add_fderiv_sub_mul_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 → ℝ} {b : E → 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) (hb : ∀ ⦃x : E⦄, x ∈ interior K → ‖b x‖ ≤ β) (hL : ∀ ⦃x : E⦄, x ∈ interior K → Laplacian.laplacian g x + (fderiv ℝ g x) (b x) - c x * g x ≤ Laplacian.laplacian f x + (fderiv ℝ f x) (b x) - c x * f x) (hbdry : ∀ ⦃x : E⦄, x ∈ frontier K → f x ≤ g x) ⦃x : E⦄ : x ∈ K → f x ≤ g x

Comparison principle for -Δ - b·∇ + c. Functions acted on by the same lower-order coefficients are ordered on a compact set when their operator values and frontier values are ordered.

theorem TauCeti.eqOn_of_laplacian_add_fderiv_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 → ℝ} {b : E → 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) (hb : ∀ ⦃x : E⦄, x ∈ interior K → ‖b x‖ ≤ β) (hL : ∀ ⦃x : E⦄, x ∈ interior K → Laplacian.laplacian f x + (fderiv ℝ f x) (b x) - c x * f x = Laplacian.laplacian g x + (fderiv ℝ g x) (b x) - c x * g x) (hbdry : Set.EqOn f g (frontier K)) : Set.EqOn f g K

Dirichlet uniqueness for -Δ - b·∇ + c. Equal operator values and equal frontier data force two functions to agree throughout the compact set.