Classical weak maximum principle

The weak maximum principle for a C² subsolution of a non-divergence-form elliptic equation on a bounded open set: the maximum over the closure is attained on the boundary. Two pointwise facts drive the proof. At an interior maximum of a C² function the gradient vanishes and the Hessian is negative semidefinite, so the principal part -∑ aᵢⱼ ∂ᵢ∂ⱼ u is nonnegative there, the coefficient matrix being positive semidefinite; this rests on the trace inequality ∑ aᵢⱼ hᵢⱼ ≤ 0 for a positive semidefinite and h negative semidefinite, proved through the spectral theorem. A strict subsolution therefore has no interior maximum. The general case perturbs by ε exp(λ x₁), which is a strict subsolution for λ large by uniform ellipticity and the bound on the transport coefficient, and lets ε tend to zero.

The coefficients are asked to be symmetric, uniformly elliptic and, for the transport term, bounded on the set; the sources also ask for continuity, which the proof does not use.

Main declarations

• EllipticPdes.Classical.sum_mul_nonpos_of_posSemidef: the trace inequality.
• EllipticPdes.Classical.sndFDeriv_nonpos_of_isLocalMax: the Hessian is negative semidefinite at an interior local maximum.
• EllipticPdes.Classical.nondivOp: the non-divergence-form operator.
• EllipticPdes.Classical.weak_maximum_principle: the weak maximum principle for a subsolution with no zeroth-order term.
• EllipticPdes.Classical.weak_minimum_principle: the same for a supersolution.
• EllipticPdes.Classical.weak_maximum_principle_of_nonneg: the weak maximum principle with nonnegative zeroth-order coefficient, through the positive part on the boundary.

Operator convention

The non-divergence operator here is L u = -∑ aᵢⱼ ∂ᵢⱼu + ∑ bᵢ ∂ᵢu + c u. All Guo results cited in this file are translated by negating the source operator: Guo's operator is -L, with coefficients a, -b, -c. Thus his subsolution inequality (-L) u ≥ 0 becomes L u ≤ 0, and his potential condition -c ≤ 0 becomes c ≥ 0.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §6.4.1 Theorem 1 (p. 343) and Theorem 2 (p. 344); D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, §3.1 Theorem 3.1 (p. 32) and Corollary 3.2 (p. 33); James Guo, Partial Differential Equations (Course Lecture Notes), Theorem XI.3.7.

The trace inequality

theorem EllipticPdes.Classical.isHermitian_of_symm {d : ℕ} {A : Matrix (Fin d) (Fin d) ℝ} (h : ∀ (i j : Fin d), A i j = A j i) : A.IsHermitian

A real matrix is Hermitian when it is symmetric.

theorem EllipticPdes.Classical.posSemidef_of_forall {d : ℕ} {A : Matrix (Fin d) (Fin d) ℝ} (hsymm : ∀ (i j : Fin d), A i j = A j i) (hnn : ∀ (ξ : Fin d → ℝ), 0 ≤ ∑ i : Fin d, ∑ j : Fin d, A i j * ξ i * ξ j) : A.PosSemidef

A symmetric real matrix with nonnegative quadratic form is positive semidefinite.

theorem EllipticPdes.Classical.sum_mul_nonpos_of_posSemidef {d : ℕ} {A H : Matrix (Fin d) (Fin d) ℝ} (hA : A.PosSemidef) (hH : (-H).PosSemidef) : ∑ i : Fin d, ∑ j : Fin d, A i j * H i j ≤ 0

Trace inequality. For A positive semidefinite and -H positive semidefinite, ∑ᵢⱼ Aᵢⱼ Hᵢⱼ ≤ 0. Through the spectral theorem A = U D U*, the sum is the trace of A H, which is the trace of D (U* H U), a sum of nonnegative eigenvalues times the nonpositive diagonal entries of U* H U.

The second-order test at a local maximum

