Truncation in H₀¹

H₀¹(Ω) is closed under the truncation u ↦ (u - k)⁺ for k ≥ 0. Two steps. A class on the whole space with an L² weak gradient and compact support inside the open set Ω lies in H₀¹(Ω): its mollifications are test functions of Ω once the radius is below the distance from the support to the complement, and they converge to it in H¹ together with their gradients, which are the mollified weak gradient. Then, for V ∈ H₀¹(Ω) approximated by test functions φ_n, the truncations (φ_n - k)⁺ have compact support in Ω because k ≥ 0, have the weak gradient ∇φ_n on {φ_n > k} by the chain rule for the positive part, so lie in H₀¹(Ω) by the first step, and converge in H¹(Ω) to (v - k)⁺ with gradient ∇v on {v > k}: the function coordinates because truncation is 1-Lipschitz, the gradient coordinates along a subsequence converging almost everywhere by dominated convergence, the level set {v = k} giving nothing because the weak gradient vanishes there.

This is the step the proof of the weak maximum principle takes for granted when it tests against (u - k)⁺. With it, the principle applies to every subsolution in H₀¹(Ω), and the uniqueness of the generalised Dirichlet problem follows by applying it to the solution and to its negative.

Main declarations

• EllipticPdes.Sobolev.mem_H01_of_hasCompactSupport: a compactly supported class with L² weak gradient lies in H₀¹.
• EllipticPdes.Sobolev.exists_mem_H01_posPart_sub_const: H₀¹ is closed under u ↦ (u - k)⁺ for k ≥ 0.
• EllipticPdes.Sobolev.weak_maximum_principle_H01: a subsolution in H₀¹ is nonpositive.
• EllipticPdes.Sobolev.eq_zero_of_weakSolution_H01: uniqueness of the generalised Dirichlet problem.

References

D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, §8.1 Theorem 8.1 and Corollary 8.2 (pp. 179–180); L. C. Evans, Partial Differential Equations (2nd ed.), §5.3.1 Theorem 1 (p. 264).

Compactly supported classes lie in H₀¹

theorem EllipticPdes.Sobolev.mem_H01_of_hasCompactSupport {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩ : IsOpen Ω) {w : EuclideanSpace ℝ (Fin d) → ℝ} {h : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hwg : Embedding.HasWeakGradOn Set.univ w h) (hw : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hh : ∀ (k : Fin d), MeasureTheory.MemLp (h k) 2 MeasureTheory.volume) (hwcs : HasCompactSupport w) (hwΩ : tsupport w ⊆ Ω) : WithLp.toLp 2 (Fin.cons (MeasureTheory.MemLp.toLp w ⋯) fun (k : Fin d) => MeasureTheory.MemLp.toLp (h k) ⋯) ∈ H01 Ω

Compactly supported classes with L² weak gradient lie in H₀¹. A class on the whole space with an L² weak gradient whose support is a compact subset of the open set Ω is, with its gradient, the H¹(Ω) limit of its mollifications, which are test functions of Ω.

Truncation

theorem EllipticPdes.Sobolev.abs_max_sub_le (a b k : ℝ) : |max (a - k) 0 - max (b - k) 0| ≤ |a - b|

The truncation t ↦ max (t - k) 0 is 1-Lipschitz.

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

Truncation in H₀¹. For V ∈ H₀¹(Ω) and k ≥ 0 there is W ∈ H₀¹(Ω) whose function coordinate is (v - k)⁺ and whose gradient coordinates are those of V on {v > k} and zero elsewhere.

The maximum principle in H₀¹

theorem EllipticPdes.Sobolev.weak_maximum_principle_H01 {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 : ↥(H01 Ω)) (hsub : ∀ (V : ↥(H01 Ω)), (∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, 0 ≤ ↑↑((↑V).ofLp 0) x) → ((Op.fullBilin Ω) U) V ≤ 0) : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict Ω, ↑↑((↑U).ofLp 0) x ≤ 0

Weak maximum principle for a subsolution in H₀¹. With the boundary inequality u ≤ 0 supplied by membership of the subsolution in H₀¹(Ω), a subsolution of a transport-free operator with nonnegative zeroth-order coefficient on a bounded open set is nonpositive almost everywhere.

theorem EllipticPdes.Sobolev.eq_zero_of_weakSolution_H01 {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 : ↥(H01 Ω)) (hsol : ∀ (V : ↥(H01 Ω)), ((Op.fullBilin Ω) U) V = 0) : U = 0

Uniqueness of the generalised Dirichlet problem (Gilbarg and Trudinger Corollary 8.2, transport-free case). A weak solution in H₀¹(Ω) of the homogeneous equation for a transport-free operator with nonnegative zeroth-order coefficient on a bounded open set is zero.