Weak maximum principle with a transport term

Gilbarg and Trudinger's Theorem 8.1 with the transport term present, in dimension at least two. The transport-free case tests the subsolution inequality against (u - k)⁺ and finds the energy of the truncation nonpositive. With a transport term the energy is bounded by the transport coefficient times the gradient norm of the truncation times its L² norm over the set Γ_k where u > k and the gradient does not vanish. Ellipticity, a Sobolev inequality on H₀¹ at an exponent above 2, which is the critical one in dimension at least three and the embedding into L⁴ in dimension two, and Hölder's inequality then bound the measure of Γ_k below by a constant independent of k, at every level whose superlevel set has positive measure.

The bound is contradicted as k increases to the supremum T of the levels at which the superlevel set has positive measure: the sets Γ_k decrease to a subset of {u ≥ T} on which the gradient does not vanish, and this set is null because {u > T} is null by the choice of T and the gradient vanishes almost everywhere on {u = T}. So no level above the boundary value has a nonzero truncation, which is the conclusion.

The membership of (u - k)⁺ in H₀¹(Ω) for every k above the boundary value comes from the truncation lemma of EllipticPdes.Sobolev.H01Lattice.

Main declarations

• EllipticPdes.Sobolev.weak_maximum_principle_transport: the weak maximum principle with a transport term, in dimension at least two.

References

D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, §8.1 Theorem 8.1 (pp. 179–180).

The set where the truncation has nonvanishing gradient

def EllipticPdes.Sobolev.truncSupport {d : ℕ} (u : EuclideanSpace ℝ (Fin d) → ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (k : ℝ) : Set (EuclideanSpace ℝ (Fin d))

The set where u > k and the gradient does not vanish.

Equations

• EllipticPdes.Sobolev.truncSupport u g k = {x : EuclideanSpace ℝ (Fin d) | k < u x ∧ ∃ (i : Fin d), g i x ≠ 0}

theorem EllipticPdes.Sobolev.measurableSet_truncSupport {d : ℕ} {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : Measurable u) (hg : ∀ (i : Fin d), Measurable (g i)) (k : ℝ) : MeasurableSet (truncSupport u g k)

The set is measurable when the functions are.

theorem EllipticPdes.Sobolev.truncSupport_antitone {d : ℕ} (u : EuclideanSpace ℝ (Fin d) → ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) : Antitone (truncSupport u g)

The set is antitone in the level.

theorem EllipticPdes.Sobolev.truncSupport_subset {d : ℕ} (u : EuclideanSpace ℝ (Fin d) → ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (k : ℝ) : truncSupport u g k ⊆ {x : EuclideanSpace ℝ (Fin d) | k < u x}

The set lies in the superlevel set.

The tail of the argument

theorem EllipticPdes.Sobolev.measure_superlevel_eq_zero {d : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))} [MeasureTheory.IsFiniteMeasure μ] {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : Measurable u) (hg : ∀ (i : Fin d), Measurable (g i)) (hlevel : ∀ (T : ℝ) (i : Fin d), ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂μ, u x = T → g i x = 0) {c : ℝ} (hc : 0 < c) {k₀ : ℝ} (hest : ∀ (k : ℝ), k₀ ≤ k → 0 < μ {x : EuclideanSpace ℝ (Fin d) | k < u x} → c ≤ (μ (truncSupport u g k)).toReal) : μ {x : EuclideanSpace ℝ (Fin d) | k₀ < u x} = 0

Impossibility of a uniform lower bound on the measure of Γ_k. If the measure of Γ_k is at least c > 0 at every level k ≥ k₀ whose superlevel set has positive measure, and the gradient vanishes almost everywhere on every level set, then the superlevel set of k₀ is null.

The truncation at every level above the boundary value

theorem EllipticPdes.Sobolev.max_max_sub_eq {a k₀ k : ℝ} (hk : k₀ ≤ k) : max (max (a - k₀) 0 - (k - k₀)) 0 = max (a - k) 0

Truncating twice is truncating once.

theorem EllipticPdes.Sobolev.ite_lt_max_sub {k₀ k : ℝ} (hk : k₀ ≤ k) (a b : ℝ) : (if k - k₀ < max (a - k₀) 0 then if k₀ < a then b else 0 else 0) = if k < a then b else 0

The indicator of the second truncation is the indicator of {k < a}.

