Functions of zero trace on a Lipschitz domain

Let Ω ⊆ ℝ × E be open and 1 ≤ p < ∞. Functions in W^{1,p}_0(Ω) have zero local trace in every Lipschitz boundary chart (TauCeti.W1p.lipschitzChartTrace_eq_zero_of_mem_w1p0Submodule). This file proves the converse: zero local traces in the charts of a partition of unity force zero boundary values.

The key step is local. If the trace of u ∈ W^{1,p}(Ω) through one chart, localized by a cutoff ψ, vanishes, then ψ u ∈ W^{1,p}_0(Ω). In chart coordinates the localized function lies above a Lipschitz graph and has zero graph trace, so it lies in W^{1,p}_0 of the epigraph (TauCeti.W1p.mem_w1p0Submodule_iff_normalEpigraphTrace_eq_zero). A second cutoff, equal to one near the support of ψ and supported in the chart cylinder, carries it back to W^{1,p}_0(Ω), because Ω and the epigraph agree inside the cylinder. Writing u = ψ₀ u + ∑ ψᵢ u with ψ₀ compactly supported in Ω then gives u ∈ W^{1,p}_0(Ω) whenever every chart trace vanishes.

Every bounded Lipschitz domain carries such a partition of unity (Set.IsLipschitzDomainWith.exists_contDiff_partitionOfUnity). Hence on a bounded Lipschitz domain, W^{1,p}_0(Ω) is the common kernel of finitely many local chart traces W^{1,p}(Ω) → Lᵖ(E). These traces are measured by tangential Lebesgue measure in each chart; no surface measure on frontier Ω is involved. TauCeti.W1p.ker_frontierTrace deduces that W^{1,p}_0(Ω) is the kernel of the trace into Lᵖ of surface measure on the frontier.

Main declarations

• TauCeti.W1p.contDiffSMul_mem_w1p0Submodule_of_lipschitzChartTrace_eq_zero: a cutoff product with zero local chart trace lies in W^{1,p}_0(Ω).
• TauCeti.W1p.mem_w1p0Submodule_iff_forall_lipschitzChartTrace_eq_zero and TauCeti.W1p.iInf_ker_lipschitzChartTrace: for the charts of a partition of unity, W^{1,p}_0(Ω) is the common kernel of the local traces.
• TauCeti.W1p.exists_iInf_ker_lipschitzChartTrace_eq_of_isLipschitzDomainWith: on a bounded Lipschitz domain, W^{1,p}_0(Ω) is the common kernel of finitely many local chart traces.

References

• L. C. Evans, Partial Differential Equations, 2nd ed., §5.5, Theorem 2.
• J. Nečas, Direct Methods in the Theory of Elliptic Equations, Chapter 2 (traces on Lipschitz domains by local flattening).

theorem TauCeti.W1p.contDiffSMul_mem_w1p0Submodule_of_lipschitzChartTrace_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : TopologicalSpace.Opens (WithLp 2 (ℝ × E))} {p : ENNReal} [Fact (1 ≤ p)] {L : NNReal} {e : WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} {ψ : WithLp 2 (ℝ × E) → ℝ} {M : ℝ} (hp : 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 : (lipschitzChartTrace hp h ψ hψ hM hψM hgM hs) u = 0) : contDiffSMul ψ hψ hM hψM hgM u ∈ w1p0Submodule MeasureTheory.volume Ω p

Zero local trace gives zero boundary values. Let 1 ≤ p < ∞. If the trace of u ∈ W^{1,p}(Ω) through a Lipschitz boundary chart, localized by the cutoff ψ, vanishes, then ψ u ∈ W^{1,p}_0(Ω).

