Partitions of unity adapted to Lipschitz boundary charts

Sobolev trace and extension operators on a bounded Lipschitz domain Ω are assembled from their flat models by a partition of unity: one smooth cutoff supported inside Ω, and one cutoff for each boundary chart of a finite cover. This file constructs such a partition.

Each boundary cutoff is supported, in the coordinates of its chart, in the shortened cylinder normalCylinder (a - 2 * L * b) b, where a and b are the normal and tangential radii of the chart and L is the Lipschitz constant of its graph. On this cylinder the reflection t ↦ 2 * φ y - t across the graph of φ stays inside the chart cylinder, so the reflected values of a cutoff product never reach parts of Ω outside the chart. This is the support hypothesis of the extension through one chart in Evans–Gariepy §4.4.

The charts come from Set.IsLipschitzDomainWith.exists_finset_isLipschitzChartWith_two_mul_lt_cover, and the cutoffs from Mathlib's SmoothPartitionOfUnity.exists_isSubordinate. Every cylinder is bounded, so each cutoff has compact support; its value and gradient are then bounded, as the localization operator TauCeti.W1p.localizeL requires, by ContDiff.exists_abs_le_and_norm_gradient_le.

Main declarations

• Set.IsLipschitzDomainWith.exists_contDiff_partitionOfUnity: a smooth partition of unity on the closure of a bounded Lipschitz domain, subordinate to the domain itself and to the shortened cylinders of finitely many boundary charts.

References

• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised ed., §4.4.
• L. C. Evans, Partial Differential Equations, 2nd ed., §5.4.

theorem Set.IsLipschitzDomainWith.exists_contDiff_partitionOfUnity {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Omega : Set (WithLp 2 (ℝ × E))} {L : NNReal} [FiniteDimensional ℝ E] (h : Omega.IsLipschitzDomainWith L) (hb : Bornology.IsBounded Omega) : ∃ (t : Finset (WithLp 2 (ℝ × E))) (e : WithLp 2 (ℝ × E) → WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (φ : WithLp 2 (ℝ × E) → E → ℝ) (a : WithLp 2 (ℝ × E) → ℝ) (b : WithLp 2 (ℝ × E) → ℝ) (ψ₀ : WithLp 2 (ℝ × E) → ℝ) (ψ : WithLp 2 (ℝ × E) → WithLp 2 (ℝ × E) → ℝ), (∀ x ∈ t, x ∈ frontier Omega ∧ (e x) x = 0 ∧ Omega.IsLipschitzChartWith L (e x) (φ x) (a x) (b x) ∧ 2 * ↑L * b x < a x) ∧ (ContDiff ℝ (↑⊤) ψ₀ ∧ range ψ₀ ⊆ Icc 0 1 ∧ HasCompactSupport ψ₀ ∧ tsupport ψ₀ ⊆ Omega) ∧ (∀ x ∈ t, ContDiff ℝ (↑⊤) (ψ x) ∧ range (ψ x) ⊆ Icc 0 1 ∧ HasCompactSupport (ψ x) ∧ tsupport (ψ x) ⊆ ⇑(e x) ⁻¹' TauCeti.normalCylinder (a x - 2 * ↑L * b x) (b x)) ∧ ∀ y ∈ closure Omega, ψ₀ y + ∑ x ∈ t, ψ x y = 1

Partition of unity for a bounded Lipschitz domain. For a bounded Lipschitz domain Omega with constant L, there are finitely many frontier points x ∈ t carrying Lipschitz boundary charts e x, φ x with radii a x, b x satisfying 2 * L * b x < a x, together with smooth cutoffs ψ₀ and ψ x with values in [0, 1] and compact support, such that ψ₀ is supported in Omega, each ψ x is supported in the preimage of the shortened chart cylinder normalCylinder (a x - 2 * L * b x) (b x), and ψ₀ + ∑ x ∈ t, ψ x = 1 on the closure of Omega.