Weak maximum principle

A weak subsolution of a transport-free divergence-form equation with nonnegative zeroth-order coefficient is bounded above by its boundary values. The boundary inequality u ≤ k on ∂Ω for a Sobolev class is read, following Gilbarg and Trudinger, as membership of (u - k)⁺ in H₀¹(Ω), and the conclusion is u ≤ k almost everywhere for every k ≥ 0 with that property, which is the inequality sup_Ω u ≤ sup_∂Ω u⁺ between the essential supremum and the infimum of such k.

The proof is the transport-free case the source singles out. Testing the subsolution inequality against v = (u - k)⁺, the zeroth-order term is nonnegative because u v ≥ 0, so the principal term is nonpositive. The weak gradient of v is the gradient of u where u > k and zero elsewhere, so the principal term is the energy of v itself, which ellipticity bounds below by the gradient norm. The gradient of v therefore vanishes, and the Poincaré inequality on H₀¹ of a bounded domain makes v vanish.

The subsolution inequality is taken against every nonnegative element of H₀¹(Ω), which is the form the source uses in the proof, having extended the inequality from C¹ test functions by density.

Main declarations

• EllipticPdes.Sobolev.weak_maximum_principle: the weak maximum principle for a transport-free operator with nonnegative zeroth-order coefficient.

References

D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, §8.1 Theorem 8.1 (p. 179); L. C. Evans, Partial Differential Equations (2nd ed.), §6.4.1 Theorem 2 (p. 346).

theorem EllipticPdes.Sobolev.weak_maximum_principle {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hd : 0 < d) (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (Op : FullEllipticOp d) (hb : ∀ (x : EuclideanSpace ℝ (Fin d)) (i : Fin d), Op.b x i = 0) (hc : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), 0 ≤ Op.c x) {U : H1amb Ω} (hU : U ∈ W12 Ω) (hsub : ∀ (V : ↥(H01 Ω)), (∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, 0 ≤ ↑↑((↑V).ofLp 0) x) → ∑ i : Fin d, ∑ j : Fin d, inner ℝ ((Op.actL i j) (U.ofLp i.succ)) ((↑V).ofLp j.succ) + ∑ i : Fin d, inner ℝ ((Op.bAct i) (U.ofLp i.succ)) ((↑V).ofLp 0) + inner ℝ (Op.cAct (U.ofLp 0)) ((↑V).ofLp 0) ≤ 0) {k : ℝ} (hk : 0 ≤ k) (hbd : ∃ (V : ↥(H01 Ω)), ↑↑((↑V).ofLp 0) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => max (↑↑(U.ofLp 0) x - k) 0) : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, ↑↑(U.ofLp 0) x ≤ k

Weak maximum principle (Gilbarg and Trudinger Theorem 8.1, in the transport-free case). Let Ω be a bounded open set, L a divergence-form operator with no transport term and nonnegative zeroth-order coefficient, and U ∈ H¹(Ω) a weak subsolution, meaning the bilinear pairing of U against every nonnegative V ∈ H₀¹(Ω) is nonpositive. If k ≥ 0 and (u - k)⁺ is the function coordinate of some element of H₀¹(Ω), then u ≤ k almost everywhere on Ω.