Partition of unity over a finite cover of the boundary

Guo's third step covers the boundary with finitely many chart neighbourhoods and glues the local extensions with a partition of unity. This file supplies the partition, and bundles it with the cover into the data that step consumes.

Mathlib states its smooth partitions of unity for a manifold, and a normed space is a manifold over itself, so the statement applies here once the smoothness of a bundled map is read back as ContDiff. exists_smooth_partition does that reading, so nothing downstream of this file meets a manifold.

The index of the partition is an Option: the piece indexed none sits inside the domain, away from the boundary, and the piece indexed some x sits in the ball of the chart at the boundary point x. The pieces add to one on the closure of the domain, as the sum of the local extensions requires.

Main declarations

• EllipticPdes.Extension.exists_smooth_partition: a smooth partition of unity subordinate to a finite open cover, stated with ContDiff.
• EllipticPdes.Extension.exists_cutoff_one_on_ball: a smooth cutoff between two balls.
• EllipticPdes.Extension.BoundaryPartition: the cover and the partition together.
• EllipticPdes.Extension.nonempty_boundaryPartition: every bounded domain with C¹ boundary admits one.

References

James Guo, Partial Differential Equations (Course Lecture Notes), Theorem III.2.2 (p. 20), proof step 3 (p. 21); L. C. Evans, Partial Differential Equations (2nd ed.), §5.4 Theorem 1 (p. 253).

theorem EllipticPdes.Extension.exists_smooth_partition {d : ℕ} {ι : Type} [Fintype ι] {s : Set (EuclideanSpace ℝ (Fin d))} (hs : IsClosed s) (U : ι → Set (EuclideanSpace ℝ (Fin d))) (ho : ∀ (i : ι), IsOpen (U i)) (hU : s ⊆ ⋃ (i : ι), U i) : ∃ (ζ : ι → EuclideanSpace ℝ (Fin d) → ℝ), (∀ (i : ι), ContDiff ℝ (↑⊤) (ζ i)) ∧ (∀ (i : ι) (x : EuclideanSpace ℝ (Fin d)), 0 ≤ ζ i x) ∧ (∀ (i : ι), tsupport (ζ i) ⊆ U i) ∧ ∀ x ∈ s, ∑ i : ι, ζ i x = 1

Smooth partition of unity subordinate to a finite open cover, with the smoothness of each piece stated as ContDiff rather than through the manifold structure Mathlib proves it in.

theorem EllipticPdes.Extension.exists_cutoff_one_on_ball {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) {r R : ℝ} (hrR : r < R) : ∃ (ξ : EuclideanSpace ℝ (Fin d) → ℝ), ContDiff ℝ (↑⊤) ξ ∧ (∀ y ∈ Metric.closedBall x r, ξ y = 1) ∧ tsupport ξ ⊆ Metric.ball x R

Smooth cutoff equal to one on a closed ball and supported in a larger one. Guo's third step asks the support of each piece of the partition to sit compactly inside its neighbourhood, and the local extension of step 2 reads the class on a neighbourhood of that support, so a cutoff between two balls is what mediates the two.

structure EllipticPdes.Extension.BoundaryPartition (d : ℕ) (Ω : Set (EuclideanSpace ℝ (Fin d))) : Type

Data Guo's third step glues with. A finite family of boundary charts whose balls cover the boundary, and a smooth partition of unity subordinate to those balls together with the domain itself. The index none is the piece supported inside the domain, away from the boundary; each some x is the piece supported in the ball of the chart at x.

• centres : Finset (EuclideanSpace ℝ (Fin d))

  The boundary points the charts are taken at.

• chart : EuclideanSpace ℝ (Fin d) → C1Chart d

  The chart at each of them.

• part : Option ↥self.centres → EuclideanSpace ℝ (Fin d) → ℝ

  The pieces of the partition.

• centres_mem (x : EuclideanSpace ℝ (Fin d)) : x ∈ self.centres → x ∈ frontier Ω

  Every centre is a boundary point.

• chart_fits (x : EuclideanSpace ℝ (Fin d)) : x ∈ self.centres → (self.chart x).Fits Ω x

  The chart at a centre describes the domain there.

• part_contDiff (i : Option ↥self.centres) : ContDiff ℝ (↑⊤) (self.part i)

  Every piece is smooth.

• part_nonneg (i : Option ↥self.centres) (x : EuclideanSpace ℝ (Fin d)) : 0 ≤ self.part i x

  Every piece is nonnegative.

• part_interior : tsupport (self.part none) ⊆ Ω

  The interior piece is supported inside the domain.

• part_boundary (x : ↥self.centres) : tsupport (self.part (some x)) ⊆ Metric.ball (↑x) (self.chart ↑x).radius

  Each boundary piece is supported in its chart's ball.

• part_sum (x : EuclideanSpace ℝ (Fin d)) : x ∈ closure Ω → ∑ i : Option ↥self.centres, self.part i x = 1

  The pieces add to one on the closure of the domain.

theorem EllipticPdes.Extension.nonempty_boundaryPartition {d : ℕ} (hd : 0 < d) {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩopen : IsOpen Ω) (hΩ : Bornology.IsBounded Ω) (hC1 : HasC1Boundary Ω) : Nonempty (BoundaryPartition d Ω)

Every bounded domain with C¹ boundary admits such a partition.