theorem TauCeti.W1p.mem_w1p0Submodule_iff_forall_lipschitzChartTrace_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : TopologicalSpace.Opens (WithLp 2 (ℝ × E))} {p : ENNReal} [Fact (1 ≤ p)] {ι : Type u_2} [Fintype ι] {L : ι → NNReal} {e : ι → WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : ι → E → ℝ} {a b : ι → ℝ} {ψ₀ : WithLp 2 (ℝ × E) → ℝ} {ψ : ι → WithLp 2 (ℝ × E) → ℝ} {M : ι → ℝ} (hp : p ≠ ⊤) (h : ∀ (i : ι), (↑Ω).IsLipschitzChartWith (L i) (e i) (φ i) (a i) (b i)) (hψ₀ : ContDiff ℝ (↑⊤) ψ₀) (hψ₀c : HasCompactSupport ψ₀) (hψ₀Ω : tsupport ψ₀ ⊆ ↑Ω) (hψ : ∀ (i : ι), ContDiff ℝ (↑⊤) (ψ i)) (hM : ∀ (i : ι), 0 ≤ M i) (hψM : ∀ (i : ι), ∀ x ∈ Ω, |ψ i x| ≤ M i) (hgM : ∀ (i : ι), ∀ x ∈ Ω, ‖_root_.gradient (ψ i) x‖ ≤ M i) (hs : ∀ (i : ι), tsupport (ψ i) ⊆ ⇑(e i) ⁻¹' normalCylinder (a i) (b i)) (hsum : ∀ x ∈ Ω, ψ₀ x + ∑ i : ι, ψ i x = 1) (u : ↥(W1p MeasureTheory.volume Ω p)) : u ∈ w1p0Submodule MeasureTheory.volume Ω p ↔ ∀ (i : ι), (lipschitzChartTrace hp ⋯ (ψ i) ⋯ ⋯ ⋯ ⋯ ⋯) u = 0

The functions of zero trace on a chart-covered domain are those of W^{1,p}_0. Let 1 ≤ p < ∞, let ψ₀ be a smooth cutoff compactly supported in Ω, and let each ψ i be supported in the cylinder of a Lipschitz boundary chart, with ψ₀ + ∑ i, ψ i = 1 on Ω. Then u ∈ W^{1,p}(Ω) lies in W^{1,p}_0(Ω) if and only if all of its local chart traces vanish.

theorem TauCeti.W1p.iInf_ker_lipschitzChartTrace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : TopologicalSpace.Opens (WithLp 2 (ℝ × E))} {p : ENNReal} [Fact (1 ≤ p)] {ι : Type u_2} [Fintype ι] {L : ι → NNReal} {e : ι → WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : ι → E → ℝ} {a b : ι → ℝ} {ψ₀ : WithLp 2 (ℝ × E) → ℝ} {ψ : ι → WithLp 2 (ℝ × E) → ℝ} {M : ι → ℝ} (hp : p ≠ ⊤) (h : ∀ (i : ι), (↑Ω).IsLipschitzChartWith (L i) (e i) (φ i) (a i) (b i)) (hψ₀ : ContDiff ℝ (↑⊤) ψ₀) (hψ₀c : HasCompactSupport ψ₀) (hψ₀Ω : tsupport ψ₀ ⊆ ↑Ω) (hψ : ∀ (i : ι), ContDiff ℝ (↑⊤) (ψ i)) (hM : ∀ (i : ι), 0 ≤ M i) (hψM : ∀ (i : ι), ∀ x ∈ Ω, |ψ i x| ≤ M i) (hgM : ∀ (i : ι), ∀ x ∈ Ω, ‖_root_.gradient (ψ i) x‖ ≤ M i) (hs : ∀ (i : ι), tsupport (ψ i) ⊆ ⇑(e i) ⁻¹' normalCylinder (a i) (b i)) (hsum : ∀ x ∈ Ω, ψ₀ x + ∑ i : ι, ψ i x = 1) : ⨅ (i : ι), (↑(lipschitzChartTrace hp ⋯ (ψ i) ⋯ ⋯ ⋯ ⋯ ⋯)).ker = ↑(w1p0Submodule MeasureTheory.volume Ω p)

The common kernel of the local traces is W^{1,p}_0. For 1 ≤ p < ∞ and the charts of a partition of unity as in TauCeti.W1p.mem_w1p0Submodule_iff_forall_lipschitzChartTrace_eq_zero, the local traces W^{1,p}(Ω) → Lᵖ(E) vanish simultaneously exactly on W^{1,p}_0(Ω).

theorem TauCeti.W1p.exists_iInf_ker_lipschitzChartTrace_eq_of_isLipschitzDomainWith {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : TopologicalSpace.Opens (WithLp 2 (ℝ × E))} {L : NNReal} (hΩ : (↑Ω).IsLipschitzDomainWith L) (hb : Bornology.IsBounded ↑Ω) : ∃ (t : Finset (WithLp 2 (ℝ × E))) (e : ↥t → WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (φ : ↥t → E → ℝ) (a : ↥t → ℝ) (b : ↥t → ℝ) (h : ∀ (i : ↥t), (↑Ω).IsLipschitzChartWith L (e i) (φ i) (a i) (b i)) (ψ : ↥t → WithLp 2 (ℝ × E) → ℝ) (hψ : ∀ (i : ↥t), ContDiff ℝ (↑⊤) (ψ i)) (M : ↥t → ℝ) (hM : ∀ (i : ↥t), 0 ≤ M i) (hψM : ∀ (i : ↥t), ∀ x ∈ Ω, |ψ i x| ≤ M i) (hgM : ∀ (i : ↥t), ∀ x ∈ Ω, ‖_root_.gradient (ψ i) x‖ ≤ M i) (hs : ∀ (i : ↥t), tsupport (ψ i) ⊆ ⇑(e i) ⁻¹' normalCylinder (a i) (b i)), ∀ (q : ENNReal) [inst : Fact (1 ≤ q)] (hq : q ≠ ⊤), ⨅ (i : ↥t), (↑(lipschitzChartTrace hq ⋯ (ψ i) ⋯ ⋯ ⋯ ⋯ ⋯)).ker = ↑(w1p0Submodule MeasureTheory.volume Ω q)

Zero trace on a bounded Lipschitz domain. A bounded Lipschitz domain has finitely many boundary charts with cutoffs such that, for every 1 ≤ p < ∞, the local traces W^{1,p}(Ω) → Lᵖ(E) vanish simultaneously exactly on W^{1,p}_0(Ω).