theorem EllipticPdes.Classical.deriv2_nonpos_of_isLocalMax {φ φ' φ'' : ℝ → ℝ} (h1 : ∀ᶠ (t : ℝ) in nhds 0, HasDerivAt φ (φ' t) t) (h2 : ∀ᶠ (t : ℝ) in nhds 0, HasDerivAt φ' (φ'' t) t) (hc : ContinuousAt φ'' 0) (hmax : IsLocalMax φ 0) : φ'' 0 ≤ 0

One-dimensional second-order test. A function with a continuous second derivative near 0 and a local maximum at 0 has nonpositive second derivative at 0.

theorem EllipticPdes.Classical.hasDerivAt_line {d : ℕ} {u : EuclideanSpace ℝ (Fin d) → ℝ} {x₀ ξ : EuclideanSpace ℝ (Fin d)} {t : ℝ} (hu : DifferentiableAt ℝ u (x₀ + t • ξ)) : HasDerivAt (fun (s : ℝ) => u (x₀ + s • ξ)) ((fderiv ℝ u (x₀ + t • ξ)) ξ) t

The derivative of a C² function along a line, and the derivative of that.

theorem EllipticPdes.Classical.hasDerivAt_line_fderiv {d : ℕ} {u : EuclideanSpace ℝ (Fin d) → ℝ} {x₀ ξ : EuclideanSpace ℝ (Fin d)} {t : ℝ} (hu : DifferentiableAt ℝ (fderiv ℝ u) (x₀ + t • ξ)) : HasDerivAt (fun (s : ℝ) => (fderiv ℝ u (x₀ + s • ξ)) ξ) (((fderiv ℝ (fderiv ℝ u) (x₀ + t • ξ)) ξ) ξ) t

The second derivative along a line.

theorem EllipticPdes.Classical.sndFDeriv_nonpos_of_isLocalMax {d : ℕ} {u : EuclideanSpace ℝ (Fin d) → ℝ} {x₀ : EuclideanSpace ℝ (Fin d)} (hu : ContDiffAt ℝ 2 u x₀) (hmax : IsLocalMax u x₀) (ξ : EuclideanSpace ℝ (Fin d)) : ((fderiv ℝ (fderiv ℝ u) x₀) ξ) ξ ≤ 0

Hessian at an interior local maximum. A C² function with a local maximum at x₀ has D²u(x₀)(ξ, ξ) ≤ 0 for every direction ξ.

The Hessian in coordinates

@[reducible, inline]

noncomputable abbrev EllipticPdes.Classical.e {d : ℕ} (i : Fin d) : EuclideanSpace ℝ (Fin d)

The coordinate vectors.

Equations

• EllipticPdes.Classical.e i = EuclideanSpace.single i 1

theorem EllipticPdes.Classical.sum_coord_smul_e {d : ℕ} (ξ : EuclideanSpace ℝ (Fin d)) : ∑ i : Fin d, ξ.ofLp i • e i = ξ

A vector is the sum of its coordinates times the coordinate vectors.

theorem EllipticPdes.Classical.sndFDeriv_apply_eq_sum {d : ℕ} (L : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (ξ : EuclideanSpace ℝ (Fin d)) : (L ξ) ξ = ∑ i : Fin d, ∑ j : Fin d, ξ.ofLp i * ξ.ofLp j * (L (e i)) (e j)

Second derivative in coordinates.

theorem EllipticPdes.Classical.partialD_eq {d : ℕ} (i : Fin d) (u : EuclideanSpace ℝ (Fin d) → ℝ) : Sobolev.partialD i u = fun (x : EuclideanSpace ℝ (Fin d)) => (fderiv ℝ u x) (e i)

The partial derivative, unapplied.

theorem EllipticPdes.Classical.partialD_partialD_eq {d : ℕ} {u : EuclideanSpace ℝ (Fin d) → ℝ} {x : EuclideanSpace ℝ (Fin d)} (hu : DifferentiableAt ℝ (fderiv ℝ u) x) (i j : Fin d) : Sobolev.partialD i (Sobolev.partialD j u) x = ((fderiv ℝ (fderiv ℝ u) x) (e i)) (e j)

Second partials as entries of the Hessian.

theorem EllipticPdes.Classical.sum_coeff_sndPartial_nonpos {d : ℕ} {a : Fin d → Fin d → ℝ} (hsymm : ∀ (i j : Fin d), a i j = a j i) (hpsd : ∀ (ξ : Fin d → ℝ), 0 ≤ ∑ i : Fin d, ∑ j : Fin d, a i j * ξ i * ξ j) {u : EuclideanSpace ℝ (Fin d) → ℝ} {x₀ : EuclideanSpace ℝ (Fin d)} (hu : ContDiffAt ℝ 2 u x₀) (hmax : IsLocalMax u x₀) : ∑ i : Fin d, ∑ j : Fin d, a i j * Sobolev.partialD i (Sobolev.partialD j u) x₀ ≤ 0

Nonpositivity of the coefficient-weighted Hessian at a local maximum.

The operator

noncomputable def EllipticPdes.Classical.nondivOp {d : ℕ} (a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ) (b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ) (c u : EuclideanSpace ℝ (Fin d) → ℝ) (x : EuclideanSpace ℝ (Fin d)) : ℝ

Non-divergence-form operator L u = -∑ aᵢⱼ ∂ᵢ∂ⱼ u + ∑ bᵢ ∂ᵢ u + c u.

Equations

• One or more equations did not get rendered due to their size.

theorem EllipticPdes.Classical.le_nondivOp_of_isLocalMax {d : ℕ} {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {c : EuclideanSpace ℝ (Fin d) → ℝ} {x₀ : EuclideanSpace ℝ (Fin d)} (hsymm : ∀ (i j : Fin d), a x₀ i j = a x₀ j i) (hpsd : ∀ (ξ : Fin d → ℝ), 0 ≤ ∑ i : Fin d, ∑ j : Fin d, a x₀ i j * ξ i * ξ j) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffAt ℝ 2 u x₀) (hmax : IsLocalMax u x₀) : c x₀ * u x₀ ≤ nondivOp a b c u x₀

Operator at an interior local maximum. The gradient vanishes and the coefficient-weighted Hessian is nonpositive, so L u ≥ c u there.

The exponential perturbation

noncomputable def EllipticPdes.Classical.expFn {d : ℕ} (lam : ℝ) (i₀ : Fin d) (x : EuclideanSpace ℝ (Fin d)) : ℝ

The perturbation exp (λ x_{i₀}).

Equations

• EllipticPdes.Classical.expFn lam i₀ x = Real.exp (lam * x.ofLp i₀)

theorem EllipticPdes.Classical.expFn_pos {d : ℕ} (lam : ℝ) (i₀ : Fin d) (x : EuclideanSpace ℝ (Fin d)) : 0 < expFn lam i₀ x

The perturbation is positive.

theorem EllipticPdes.Classical.contDiff_expFn {d : ℕ} (lam : ℝ) (i₀ : Fin d) : ContDiff ℝ 2 (expFn lam i₀)

The perturbation is smooth.

theorem EllipticPdes.Classical.hasFDerivAt_expFn {d : ℕ} (lam : ℝ) (i₀ : Fin d) (x : EuclideanSpace ℝ (Fin d)) : HasFDerivAt (expFn lam i₀) (expFn lam i₀ x • lam • EuclideanSpace.proj i₀) x

The derivative of the perturbation.

theorem EllipticPdes.Classical.proj_apply' {d : ℕ} (i : Fin d) (y : EuclideanSpace ℝ (Fin d)) : (EuclideanSpace.proj i) y = y.ofLp i

The projection is the coordinate.

theorem EllipticPdes.Classical.partialD_expFn {d : ℕ} (lam : ℝ) (i₀ i : Fin d) (x : EuclideanSpace ℝ (Fin d)) : Sobolev.partialD i (expFn lam i₀) x = (lam * if i₀ = i then 1 else 0) * expFn lam i₀ x

The first partials of the perturbation.

theorem EllipticPdes.Classical.partialD_partialD_expFn {d : ℕ} (lam : ℝ) (i₀ i j : Fin d) (x : EuclideanSpace ℝ (Fin d)) : Sobolev.partialD i (Sobolev.partialD j (expFn lam i₀)) x = (lam * if i₀ = j then 1 else 0) * ((lam * if i₀ = i then 1 else 0) * expFn lam i₀ x)

The second partials of the perturbation.

theorem EllipticPdes.Classical.nondivOp_expFn {d : ℕ} (a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ) (b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ) (c : EuclideanSpace ℝ (Fin d) → ℝ) (lam : ℝ) (i₀ : Fin d) (x : EuclideanSpace ℝ (Fin d)) : nondivOp a b c (expFn lam i₀) x = (-(a x i₀ i₀ * lam ^ 2) + b x i₀ * lam + c x) * expFn lam i₀ x

Operator on the perturbation.

Linearity of the operator at a point

theorem EllipticPdes.Classical.nondivOp_add_smul {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) {u v : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (hv : ContDiffOn ℝ 2 v U) (a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ) (b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ) (c : EuclideanSpace ℝ (Fin d) → ℝ) (ε : ℝ) {x : EuclideanSpace ℝ (Fin d)} (hx : x ∈ U) : nondivOp a b c (fun (y : EuclideanSpace ℝ (Fin d)) => u y + ε * v y) x = nondivOp a b c u x + ε * nondivOp a b c v x

Linearity of the operator at a point of an open set on which both functions are C².

The weak maximum principle

theorem EllipticPdes.Classical.frontier_nonempty_of_isBounded {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hUb : Bornology.IsBounded U) (hUne : U.Nonempty) : (frontier U).Nonempty

A bounded nonempty set has nonempty frontier.

theorem EllipticPdes.Classical.weak_maximum_principle {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hUne : U.Nonempty) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {θ B : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (huc : ContinuousOn u (closure U)) (hsub : ∀ x ∈ U, nondivOp a b (fun (x : EuclideanSpace ℝ (Fin d)) => 0) u x ≤ 0) : ∃ y ∈ frontier U, ∀ x ∈ closure U, u x ≤ u y

Weak maximum principle (Evans §6.4.1 Theorem 1(i), Gilbarg and Trudinger Theorem 3.1, Guo Theorem XI.3.7(i)). Let U be a bounded open nonempty set, L a non-divergence-form operator with symmetric uniformly elliptic coefficients, bounded transport coefficients and no zeroth-order term, and u a function C² on U and continuous on its closure with L u ≤ 0 on U. Then the maximum of u over the closure is attained on the boundary.

theorem EllipticPdes.Classical.nondivOp_zero {d : ℕ} (a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ) (b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ) (c : EuclideanSpace ℝ (Fin d) → ℝ) (x : EuclideanSpace ℝ (Fin d)) : nondivOp a b c (fun (x : EuclideanSpace ℝ (Fin d)) => 0) x = 0

The operator vanishes on the zero function.

theorem EllipticPdes.Classical.nondivOp_const {d : ℕ} (a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ) (b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ) (c : EuclideanSpace ℝ (Fin d) → ℝ) (K : ℝ) (x : EuclideanSpace ℝ (Fin d)) : nondivOp a b c (fun (x : EuclideanSpace ℝ (Fin d)) => K) x = c x * K

The operator on a constant.

theorem EllipticPdes.Classical.nondivOp_sub_const {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ) (b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ) (c : EuclideanSpace ℝ (Fin d) → ℝ) (K : ℝ) {x : EuclideanSpace ℝ (Fin d)} (hx : x ∈ U) : nondivOp a b c (fun (y : EuclideanSpace ℝ (Fin d)) => u y - K) x = nondivOp a b c u x - c x * K

The operator on a function minus a constant.

theorem EllipticPdes.Classical.nondivOp_sub {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) {u v : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (hv : ContDiffOn ℝ 2 v U) (a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ) (b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ) (c : EuclideanSpace ℝ (Fin d) → ℝ) {x : EuclideanSpace ℝ (Fin d)} (hx : x ∈ U) : nondivOp a b c (fun (y : EuclideanSpace ℝ (Fin d)) => u y - v y) x = nondivOp a b c u x - nondivOp a b c v x

The operator on a difference.

theorem EllipticPdes.Classical.nondivOp_congr_zeroth {d : ℕ} (a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ) (b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ) (c c' u : EuclideanSpace ℝ (Fin d) → ℝ) (x : EuclideanSpace ℝ (Fin d)) : nondivOp a b c' u x = nondivOp a b c u x + (c' x - c x) * u x

Changing the zeroth-order coefficient changes the operator by the difference times the function.

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

The operator on the negative.

theorem EllipticPdes.Classical.weak_minimum_principle {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hUne : U.Nonempty) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {θ B : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (huc : ContinuousOn u (closure U)) (hsup : ∀ x ∈ U, 0 ≤ nondivOp a b (fun (x : EuclideanSpace ℝ (Fin d)) => 0) u x) : ∃ y ∈ frontier U, ∀ x ∈ closure U, u y ≤ u x

Weak maximum principle for supersolutions (Evans §6.4.1 Theorem 1(ii)). A supersolution attains its minimum over the closure on the boundary.

theorem EllipticPdes.Classical.weak_maximum_principle_of_nonneg {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hUne : U.Nonempty) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {c : EuclideanSpace ℝ (Fin d) → ℝ} {θ B : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) (hc : ∀ x ∈ U, 0 ≤ c x) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (huc : ContinuousOn u (closure U)) (hsub : ∀ x ∈ U, nondivOp a b c u x ≤ 0) : ∃ y ∈ frontier U, ∀ x ∈ closure U, u x ≤ max (u y) 0

Weak maximum principle with nonnegative zeroth-order coefficient (Evans §6.4.1 Theorem 2(i), Gilbarg and Trudinger Corollary 3.2, Guo Theorem XI.3.7(ii), translated by negating the source operator). With c ≥ 0, a subsolution is bounded on the closure by the maximum of its positive part over the boundary.

Corollaries

theorem EllipticPdes.Classical.not_isLocalMax_of_nondivOp_neg {d : ℕ} {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {c : EuclideanSpace ℝ (Fin d) → ℝ} {x₀ : EuclideanSpace ℝ (Fin d)} (hsymm : ∀ (i j : Fin d), a x₀ i j = a x₀ j i) (hpsd : ∀ (ξ : Fin d → ℝ), 0 ≤ ∑ i : Fin d, ∑ j : Fin d, a x₀ i j * ξ i * ξ j) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffAt ℝ 2 u x₀) (hcu : 0 ≤ c x₀ * u x₀) (hstrict : nondivOp a b c u x₀ < 0) : ¬IsLocalMax u x₀

Strict maximum principle (Guo Theorem XI.3.5). A strict subsolution, meaning L u < 0 at a point, has no local maximum at that point whenever c u ≥ 0 there: in particular when c = 0, when c ≥ 0 and the maximum is nonnegative, and when the maximum is zero.

theorem EllipticPdes.Classical.comparison_principle {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hUne : U.Nonempty) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {c : EuclideanSpace ℝ (Fin d) → ℝ} {θ B : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) (hc : ∀ x ∈ U, 0 ≤ c x) {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, nondivOp a b c u x ≤ nondivOp a b c v x) (hbd : ∀ x ∈ frontier U, u x ≤ v x) (x : EuclideanSpace ℝ (Fin d)) : x ∈ closure U → u x ≤ v x

Comparison principle (Gilbarg and Trudinger Theorem 3.3, Guo Corollary XI.3.11). With c ≥ 0, if L u ≤ L v on the set and u ≤ v on the boundary, then u ≤ v on the closure.

theorem EllipticPdes.Classical.abs_le_of_nondivOp_eq_zero {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hUne : U.Nonempty) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {c : EuclideanSpace ℝ (Fin d) → ℝ} {θ B : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) (hc : ∀ x ∈ U, 0 ≤ c x) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (huc : ContinuousOn u (closure U)) (hsol : ∀ x ∈ U, nondivOp a b c u x = 0) : ∃ y ∈ frontier U, ∀ x ∈ closure U, |u x| ≤ |u y|

Bound by the boundary values (Gilbarg and Trudinger Corollary 3.2, second clause). With c ≥ 0, a solution of L u = 0 on a bounded open set is bounded in absolute value on the closure by the maximum of |u| over the boundary.

theorem EllipticPdes.Classical.weak_minimum_principle_of_nonneg {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hUne : U.Nonempty) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {c : EuclideanSpace ℝ (Fin d) → ℝ} {θ B : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) (hc : ∀ x ∈ U, 0 ≤ c x) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (huc : ContinuousOn u (closure U)) (hsup : ∀ x ∈ U, 0 ≤ nondivOp a b c u x) : ∃ y ∈ frontier U, ∀ x ∈ closure U, min (u y) 0 ≤ u x

Weak minimum principle with nonnegative zeroth-order coefficient (Evans §6.4.1 Theorem 2(ii)). With c ≥ 0, a supersolution is bounded below on the closure by the minimum of its negative part over the boundary.

theorem EllipticPdes.Classical.dirichlet_unique {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hUne : U.Nonempty) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {c : EuclideanSpace ℝ (Fin d) → ℝ} {θ B : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) (hc : ∀ x ∈ U, 0 ≤ c x) {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, nondivOp a b c u x = nondivOp a b c 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 (Guo Corollary XI.3.9). With c ≥ 0, two functions with the same image under L on the set and the same boundary values agree on the closure.