Localization of the flat Sobolev trace

For 1 ≤ p < ∞, the trace of a smooth bounded multiplier times a W^{1,p} function is the boundary restriction of the multiplier times the trace. This holds for both the whole-space hyperplane trace and the one-sided half-space trace. In particular, equality of Sobolev values wherever a multiplier is nonzero implies equality of their traces wherever it is nonzero on the boundary.

These identities allow local boundary traces to be patched with a partition of unity: localizing before taking the trace agrees with localizing the boundary data. Bounds on both the cutoff and its gradient are explicit. Compact support is not required.

References

• L. C. Evans, Partial Differential Equations, 2nd ed., §5.5, Theorem 1 (trace theorem background).
• TauCeti.Analysis.Sobolev.Trace.Extension: flat Sobolev traces.
• TauCeti.Analysis.Sobolev.W1p.Multiplication: bounded smooth multiplication.
• Mathlib's ContinuousLinearMap.holderL: L∞ × Lᵖ → Lᵖ multiplication.

theorem TauCeti.W1p.hyperplaneTrace_contDiffSMul_ae {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ψ : WithLp 2 (ℝ × E) → ℝ} {M : ℝ} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (a : ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hψM : ∀ (x : WithLp 2 (ℝ × E)), |ψ x| ≤ M) (hgradM : ∀ (x : WithLp 2 (ℝ × E)), ‖_root_.gradient ψ x‖ ≤ M) (u : ↥(W1p MeasureTheory.volume ⊤ p)) : ∀ᵐ (y : E), ↑↑((hyperplaneTrace hp a) (contDiffSMul ψ hψ ⋯ ⋯ ⋯ u)) y = ψ (WithLp.toLp 2 (a, y)) * ↑↑((hyperplaneTrace hp a) u) y

The whole-space W^{1,p} trace commutes with multiplication by a smooth function whose value and gradient are bounded. The multiplier on the boundary is its classical restriction to the hyperplane.

theorem TauCeti.W1p.halfSpaceTrace_contDiffSMul_ae {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ψ : WithLp 2 (ℝ × E) → ℝ} {M : ℝ} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (a : ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hψM : ∀ (x : WithLp 2 (ℝ × E)), |ψ x| ≤ M) (hgradM : ∀ (x : WithLp 2 (ℝ × E)), ‖_root_.gradient ψ x‖ ≤ M) (u : ↥(W1p MeasureTheory.volume (normalHalfSpace a) p)) : ∀ᵐ (y : E), ↑↑((halfSpaceTrace hp a) (contDiffSMul ψ hψ ⋯ ⋯ ⋯ u)) y = ψ (WithLp.toLp 2 (a, y)) * ↑↑((halfSpaceTrace hp a) u) y

The one-sided W^{1,p} trace commutes with smooth bounded multiplication. No symmetry of the multiplier across the boundary is assumed.

theorem TauCeti.W1p.halfSpaceTrace_ae_eq_on_of_value_ae_eq_on {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ψ : WithLp 2 (ℝ × E) → ℝ} {M : ℝ} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (a : ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hψM : ∀ (x : WithLp 2 (ℝ × E)), |ψ x| ≤ M) (hgradM : ∀ (x : WithLp 2 (ℝ × E)), ‖_root_.gradient ψ x‖ ≤ M) {u v : ↥(W1p MeasureTheory.volume (normalHalfSpace a) p)} (huv : ∀ᵐ (x : WithLp 2 (ℝ × E)) ∂MeasureTheory.volume.restrict ↑(normalHalfSpace a), ψ x ≠ 0 → ↑↑(value u) x = ↑↑(value v) x) : ∀ᵐ (y : E), ψ (WithLp.toLp 2 (a, y)) ≠ 0 → ↑↑((halfSpaceTrace hp a) u) y = ↑↑((halfSpaceTrace hp a) v) y

Half-space Sobolev functions agreeing almost everywhere wherever a smooth bounded multiplier is nonzero have equal traces almost everywhere wherever its boundary restriction is nonzero. This is the local agreement needed when gluing boundary charts.