theorem EllipticPdes.Sobolev.exists_truncation_mem_H01 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) {U : H1amb Ω} (hU : U ∈ W12 Ω) {k₀ : ℝ} (V₀ : ↥(H01 Ω)) (hV₀ : ↑↑((↑V₀).ofLp 0) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => max (↑↑(U.ofLp 0) x - k₀) 0) {k : ℝ} (hk : k₀ ≤ k) : ∃ (V : ↥(H01 Ω)), (↑↑((↑V).ofLp 0) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => max (↑↑(U.ofLp 0) x - k) 0) ∧ ∀ (i : Fin d), ↑↑((↑V).ofLp i.succ) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => if k < ↑↑(U.ofLp 0) x then ↑↑(U.ofLp i.succ) x else 0

Truncations at every level above the boundary value in H₀¹. If (u - k₀)⁺ is the function coordinate of an element of H₀¹(Ω), then for every k ≥ k₀ there is an element of H₀¹(Ω) with function coordinate (u - k)⁺ and gradient coordinates those of u on {u > k} and zero elsewhere.

The energy estimate

theorem EllipticPdes.Sobolev.integrable_coeff_mul_mul {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : Measurable f) {M : ℝ} (hM : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, |f x| ≤ M) (p q : L2D Ω) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin d)) => f x * ↑↑p x * ↑↑q x) (MeasureTheory.volume.restrict Ω)

A bounded coefficient times two L² classes is integrable.

theorem EllipticPdes.Sobolev.energy_le_transport {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (Op : FullEllipticOp d) (hc : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), 0 ≤ Op.c x) {U : H1amb Ω} (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) (V : ↥(H01 Ω)) (hV0 : ↑↑((↑V).ofLp 0) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => max (↑↑(U.ofLp 0) x - k) 0) (hVi : ∀ (i : Fin d), ↑↑((↑V).ofLp i.succ) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => if k < ↑↑(U.ofLp 0) x then ↑↑(U.ofLp i.succ) x else 0) : Op.lam * ∑ i : Fin d, ‖(↑V).ofLp i.succ‖ ^ 2 ≤ (Op.Bsup * ∑ i : Fin d, ‖(↑V).ofLp i.succ‖) * (MeasureTheory.eLpNorm (↑↑((↑V).ofLp 0)) 2 ((MeasureTheory.volume.restrict Ω).restrict (truncSupport (fun (x : EuclideanSpace ℝ (Fin d)) => ↑↑(U.ofLp 0) x) (fun (i : Fin d) (x : EuclideanSpace ℝ (Fin d)) => ↑↑(U.ofLp i.succ) x) k))).toReal

Energy estimate from testing with the truncation. For a subsolution U and an element V of H₀¹(Ω) whose coordinates are the truncation (u - k)⁺ and its gradient, ellipticity times the gradient norm squared of V is at most the transport bound times the sum of the gradient norms times the L² norm of the truncation over Γ_k.

The Sobolev-Hölder lower bound

theorem EllipticPdes.Sobolev.exists_measure_truncSupport_ge_of_sobolev {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩb : Bornology.IsBounded Ω) (Op : FullEllipticOp d) {q : NNReal} (hq2 : 2 < q) {C : NNReal} (hsobolev : ∀ (V : ↥(H01 Ω)), MeasureTheory.eLpNorm (↑↑((↑V).ofLp 0)) (↑q) (MeasureTheory.volume.restrict Ω) ≤ ↑C * ∑ i : Fin d, ‖(↑V).ofLp i.succ‖ₑ) : ∃ (c : ℝ), 0 < c ∧ ∀ (V : ↥(H01 Ω)) (u : EuclideanSpace ℝ (Fin d) → ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ), Measurable u → (∀ (i : Fin d), Measurable (g i)) → ∀ (k : ℝ), (↑↑((↑V).ofLp 0) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => max (u x - k) 0) → 0 < (MeasureTheory.volume.restrict Ω) {x : EuclideanSpace ℝ (Fin d) | k < u x} → Op.lam * ∑ i : Fin d, ‖(↑V).ofLp i.succ‖ ^ 2 ≤ (Op.Bsup * ∑ i : Fin d, ‖(↑V).ofLp i.succ‖) * (MeasureTheory.eLpNorm (↑↑((↑V).ofLp 0)) 2 ((MeasureTheory.volume.restrict Ω).restrict (truncSupport u g k))).toReal → c ≤ ((MeasureTheory.volume.restrict Ω) (truncSupport u g k)).toReal

