Smooth partition of unity #

In this file we define two structures, smooth_bump_covering and smooth_partition_of_unity. Both structures describe coverings of a set by a locally finite family of supports of smooth functions with some additional properties. The former structure is mostly useful as an intermediate step in the construction of a smooth partition of unity but some proofs that traditionally deal with a partition of unity can use a smooth_bump_covering as well.

Given a real manifold M and its subset s, a smooth_bump_covering ι I M s is a collection of smooth_bump_functions f i indexed by i : ι such that

• the center of each f i belongs to s;

• the family of sets support (f i) is locally finite;

• for each x ∈ s, there exists i : ι such that f i =ᶠ[𝓝 x] 1. In the same settings, a smooth_partition_of_unity ι I M s is a collection of smooth nonnegative functions f i : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯, i : ι, such that

• the family of sets support (f i) is locally finite;

• for each x ∈ s, the sum ∑ᶠ i, f i x equals one;

• for each x, the sum ∑ᶠ i, f i x is less than or equal to one.

We say that f : smooth_bump_covering ι I M s is subordinate to a map U : M → set M if for each index i, we have closure (support (f i)) ⊆ U (f i).c. This notion is a bit more general than being subordinate to an open covering of M, because we make no assumption about the way U x depends on x.

We prove that on a smooth finitely dimensional real manifold with σ-compact Hausdorff topology, for any U : M → set M such that ∀ x ∈ s, U x ∈ 𝓝 x there exists a smooth_bump_covering ι I M s subordinate to U. Then we use this fact to prove a similar statement about smooth partitions of unity.

Implementation notes #

TODO #

• Build a framework for to transfer local definitions to global using partition of unity and use it to define, e.g., the integral of a differential form over a manifold.

Tags #

smooth bump function, partition of unity

Covering by supports of smooth bump functions #

In this section we define smooth_bump_covering ι I M s to be a collection of smooth_bump_functions such that their supports is a locally finite family of sets and for each x ∈ s some function f i from the collection is equal to 1 in a neighborhood of x. A covering of this type is useful to construct a smooth partition of unity and can be used instead of a partition of unity in some proofs.

We prove that on a smooth finite dimensional real manifold with σ-compact Hausdorff topology, for any U : M → set M such that ∀ x ∈ s, U x ∈ 𝓝 x there exists a smooth_bump_covering ι I M s subordinate to U. Then we use this fact to prove a version of the Whitney embedding theorem: any compact real manifold can be embedded into ℝ^n for large enough n.