Sobolev localization in Lipschitz boundary charts

W1p.lipschitzChartLocalizeL cuts off a Sobolev function, extends it by zero past the artificial chart boundary, and transports it to the whole epigraph of the chart graph. Its norm is at most 2 M, for every 1 ≤ p ≤ ∞; it preserves zero boundary values for finite exponents. This is the common localization step for chart trace and reflection extension operators. The support need only lie in the original chart cylinder.

References

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

noncomputable def TauCeti.W1p.lipschitzChartLocalizeL {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : TopologicalSpace.Opens (WithLp 2 (ℝ × E))} {L : NNReal} {e : WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b M : ℝ} {p : ENNReal} [Fact (1 ≤ p)] (h : (↑Ω).IsLipschitzChartWith L e φ a b) (ψ : WithLp 2 (ℝ × E) → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hM : 0 ≤ M) (hψM : ∀ x ∈ Ω, |ψ x| ≤ M) (hgM : ∀ x ∈ Ω, ‖_root_.gradient ψ x‖ ≤ M) (hs : tsupport ψ ⊆ ⇑e ⁻¹' normalCylinder a b) : ↥(W1p MeasureTheory.volume Ω p) →L[ℝ] ↥(W1p MeasureTheory.volume (normalEpigraph { toFun := φ, continuous_toFun := ⋯ }) p)

Cut off a Sobolev function inside a Lipschitz boundary chart, extend by zero along the artificial chart boundary, and express it in the rigid chart coordinates. The resulting function is defined on the whole epigraph of the chart graph.

theorem TauCeti.W1p.lipschitzChartLocalizeL_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : TopologicalSpace.Opens (WithLp 2 (ℝ × E))} {L : NNReal} {e : WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} {ψ : WithLp 2 (ℝ × E) → ℝ} {M : ℝ} {p : ENNReal} [Fact (1 ≤ p)] (h : (↑Ω).IsLipschitzChartWith L e φ a b) (hψ : ContDiff ℝ (↑⊤) ψ) (hM : 0 ≤ M) (hψM : ∀ x ∈ Ω, |ψ x| ≤ M) (hgM : ∀ x ∈ Ω, ‖_root_.gradient ψ x‖ ≤ M) (hs : tsupport ψ ⊆ ⇑e ⁻¹' normalCylinder a b) (u : ↥(W1p MeasureTheory.volume Ω p)) : let V := chartEpigraph e ⋯; (lipschitzChartLocalizeL h ψ hψ hM hψM hgM hs) u = (compAffineIsometryEquivL e.symm ⋯) ((localizeL ⋯ ψ hψ hM ⋯ ⋯ ⋯) ((restrictL ⋯) u))

Chart localization is restriction, localization on the chart epigraph, and rigid transport.

theorem TauCeti.W1p.value_lipschitzChartLocalizeL_ae {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : TopologicalSpace.Opens (WithLp 2 (ℝ × E))} {L : NNReal} {e : WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} {ψ : WithLp 2 (ℝ × E) → ℝ} {M : ℝ} {p : ENNReal} [Fact (1 ≤ p)] (h : (↑Ω).IsLipschitzChartWith L e φ a b) (hψ : ContDiff ℝ (↑⊤) ψ) (hM : 0 ≤ M) (hψM : ∀ x ∈ Ω, |ψ x| ≤ M) (hgM : ∀ x ∈ Ω, ‖_root_.gradient ψ x‖ ≤ M) (hs : tsupport ψ ⊆ ⇑e ⁻¹' normalCylinder a b) (u : ↥(W1p MeasureTheory.volume Ω p)) : ↑↑(value ((lipschitzChartLocalizeL h ψ hψ hM hψM hgM hs) u)) =ᵐ[MeasureTheory.volume.restrict ↑(normalEpigraph { toFun := φ, continuous_toFun := ⋯ })] fun (z : WithLp 2 (ℝ × E)) => (↑Ω).indicator (fun (x : WithLp 2 (ℝ × E)) => ψ x • ↑↑(value u) x) (e.symm z)

In chart coordinates, localization is the cutoff product, set to zero outside the original domain. This formula characterizes the localized Sobolev function by its value.

theorem TauCeti.W1p.norm_lipschitzChartLocalizeL_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : TopologicalSpace.Opens (WithLp 2 (ℝ × E))} {L : NNReal} {e : WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} {ψ : WithLp 2 (ℝ × E) → ℝ} {M : ℝ} {p : ENNReal} [Fact (1 ≤ p)] (h : (↑Ω).IsLipschitzChartWith L e φ a b) (hψ : ContDiff ℝ (↑⊤) ψ) (hM : 0 ≤ M) (hψM : ∀ x ∈ Ω, |ψ x| ≤ M) (hgM : ∀ x ∈ Ω, ‖_root_.gradient ψ x‖ ≤ M) (hs : tsupport ψ ⊆ ⇑e ⁻¹' normalCylinder a b) (u : ↥(W1p MeasureTheory.volume Ω p)) : ‖(lipschitzChartLocalizeL h ψ hψ hM hψM hgM hs) u‖ ≤ 2 * M * ‖u‖

Chart localization multiplies the Sobolev norm by at most 2 M, independently of the Lipschitz constant of the graph.

theorem TauCeti.W1p.lipschitzChartLocalizeL_mem_w1p0Submodule {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : TopologicalSpace.Opens (WithLp 2 (ℝ × E))} {L : NNReal} {e : WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} {ψ : WithLp 2 (ℝ × E) → ℝ} {M : ℝ} {p : ENNReal} [Fact (1 ≤ p)] (h : (↑Ω).IsLipschitzChartWith L e φ a b) (hψ : ContDiff ℝ (↑⊤) ψ) (hM : 0 ≤ M) (hψM : ∀ x ∈ Ω, |ψ x| ≤ M) (hgM : ∀ x ∈ Ω, ‖_root_.gradient ψ x‖ ≤ M) (hs : tsupport ψ ⊆ ⇑e ⁻¹' normalCylinder a b) {u : ↥(W1p MeasureTheory.volume Ω p)} (hu : u ∈ w1p0Submodule MeasureTheory.volume Ω p) : (lipschitzChartLocalizeL h ψ hψ hM hψM hgM hs) u ∈ w1p0Submodule MeasureTheory.volume (normalEpigraph { toFun := φ, continuous_toFun := ⋯ }) p

Chart localization preserves zero boundary values.