Local Sobolev traces and surface measure

For 1 ≤ p < ∞, the localized Sobolev trace in a Lipschitz boundary chart is constructed as an Lᵖ function on the tangential parameter space. Surface measure on the chart graph and tangential Lebesgue measure have the same null sets. Consequently, the chart trace can also be read almost everywhere on the frontier by evaluating it at the tangential coordinate of each boundary point.

For a Sobolev function represented by a function continuous up to the boundary, this surface-measure interpretation agrees almost everywhere with the classical boundary value of the localized function. This is the compatibility needed to patch the local chart traces into a global trace on the frontier.

Main declaration

• TauCeti.W1p.lipschitzChartTrace_comp_snd_ae_of_continuousOn: the localized chart trace of a continuous Sobolev representative agrees with its classical value almost everywhere for normalized Euclidean Hausdorff measure on the frontier patch.

References

• L. C. Evans, Partial Differential Equations, 2nd ed., §5.5, Theorem 1.
• J. Nečas, Direct Methods in the Theory of Elliptic Equations, Chapter 2.

theorem TauCeti.W1p.lipschitzChartTrace_comp_snd_ae_of_continuousOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Omega : TopologicalSpace.Opens (WithLp 2 (ℝ × E))} {L : NNReal} {e : WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {phi : E → ℝ} {a b : ℝ} {psi : WithLp 2 (ℝ × E) → ℝ} {M : ℝ} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (h : (↑Omega).IsLipschitzChartWith L e phi a b) (hpsi : ContDiff ℝ (↑⊤) psi) (hM : 0 ≤ M) (hpsiM : ∀ x ∈ Omega, |psi x| ≤ M) (hgM : ∀ x ∈ Omega, ‖_root_.gradient psi x‖ ≤ M) (hs : tsupport psi ⊆ ⇑e ⁻¹' normalCylinder a b) {u : ↥(W1p MeasureTheory.volume Omega p)} {f : WithLp 2 (ℝ × E) → ℝ} (hf : ContinuousOn f (closure ↑Omega)) (hu : ↑↑(value u) =ᵐ[MeasureTheory.volume.restrict ↑Omega] f) : ∀ᵐ (x : WithLp 2 (ℝ × E)) ∂(MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)).restrict (frontier ↑Omega ∩ ⇑e ⁻¹' normalCylinder a b), ↑↑((lipschitzChartTrace hp h psi hpsi hM hpsiM hgM hs) u) (e x).snd = psi x * f x

The local trace agrees with classical boundary values in surface measure. Let 1 ≤ p < ∞. If u ∈ W^{1,p}(Ω) agrees almost everywhere with a function f continuous on closure Ω, then the localized trace through a Lipschitz boundary chart, read at the tangential coordinate of a boundary point, equals ψ * f almost everywhere on the part of the frontier in that chart.