Integration by parts on a half-space, and functions of zero trace

Let H = TauCeti.normalHalfSpace a = {x | a < x.fst} in the Euclidean product ℝ × E, with boundary hyperplane {a} × E and outward unit normal -e₁. This file proves the Gauss–Green formula on H for Sobolev functions, with the trace TauCeti.W1p.halfSpaceTrace as the boundary term: for u ∈ W^{1,p}(H) with 1 ≤ p < ∞, a compactly supported C¹ function χ on ℝ × E, and a direction v,

∫_H (∂_v χ · u + χ · ⟪v, ∇u⟫) = -v.fst ∫_E (Tr u)(y) χ(a, y) dy.

For u the restriction of a test function this is the classical divergence theorem on H, and the trace is the boundary value that makes the formula persist on all of W^{1,p}(H). Both sides are continuous in u: the fixed factors built from χ lie in Lᵠ for the conjugate exponent q = ENNReal.conjExponent p, so the integrals are Lᵖ–Lᵠ pairings. No finite-volume assumption is needed, and at p = 1 the conjugate exponent is ∞.

The boundary term is exactly what obstructs extending u by zero. Extending u and ∇u by zero to ℝ × E, the left-hand side is the pairing that tests whether the extended gradient is the weak gradient of the extended function; the right-hand side is the defect, a distribution supported on the boundary {a} × E. So the extension by zero of u lies in W^{1,p}(ℝ × E) if and only if Tr u = 0. This is the analytic half of the identification of the kernel of the trace with W^{1,p}_0(H): membership of the zero extension in W^{1,p}(ℝ × E) is the characterisation of W^{1,p}_0 used for domains with regular boundary.

Main declarations

• TauCeti.setIntegral_normalHalfSpace_fderiv_apply: the divergence theorem on H for compactly supported C¹ functions.
• TauCeti.W1p.setIntegral_fderiv_mul_value_add_mul_inner_gradient: the Gauss–Green formula on H for u ∈ W^{1,p}(H), with the trace as boundary term.
• TauCeti.W1p.extendByZeroₗᵢ_mem_w1pSubmodule_iff_halfSpaceTrace_eq_zero: the extension by zero of u ∈ W^{1,p}(H) is a Sobolev function on ℝ × E if and only if the trace of u vanishes.

References

• L. C. Evans, Partial Differential Equations, §5.5 (traces) and Appendix C.2 (the Gauss–Green theorem).
• H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Proposition 9.18.

The smooth divergence theorem on a half-space

theorem TauCeti.setIntegral_normalHalfSpace_fderiv_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {g : WithLp 2 (ℝ × E) → ℝ} (hg : ContDiff ℝ 1 g) (hgc : HasCompactSupport g) (a : ℝ) (v : WithLp 2 (ℝ × E)) : ∫ (x : WithLp 2 (ℝ × E)) in ↑(normalHalfSpace a), (fderiv ℝ g x) v = -(v.fst * ∫ (y : E), g (WithLp.toLp 2 (a, y)))

The divergence theorem on a half-space. For a compactly supported C¹ function g on ℝ × E and a direction v, the integral of the directional derivative ∂_v g over the half-space {x | a < x.fst} is the boundary integral of g over {a} × E, weighted by ⟪v, -e₁⟫ = -v.fst, the normal component of v along the outward unit normal.

Integration by parts against the trace

theorem TauCeti.W1p.setIntegral_fderiv_mul_value_add_mul_inner_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (a : ℝ) (u : ↥(W1p MeasureTheory.volume (normalHalfSpace a) p)) {χ : WithLp 2 (ℝ × E) → ℝ} (hχ : ContDiff ℝ 1 χ) (hχc : HasCompactSupport χ) (v : WithLp 2 (ℝ × E)) : ∫ (x : WithLp 2 (ℝ × E)) in ↑(normalHalfSpace a), (fderiv ℝ χ x) v * ↑↑(value u) x + χ x * inner ℝ v (↑↑(gradient u) x) = -(v.fst * ∫ (y : E), ↑↑((halfSpaceTrace hp a) u) y * χ (WithLp.toLp 2 (a, y)))

Integration by parts on a half-space, with the trace as boundary term. Let H = {x | a < x.fst}, let 1 ≤ p < ∞ and let u ∈ W^{1,p}(H). For every compactly supported C¹ function χ on the whole space ℝ × E and every direction v,

∫_H (∂_v χ · u + χ · ⟪v, ∇u⟫) = -v₁ ∫_E (Tr u)(y) χ(a, y) dy,

where Tr u = TauCeti.W1p.halfSpaceTrace hp a u and v₁ = v.fst is the normal component of v. The outward unit normal of H is -e₁, so this is the Gauss–Green formula ∫_H ∂_v(χ u) = ∫_{∂H} χ u ⟪v, ν⟫ for Sobolev functions. Tangential directions produce no boundary term.

Functions of zero trace

theorem TauCeti.W1p.extendByZeroₗᵢ_mem_w1pSubmodule_iff_halfSpaceTrace_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (a : ℝ) (u : ↥(W1p MeasureTheory.volume (normalHalfSpace a) p)) : (Sobolev1JetLp.extendByZeroₗᵢ ⋯) ↑u ∈ w1pSubmodule MeasureTheory.volume ⊤ p ↔ (halfSpaceTrace hp a) u = 0

The functions of zero trace on a half-space are those that extend by zero. Let 1 ≤ p < ∞ and u ∈ W^{1,p}(H) on the half-space H = {x | a < x.fst}. Its extension by zero is weakly differentiable on the whole space, that is, lies in W^{1,p}(ℝ × E) with weak gradient the extension by zero of ∇u, if and only if the trace of u on {a} × E vanishes.