Uniform lower bound on the measure of Γ_k, from a Sobolev inequality on H₀¹(Ω) at an exponent above 2. On a bounded open set there is c > 0, depending on the domain, the dimension, the operator and the Sobolev constant alone, such that, whenever the truncation (u - k)⁺ is the function coordinate of an element V of H₀¹(Ω) whose superlevel set has positive measure and satisfies the energy estimate, the set Γ_k has measure at least c.

theorem EllipticPdes.Sobolev.exists_measure_truncSupport_ge {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hd : 2 < d) (Op : FullEllipticOp d) : ∃ (c : ℝ), 0 < c ∧ ∀ (V : ↥(H01 Ω)) (u : EuclideanSpace ℝ (Fin d) → ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ), Measurable u → (∀ (i : Fin d), Measurable (g i)) → ∀ (k : ℝ), (↑↑((↑V).ofLp 0) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => max (u x - k) 0) → 0 < (MeasureTheory.volume.restrict Ω) {x : EuclideanSpace ℝ (Fin d) | k < u x} → Op.lam * ∑ i : Fin d, ‖(↑V).ofLp i.succ‖ ^ 2 ≤ (Op.Bsup * ∑ i : Fin d, ‖(↑V).ofLp i.succ‖) * (MeasureTheory.eLpNorm (↑↑((↑V).ofLp 0)) 2 ((MeasureTheory.volume.restrict Ω).restrict (truncSupport u g k))).toReal → c ≤ ((MeasureTheory.volume.restrict Ω) (truncSupport u g k)).toReal

Uniform lower bound on the measure of Γ_k in dimension at least three, through the Sobolev inequality at the exponent 2d/(d - 1).

theorem EllipticPdes.Sobolev.exists_measure_truncSupport_ge_two {Ω : Set (EuclideanSpace ℝ (Fin 2))} (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (Op : FullEllipticOp 2) : ∃ (c : ℝ), 0 < c ∧ ∀ (V : ↥(H01 Ω)) (u : EuclideanSpace ℝ (Fin 2) → ℝ) (g : Fin 2 → EuclideanSpace ℝ (Fin 2) → ℝ), Measurable u → (∀ (i : Fin 2), Measurable (g i)) → ∀ (k : ℝ), (↑↑((↑V).ofLp 0) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin 2)) => max (u x - k) 0) → 0 < (MeasureTheory.volume.restrict Ω) {x : EuclideanSpace ℝ (Fin 2) | k < u x} → Op.lam * ∑ i : Fin 2, ‖(↑V).ofLp i.succ‖ ^ 2 ≤ (Op.Bsup * ∑ i : Fin 2, ‖(↑V).ofLp i.succ‖) * (MeasureTheory.eLpNorm (↑↑((↑V).ofLp 0)) 2 ((MeasureTheory.volume.restrict Ω).restrict (truncSupport u g k))).toReal → c ≤ ((MeasureTheory.volume.restrict Ω) (truncSupport u g k)).toReal

Uniform lower bound on the measure of Γ_k in dimension two, through the embedding into L⁴(Ω).

theorem EllipticPdes.Sobolev.exists_measure_truncSupport_ge' {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hd : 2 ≤ d) (Op : FullEllipticOp d) : ∃ (c : ℝ), 0 < c ∧ ∀ (V : ↥(H01 Ω)) (u : EuclideanSpace ℝ (Fin d) → ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ), Measurable u → (∀ (i : Fin d), Measurable (g i)) → ∀ (k : ℝ), (↑↑((↑V).ofLp 0) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => max (u x - k) 0) → 0 < (MeasureTheory.volume.restrict Ω) {x : EuclideanSpace ℝ (Fin d) | k < u x} → Op.lam * ∑ i : Fin d, ‖(↑V).ofLp i.succ‖ ^ 2 ≤ (Op.Bsup * ∑ i : Fin d, ‖(↑V).ofLp i.succ‖) * (MeasureTheory.eLpNorm (↑↑((↑V).ofLp 0)) 2 ((MeasureTheory.volume.restrict Ω).restrict (truncSupport u g k))).toReal → c ≤ ((MeasureTheory.volume.restrict Ω) (truncSupport u g k)).toReal

Uniform lower bound on the measure of Γ_k in dimension at least two.

The weak maximum principle

theorem EllipticPdes.Sobolev.weak_maximum_principle_transport {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hd : 2 ≤ d) (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (Op : FullEllipticOp d) (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 with a transport term (Gilbarg and Trudinger Theorem 8.1, in dimension at least two). Let Ω be a bounded open set in dimension at least two, L a divergence-form operator with bounded 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 Ω.