Smooth partition of unity #
In this file we define two structures, SmoothBumpCovering and SmoothPartitionOfUnity. 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 SmoothBumpCovering as well.
Given a real manifold M and its subset s, a SmoothBumpCovering ι I M s is a collection of
SmoothBumpFunctions f i indexed by i : ι such that
the center of each
f ibelongs tos;the family of sets
support (f i)is locally finite;for each
x ∈ s, there existsi : ιsuch thatf i =ᶠ[𝓝 x] 1. In the same settings, aSmoothPartitionOfUnity ι I M sis a collection of smooth nonnegative functionsf i : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯,i : ι, such thatthe family of sets
support (f i)is locally finite;for each
x ∈ s, the sum∑ᶠ i, f i xequals one;for each
x, the sum∑ᶠ i, f i xis less than or equal to one.
We say that f : SmoothBumpCovering ι I M s is subordinate to a map U : M → Set M if for each
index i, we have tsupport (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 SmoothBumpCovering ι I M s
subordinate to U. Then we use this fact to prove a similar statement about smooth partitions of
unity, see SmoothPartitionOfUnity.exists_isSubordinate.
Finally, we use existence of a partition of unity to prove lemma
exists_smooth_forall_mem_convex_of_local that allows us to construct a globally defined smooth
function from local functions.
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. Lemma
exists_smooth_forall_mem_convex_of_localis a first step in this direction.
Tags #
smooth bump function, partition of unity
Covering by supports of smooth bump functions #
In this section we define SmoothBumpCovering ι I M s to be a collection of
SmoothBumpFunctions 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 SmoothBumpCovering ι I M s
subordinate to U.
We say that a collection of SmoothBumpFunctions is a SmoothBumpCovering of a set s if
(f i).c ∈ sfor alli;- the family
fun i ↦ support (f i)is locally finite; - for each point
x ∈ sthere existsisuch thatf i =ᶠ[𝓝 x] 1; in other words,xbelongs to the interior of{y | f i y = 1};
If M is a finite dimensional real manifold which is a σ-compact Hausdorff topological space,
then for every covering U : M → Set M, ∀ x, U x ∈ 𝓝 x, there exists a SmoothBumpCovering
subordinate to U, see SmoothBumpCovering.exists_isSubordinate.
This covering can be used, e.g., to construct a partition of unity and to prove the weak Whitney embedding theorem.
- c : ι → M
The center point of each bump in the smooth covering.
- toFun : (i : ι) → SmoothBumpFunction I (self.c i)
A smooth bump function around
c i. - c_mem' : ∀ (i : ι), self.c i ∈ s
All the bump functions in the covering are centered at points in
s. - locallyFinite' : LocallyFinite fun (i : ι) => Function.support ↑(self.toFun i)
Around each point, there are only finitely many nonzero bump functions in the family.
Around each point in
s, one of the bump functions is equal to1.
Instances For
All the bump functions in the covering are centered at points in s.
Around each point, there are only finitely many nonzero bump functions in the family.
Around each point in s, one of the bump functions is equal to 1.
We say that a collection of functions form a smooth partition of unity on a set s if
- all functions are infinitely smooth and nonnegative;
- the family
fun i ↦ support (f i)is locally finite; - for all
x ∈ sthe sum∑ᶠ i, f i xequals one; - for all
x, the sum∑ᶠ i, f i xis less than or equal to one.
- toFun : ι → ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ⊤
The family of functions forming the partition of unity.
- locallyFinite' : LocallyFinite fun (i : ι) => Function.support ⇑(self.toFun i)
Around each point, there are only finitely many nonzero functions in the family.
- nonneg' : ∀ (i : ι) (x : M), 0 ≤ (self.toFun i) x
All the functions in the partition of unity are nonnegative.
- sum_eq_one' : ∀ x ∈ s, ∑ᶠ (i : ι), (self.toFun i) x = 1
The functions in the partition of unity add up to
1at any point ofs. - sum_le_one' : ∀ (x : M), ∑ᶠ (i : ι), (self.toFun i) x ≤ 1
The functions in the partition of unity add up to at most
1everywhere.
Instances For
Around each point, there are only finitely many nonzero functions in the family.
All the functions in the partition of unity are nonnegative.
The functions in the partition of unity add up to 1 at any point of s.
The functions in the partition of unity add up to at most 1 everywhere.
Equations
- SmoothPartitionOfUnity.instFunLikeContMDiffMapRealModelWithCornersSelfTopENat = { coe := SmoothPartitionOfUnity.toFun, coe_injective' := ⋯ }
Reinterpret a smooth partition of unity as a continuous partition of unity.
Equations
- f.toPartitionOfUnity = { toFun := fun (i : ι) => ↑(f i), locallyFinite' := ⋯, nonneg' := ⋯, sum_eq_one' := ⋯, sum_le_one' := ⋯ }
Instances For
If f is a smooth partition of unity on a set s : Set M and g : ι → M → F is a family of
functions such that g i is $C^n$ smooth at every point of the topological support of f i, then
the sum fun x ↦ ∑ᶠ i, f i x • g i x is smooth on the whole manifold.
If f is a smooth partition of unity on a set s : Set M and g : ι → M → F is a family of
functions such that g i is smooth at every point of the topological support of f i, then the sum
fun x ↦ ∑ᶠ i, f i x • g i x is smooth on the whole manifold.
The support of a smooth partition of unity at a point x₀ as a Finset.
This is the set of i : ι such that x₀ ∈ support f i, i.e. f i ≠ x₀.
Equations
- ρ.finsupport x₀ = ρ.toPartitionOfUnity.finsupport x₀
Instances For
The tsupports of a smooth partition of unity are locally finite.
The tsupport of a partition of unity at a point x₀ as a Finset.
This is the set of i : ι such that x₀ ∈ tsupport f i.
Equations
- ρ.fintsupport x = ⋯.toFinset
Instances For
A smooth partition of unity f i is subordinate to a family of sets U i indexed by the same
type if for each i the closure of the support of f i is a subset of U i.
Instances For
Alias of the reverse direction of SmoothPartitionOfUnity.isSubordinate_toPartitionOfUnity.
If f is a smooth partition of unity on a set s : Set M subordinate to a family of open sets
U : ι → Set M and g : ι → M → F is a family of functions such that g i is $C^n$ smooth on
U i, then the sum fun x ↦ ∑ᶠ i, f i x • g i x is $C^n$ smooth on the whole manifold.
If f is a smooth partition of unity on a set s : Set M subordinate to a family of open sets
U : ι → Set M and g : ι → M → F is a family of functions such that g i is smooth on U i,
then the sum fun x ↦ ∑ᶠ i, f i x • g i x is smooth on the whole manifold.
A BumpCovering such that all functions in this covering are smooth generates a smooth
partition of unity.
In our formalization, not every f : BumpCovering ι M s with smooth functions f i is a
SmoothBumpCovering; instead, a SmoothBumpCovering is a covering by supports of
SmoothBumpFunctions. So, we define BumpCovering.toSmoothPartitionOfUnity, then reuse it
in SmoothBumpCovering.toSmoothPartitionOfUnity.
Equations
- f.toSmoothPartitionOfUnity hf = { toFun := fun (i : ι) => ⟨⇑(f.toPartitionOfUnity i), ⋯⟩, locallyFinite' := ⋯, nonneg' := ⋯, sum_eq_one' := ⋯, sum_le_one' := ⋯ }
Instances For
Equations
- SmoothBumpCovering.instCoeFunForallSmoothBumpFunctionC = { coe := SmoothBumpCovering.toFun }
We say that f : SmoothBumpCovering ι I M s is subordinate to a map U : M → Set M if for each
index i, we have tsupport (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.
Instances For
Let M be a smooth manifold with corners modelled on a finite dimensional real vector space.
Suppose also that M is a Hausdorff σ-compact topological space. Let s be a closed set
in M and U : M → Set M be a collection of sets such that U x ∈ 𝓝 x for every x ∈ s.
Then there exists a smooth bump covering of s that is subordinate to U.
Index of a bump function such that fs i =ᶠ[𝓝 x] 1.
Equations
- fs.ind x hx = ⋯.choose
Instances For
The index type of a SmoothBumpCovering of a compact manifold is finite.
Equations
- fs.fintype = ⋯.fintypeOfCompact ⋯
Instances For
Reinterpret a SmoothBumpCovering as a continuous BumpCovering. Note that not every
f : BumpCovering ι M s with smooth functions f i is a SmoothBumpCovering.
Equations
- fs.toBumpCovering = { toFun := fun (i : ι) => { toFun := ↑(fs.toFun i), continuous_toFun := ⋯ }, locallyFinite' := ⋯, nonneg' := ⋯, le_one' := ⋯, eventuallyEq_one' := ⋯ }
Instances For
Alias of the reverse direction of SmoothBumpCovering.isSubordinate_toBumpCovering.
Every SmoothBumpCovering defines a smooth partition of unity.
Equations
- fs.toSmoothPartitionOfUnity = fs.toBumpCovering.toSmoothPartitionOfUnity ⋯
Instances For
Given two disjoint closed sets s, t in a Hausdorff σ-compact finite dimensional manifold,
there exists an infinitely smooth function that is equal to 0 on s and to 1 on t.
See also exists_msmooth_zero_iff_one_iff_of_isClosed, which ensures additionally that
f is equal to 0 exactly on s and to 1 exactly on t.
Given two disjoint closed sets s, t in a Hausdorff normal σ-compact finite dimensional
manifold M, there exists a smooth function f : M → [0,1] that vanishes in a neighbourhood of s
and is equal to 1 in a neighbourhood of t.
Given two sets s, t in a Hausdorff normal σ-compact finite-dimensional manifold M
with s open and s ⊆ interior t, there is a smooth function f : M → [0,1] which is equal to s
in a neighbourhood of s and has support contained in t.
A SmoothPartitionOfUnity that consists of a single function, uniformly equal to one,
defined as an example for Inhabited instance.
Equations
- SmoothPartitionOfUnity.single I i s = (BumpCovering.single i s).toSmoothPartitionOfUnity ⋯
Instances For
Equations
- SmoothPartitionOfUnity.instInhabited I s = { default := SmoothPartitionOfUnity.single I default s }
If X is a paracompact normal topological space and U is an open covering of a closed set
s, then there exists a SmoothPartitionOfUnity ι M s that is subordinate to U.
Let M be a σ-compact Hausdorff finite dimensional topological manifold. Let t : M → Set F
be a family of convex sets. Suppose that for each point x : M there exists a neighborhood
U ∈ 𝓝 x and a function g : M → F such that g is $C^n$ smooth on U and g y ∈ t y for all
y ∈ U. Then there exists a $C^n$ smooth function g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯ such that g x ∈ t x
for all x. See also exists_smooth_forall_mem_convex_of_local and
exists_smooth_forall_mem_convex_of_local_const.
Let M be a σ-compact Hausdorff finite dimensional topological manifold. Let t : M → Set F
be a family of convex sets. Suppose that for each point x : M there exists a neighborhood
U ∈ 𝓝 x and a function g : M → F such that g is smooth on U and g y ∈ t y for all y ∈ U.
Then there exists a smooth function g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯ such that g x ∈ t x for all x.
See also exists_contMDiffOn_forall_mem_convex_of_local and
exists_smooth_forall_mem_convex_of_local_const.
Let M be a σ-compact Hausdorff finite dimensional topological manifold. Let t : M → Set F be
a family of convex sets. Suppose that for each point x : M there exists a vector c : F such that
for all y in a neighborhood of x we have c ∈ t y. Then there exists a smooth function
g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯ such that g x ∈ t x for all x. See also
exists_contMDiffOn_forall_mem_convex_of_local and exists_smooth_forall_mem_convex_of_local.
Let M be a smooth σ-compact manifold with extended distance. Let K : ι → Set M be a locally
finite family of closed sets, let U : ι → Set M be a family of open sets such that K i ⊆ U i for
all i. Then there exists a positive smooth function δ : M → ℝ≥0 such that for any i and
x ∈ K i, we have EMetric.closedBall x (δ x) ⊆ U i.
Let M be a smooth σ-compact manifold with a metric. Let K : ι → Set M be a locally finite
family of closed sets, let U : ι → Set M be a family of open sets such that K i ⊆ U i for all
i. Then there exists a positive smooth function δ : M → ℝ≥0 such that for any i and x ∈ K i,
we have Metric.closedBall x (δ x) ⊆ U i.
Given an open set in a finite-dimensional real manifold, there exists a nonnegative smooth
function with support equal to s.
Given an open set s containing a closed set t in a finite-dimensional real manifold, there
exists a smooth function with support equal to s, taking values in [0,1], and equal to 1
exactly on t.
Given two disjoint closed sets s, t in a Hausdorff σ-compact finite dimensional manifold,
there exists an infinitely smooth function that is equal to 0 exactly on s and to 1
exactly on t. See also exists_smooth_zero_one_of_isClosed for a slightly weaker version.