The kernel of the half-space trace

Let H = TauCeti.normalHalfSpace a = {x | a < x.fst} in the Euclidean product ℝ × E. This file identifies the functions of zero trace on H with the closure of the test functions:

ker (Tr : W^{1,p}(H) → Lᵖ(E)) = W^{1,p}_0(H) for every 1 ≤ p < ∞.

The inclusion W^{1,p}_0(H) ⊆ ker Tr is TauCeti.W1p.halfSpaceTrace_eq_zero_of_w1p0, and TauCeti.W1p.extendByZeroₗᵢ_mem_w1pSubmodule_iff_halfSpaceTrace_eq_zero says that Tr u = 0 exactly when the extension of u by zero is a Sobolev function on ℝ × E. The remaining step, proved here for every 1 ≤ p < ∞, is that a function on H whose extension by zero lies in W^{1,p}(ℝ × E) belongs to W^{1,p}_0(H).

The argument

Let w ∈ W^{1,p}(ℝ × E) vanish off H. For s > 0, translating w by s in the normal direction gives a function vanishing on the layer {x.fst < a + s}. There it is unchanged by the smooth cutoff TauCeti.normalCutoff a (2 / s) of the normal coordinate, which vanishes for x.fst ≤ a + s / 2 and is one for x.fst ≥ a + s. So the translate is a whole-space Sobolev function times a bounded cutoff supported in H, and such functions lie in W^{1,p}_0(H) (TauCeti.W1p.restrictL_contDiffSMul_mem_w1p0Submodule). As s → 0 the translates converge to w in W^{1,p}(ℝ × E) (TauCeti.Wkp.continuous_translate), so the restriction of w to H lies in the closed subspace W^{1,p}_0(H).

Main declarations

• TauCeti.W1p.restrictL_mem_w1p0Submodule_normalHalfSpace: a function in W^{1,p}(ℝ × E) vanishing off H restricts to a function in W^{1,p}_0(H).
• TauCeti.W1p.mem_w1p0Submodule_normalHalfSpace_iff: u ∈ W^{1,p}_0(H) if and only if its extension by zero lies in W^{1,p}(ℝ × E).
• TauCeti.W1p.mem_w1p0Submodule_iff_halfSpaceTrace_eq_zero and TauCeti.W1p.ker_halfSpaceTrace: the kernel of the half-space trace is W^{1,p}_0(H).

References

• L. C. Evans, Partial Differential Equations, §5.5, Theorem 2 (functions of zero trace).
• H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Proposition 9.18 and its proof.

Functions vanishing off the half-space

theorem TauCeti.W1p.restrictL_mem_w1p0Submodule_normalHalfSpace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (a : ℝ) (w : ↥(W1p MeasureTheory.volume ⊤ p)) (hw : ∀ᵐ (x : WithLp 2 (ℝ × E)), x ∉ normalHalfSpace a → ↑↑(value w) x = 0) : (restrictL ⋯) w ∈ w1p0Submodule MeasureTheory.volume (normalHalfSpace a) p

A whole-space Sobolev function vanishing off a half-space has zero boundary values there. If w ∈ W^{1,p}(ℝ × E), 1 ≤ p < ∞, vanishes almost everywhere outside H = {x | a < x.fst}, then its restriction to H lies in W^{1,p}_0(H).

theorem TauCeti.W1p.mem_w1p0Submodule_normalHalfSpace_iff {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)) : u ∈ w1p0Submodule MeasureTheory.volume (normalHalfSpace a) p ↔ (Sobolev1JetLp.extendByZeroₗᵢ ⋯) ↑u ∈ w1pSubmodule MeasureTheory.volume ⊤ p

W^{1,p}_0 of a half-space consists of the functions that extend by zero. For 1 ≤ p < ∞, a function u ∈ W^{1,p}(H) on H = {x | a < x.fst} lies in W^{1,p}_0(H) if and only if its extension by zero, in value and weak gradient, is a Sobolev function on ℝ × E.

@[simp]

theorem TauCeti.W1p.mem_w1p0Submodule_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)) : u ∈ w1p0Submodule MeasureTheory.volume (normalHalfSpace a) p ↔ (halfSpaceTrace hp a) u = 0

The functions of zero trace on a half-space are those of W^{1,p}_0. For 1 ≤ p < ∞, a function u ∈ W^{1,p}(H) on H = {x | a < x.fst} lies in W^{1,p}_0(H) if and only if its trace on the boundary hyperplane {a} × E vanishes.

theorem TauCeti.W1p.ker_halfSpaceTrace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (a : ℝ) : (↑(halfSpaceTrace hp a)).ker = ↑(w1p0Submodule MeasureTheory.volume (normalHalfSpace a) p)

The kernel of the half-space trace is W^{1,p}_0. On H = {x | a < x.fst} and for 1 ≤ p < ∞, the trace W^{1,p}(H) → Lᵖ(E) on the boundary hyperplane {a} × E has kernel exactly W^{1,p}_0(H), the closure of the test functions on H.