Traces of continuous Sobolev functions

For 1 ≤ p < ∞, the flat, half-space and graph traces of W^{1,p} functions are defined abstractly, as continuous extensions of restriction from test functions. This file proves that they are the classical boundary values whenever the function is continuous up to the boundary.

• TauCeti.W1p.hyperplaneTrace_apply_ae_of_continuous: if u ∈ W^{1,p}(ℝ × E) has a continuous representative f, its trace on {a} × E is y ↦ f (a, y) almost everywhere.
• TauCeti.W1p.halfSpaceTrace_apply_ae_of_continuousOn: if u ∈ W^{1,p} of the half-space {a < t} agrees almost everywhere with a function continuous on the closed half-space {a ≤ t}, its trace is the restriction of that function to {a} × E.
• TauCeti.W1p.normalEpigraphTrace_apply_ae_of_continuousOn: if u ∈ W^{1,p} of the region above the graph of a Lipschitz function φ agrees almost everywhere with a function f continuous on the closed region {φ y ≤ t}, its graph trace is y ↦ f (φ y, y).

For a compactly supported continuous representative, mollification produces test functions converging to u in W^{1,p} and to f pointwise; their traces are their restrictions and converge in Lᵖ, so a subsequence converges almost everywhere and the two limits agree. The general whole-space case follows by multiplying with cutoffs, using that the trace commutes with smooth multipliers. On the half-space, the even reflection extension of a function continuous up to the boundary is continuous; on a graph domain, flattening is a homeomorphism of the closed regions.

Together with density of functions smooth up to the boundary, this identification is what makes traces taken in overlapping boundary charts agree.

References

• L. C. Evans, Partial Differential Equations, 2nd ed., §5.5, Theorem 1 (the trace of a function continuous up to the boundary is its restriction).
• H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, §9.3.

The flat trace

theorem TauCeti.instIsAddHaarMeasureWithLpOfNatENNRealProdRealRestrictVolumeCoeOpensTop_tauCeti {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : (MeasureTheory.volume.restrict ↑⊤).IsAddHaarMeasure

The whole-space restriction of volume is an additive Haar measure.

theorem TauCeti.W1p.hyperplaneTrace_apply_ae_of_continuous {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 ⊤ p)} {f : WithLp 2 (ℝ × E) → ℝ} (hf : Continuous f) (hu : ↑↑(value u) =ᵐ[MeasureTheory.volume] f) : ∀ᵐ (y : E), ↑↑((hyperplaneTrace hp a) u) y = f (WithLp.toLp 2 (a, y))

The flat trace of a continuous Sobolev function is its restriction. If a whole-space W^{1,p} function u is represented almost everywhere by a continuous function f, then its trace on the hyperplane {a} × E is y ↦ f (a, y) almost everywhere.

The half-space trace

theorem TauCeti.W1p.halfSpaceTrace_apply_ae_of_continuousOn {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)} {f : WithLp 2 (ℝ × E) → ℝ} (hf : ContinuousOn f {x : WithLp 2 (ℝ × E) | a ≤ x.fst}) (hu : ↑↑(value u) =ᵐ[MeasureTheory.volume.restrict ↑(normalHalfSpace a)] f) : ∀ᵐ (y : E), ↑↑((halfSpaceTrace hp a) u) y = f (WithLp.toLp 2 (a, y))

The half-space trace of a function continuous up to the boundary is its restriction. If u ∈ W^{1,p} of the half-space {a < t} agrees almost everywhere with a function f continuous on the closed half-space {a ≤ t}, then the trace of u on {a} × E is y ↦ f (a, y) almost everywhere.

The trace on a Lipschitz graph

theorem TauCeti.W1p.normalEpigraphTrace_apply_ae_of_continuousOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {p : ENNReal} [Fact (1 ≤ p)] {φ : C(E, ℝ)} {K : NNReal} (hp : p ≠ ⊤) (hφ : LipschitzWith K ⇑φ) {u : ↥(W1p MeasureTheory.volume (normalEpigraph φ) p)} {f : WithLp 2 (ℝ × E) → ℝ} (hf : ContinuousOn f {x : WithLp 2 (ℝ × E) | φ x.snd ≤ x.fst}) (hu : ↑↑(value u) =ᵐ[MeasureTheory.volume.restrict ↑(normalEpigraph φ)] f) : ∀ᵐ (y : E), ↑↑((normalEpigraphTrace hp hφ) u) y = f (normalGraphEmbedding (⇑φ) y)

The graph trace of a function continuous up to the graph is its restriction. Let φ be Lipschitz and 1 ≤ p < ∞. If u ∈ W^{1,p} of the region {φ y < t} above the graph agrees almost everywhere with a function f continuous on the closed region {φ y ≤ t}, then the trace of u is y ↦ f (φ y, y) almost everywhere.