Smooth partition of unity #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 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, asmooth_partition_of_unity ι I M sis a collection of smooth nonnegative functionsf 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 xequals one; -
for each
x, the sum∑ᶠ i, f i xis 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 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 smooth_bump_covering ι I M s
subordinate to U. Then we use this fact to prove a similar statement about smooth partitions of
unity, see smooth_partition_of_unity.exists_is_subordinate.
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 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.
- c : ι → M
- to_fun : Π (i : ι), smooth_bump_function I (self.c i)
- c_mem' : ∀ (i : ι), self.c i ∈ s
- locally_finite' : locally_finite (λ (i : ι), function.support ⇑(self.to_fun i))
- eventually_eq_one' : ∀ (x : M), x ∈ s → (∃ (i : ι), ⇑(self.to_fun i) =ᶠ[nhds x] 1)
We say that a collection of smooth_bump_functions is a smooth_bump_covering of a set s if
(f i).c ∈ sfor alli;- the family
λ 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 smooth_bump_covering
subordinate to U, see smooth_bump_covering.exists_is_subordinate.
This covering can be used, e.g., to construct a partition of unity and to prove the weak Whitney embedding theorem.
Instances for smooth_bump_covering
- smooth_bump_covering.has_sizeof_inst
- smooth_bump_covering.has_coe_to_fun
- to_fun : ι → cont_mdiff_map I (model_with_corners_self ℝ ℝ) M ℝ ⊤
- locally_finite' : locally_finite (λ (i : ι), function.support ⇑(self.to_fun i))
- nonneg' : ∀ (i : ι) (x : M), 0 ≤ ⇑(self.to_fun i) x
- sum_eq_one' : ∀ (x : M), x ∈ s → finsum (λ (i : ι), ⇑(self.to_fun i) x) = 1
- sum_le_one' : ∀ (x : M), finsum (λ (i : ι), ⇑(self.to_fun i) x) ≤ 1
We say that 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
λ 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.
Instances for smooth_partition_of_unity
- smooth_partition_of_unity.has_sizeof_inst
- smooth_partition_of_unity.has_coe_to_fun
- smooth_partition_of_unity.inhabited
Reinterpret a smooth partition of unity as a continuous partition of unity.
Equations
- f.to_partition_of_unity = {to_fun := λ (i : ι), ↑(⇑f i), locally_finite' := _, nonneg' := _, sum_eq_one' := _, sum_le_one' := _}
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 λ 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
λ x, ∑ᶠ i, f i x • g i x is smooth on the whole manifold.
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.
Alias of the reverse direction of smooth_partition_of_unity.is_subordinate_to_partition_of_unity.
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 λ 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 λ x, ∑ᶠ i, f i x • g i x is smooth on the whole manifold.
A bump_covering such that all functions in this covering are smooth generates a smooth
partition of unity.
In our formalization, not every f : bump_covering ι M s with smooth functions f i is a
smooth_bump_covering; instead, a smooth_bump_covering is a covering by supports of
smooth_bump_functions. So, we define bump_covering.to_smooth_partition_of_unity, then reuse it
in smooth_bump_covering.to_smooth_partition_of_unity.
Equations
- f.to_smooth_partition_of_unity hf = {to_fun := λ (i : ι), ⟨⇑(⇑(f.to_partition_of_unity) i), _⟩, locally_finite' := _, nonneg' := _, sum_eq_one' := _, sum_le_one' := _}
Equations
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 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.
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.
The index type of a smooth_bump_covering of a compact manifold is finite.
Equations
- fs.fintype = _.fintype_of_compact _
Reinterpret a smooth_bump_covering as a continuous bump_covering. Note that not every
f : bump_covering ι M s with smooth functions f i is a smooth_bump_covering.
Equations
- fs.to_bump_covering = {to_fun := λ (i : ι), {to_fun := ⇑(⇑fs i), continuous_to_fun := _}, locally_finite' := _, nonneg' := _, le_one' := _, eventually_eq_one' := _}
Alias of the reverse direction of smooth_bump_covering.is_subordinate_to_bump_covering.
Every smooth_bump_covering defines a smooth partition of unity.
Equations
Given two disjoint closed sets in a Hausdorff σ-compact finite dimensional manifold, there
exists an infinitely smooth function that is equal to 0 on one of them and is equal to one on the
other.
A smooth_partition_of_unity that consists of a single function, uniformly equal to one,
defined as an example for inhabited instance.
Equations
Equations
If X is a paracompact normal topological space and U is an open covering of a closed set
s, then there exists a bump_covering ι X 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_cont_mdiff_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_cont_mdiff_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.closed_ball 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.closed_ball x (δ x) ⊆ U i.