mathlib documentation

geometry.manifold.partition_of_unity

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

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 #

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.

@[nolint]
structure smooth_bump_covering (ι : Type uι) {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] (I : model_with_corners E H) (M : Type uM) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] (s : set M := set.univ) :
Type (max uM uι)

We say that a collection of smooth_bump_functions is a smooth_bump_covering of a set s if

  • (f i).c ∈ s for all i;
  • the family λ i, support (f i) is locally finite;
  • for each point x ∈ s there exists i such that f i =ᶠ[𝓝 x] 1; in other words, x belongs to the interior of {y | f i y = 1};

If M is a finite dimensional real manifold which is a sigma-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.

structure smooth_partition_of_unity (ι : Type uι) {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] (I : model_with_corners E H) (M : Type uM) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] (s : set M := set.univ) :
Type (max uM uι)

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 ∈ s the sum ∑ᶠ i, f i x equals one;
  • for all x, the sum ∑ᶠ i, f i x is less than or equal to one.
theorem smooth_partition_of_unity.locally_finite {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (f : smooth_partition_of_unity ι I M s) :
theorem smooth_partition_of_unity.nonneg {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (f : smooth_partition_of_unity ι I M s) (i : ι) (x : M) :
0 (f i) x
theorem smooth_partition_of_unity.sum_eq_one {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (f : smooth_partition_of_unity ι I M s) {x : M} (hx : x s) :
∑ᶠ (i : ι), (f i) x = 1
theorem smooth_partition_of_unity.sum_le_one {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (f : smooth_partition_of_unity ι I M s) (x : M) :
∑ᶠ (i : ι), (f i) x 1

Reinterpret a smooth partition of unity as a continuous partition of unity.

Equations
theorem smooth_partition_of_unity.smooth_sum {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (f : smooth_partition_of_unity ι I M s) :
smooth I 𝓘(, ) (λ (x : M), ∑ᶠ (i : ι), (f i) x)
theorem smooth_partition_of_unity.le_one {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (f : smooth_partition_of_unity ι I M s) (i : ι) (x : M) :
(f i) x 1
theorem smooth_partition_of_unity.sum_nonneg {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (f : smooth_partition_of_unity ι I M s) (x : M) :
0 ∑ᶠ (i : ι), (f i) x
def smooth_partition_of_unity.is_subordinate {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (f : smooth_partition_of_unity ι I M s) (U : ι → set M) :
Prop

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.

Equations

Alias of is_subordinate_to_partition_of_unity.

theorem bump_covering.smooth_to_partition_of_unity {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] {s : set M} (f : bump_covering ι M s) (hf : ∀ (i : ι), smooth I 𝓘(, ) (f i)) (i : ι) :
def bump_covering.to_smooth_partition_of_unity {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (f : bump_covering ι M s) (hf : ∀ (i : ι), smooth I 𝓘(, ) (f i)) :

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
@[simp]
theorem bump_covering.coe_to_smooth_partition_of_unity {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (f : bump_covering ι M s) (hf : ∀ (i : ι), smooth I 𝓘(, ) (f i)) (i : ι) :
theorem bump_covering.is_subordinate.to_smooth_partition_of_unity {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} {f : bump_covering ι M s} {U : ι → set M} (h : f.is_subordinate U) (hf : ∀ (i : ι), smooth I 𝓘(, ) (f i)) :
@[instance]
Equations
@[simp]
theorem smooth_bump_covering.coe_mk {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (c : ι → M) (to_fun : Π (i : ι), smooth_bump_function I (c i)) (h₁ : ∀ (i : ι), c i s) (h₂ : locally_finite (λ (i : ι), function.support (to_fun i))) (h₃ : ∀ (x : M), x s(∃ (i : ι), (to_fun i) =ᶠ[𝓝 x] 1)) :
{c := c, to_fun := to_fun, c_mem' := h₁, locally_finite' := h₂, eventually_eq_one' := h₃} = to_fun
def smooth_bump_covering.is_subordinate {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (f : smooth_bump_covering ι I M s) (U : M → set M) :
Prop

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.

Equations
theorem smooth_bump_covering.is_subordinate.support_subset {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} {fs : smooth_bump_covering ι I M s} {U : M → set M} (h : fs.is_subordinate U) (i : ι) :
function.support (fs i) U (fs.c i)
theorem smooth_bump_covering.exists_is_subordinate {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] (I : model_with_corners E H) {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} {U : M → set M} [t2_space M] [sigma_compact_space M] (hs : is_closed s) (hU : ∀ (x : M), x sU x 𝓝 x) :
∃ (ι : Type uM) (f : smooth_bump_covering ι I M s), f.is_subordinate U

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.

theorem smooth_bump_covering.locally_finite {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) :
theorem smooth_bump_covering.point_finite {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) (x : M) :
{i : ι | (fs i) x 0}.finite
theorem smooth_bump_covering.mem_chart_at_source_of_eq_one {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) {i : ι} {x : M} (h : (fs i) x = 1) :
theorem smooth_bump_covering.mem_ext_chart_at_source_of_eq_one {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) {i : ι} {x : M} (h : (fs i) x = 1) :
x (ext_chart_at I (fs.c i)).source
def smooth_bump_covering.ind {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) (x : M) (hx : x s) :
ι

Index of a bump function such that fs i =ᶠ[𝓝 x] 1.

Equations
theorem smooth_bump_covering.eventually_eq_one {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) (x : M) (hx : x s) :
(fs (fs.ind x hx)) =ᶠ[𝓝 x] 1
theorem smooth_bump_covering.apply_ind {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) (x : M) (hx : x s) :
(fs (fs.ind x hx)) x = 1
theorem smooth_bump_covering.mem_support_ind {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) (x : M) (hx : x s) :
x function.support (fs (fs.ind x hx))
theorem smooth_bump_covering.mem_chart_at_ind_source {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) (x : M) (hx : x s) :
x (chart_at H (fs.c (fs.ind x hx))).to_local_equiv.source
theorem smooth_bump_covering.mem_ext_chart_at_ind_source {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) (x : M) (hx : x s) :
x (ext_chart_at I (fs.c (fs.ind x hx))).source
def smooth_bump_covering.fintype {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) [compact_space M] :

The index type of a smooth_bump_covering of a compact manifold is finite.

Equations
def smooth_bump_covering.to_bump_covering {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) [t2_space M] :

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
@[simp]
theorem smooth_bump_covering.is_subordinate_to_bump_covering {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} [t2_space M] {f : smooth_bump_covering ι I M s} {U : M → set M} :
f.to_bump_covering.is_subordinate (λ (i : ι), U (f.c i)) f.is_subordinate U
theorem smooth_bump_covering.is_subordinate.to_bump_covering {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} [t2_space M] {f : smooth_bump_covering ι I M s} {U : M → set M} :
f.is_subordinate Uf.to_bump_covering.is_subordinate (λ (i : ι), U (f.c i))

Alias of is_subordinate_to_bump_covering.

theorem smooth_bump_covering.to_smooth_partition_of_unity_apply {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) [t2_space M] (i : ι) (x : M) :
((fs.to_smooth_partition_of_unity) i) x = ((fs i) x) * ∏ᶠ (j : ι) (hj : well_ordering_rel j i), (1 - (fs j) x)
theorem smooth_bump_covering.to_smooth_partition_of_unity_eq_mul_prod {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) [t2_space M] (i : ι) (x : M) (t : finset ι) (ht : ∀ (j : ι), well_ordering_rel j i(fs j) x 0j t) :
((fs.to_smooth_partition_of_unity) i) x = ((fs i) x) * ∏ (j : ι) in finset.filter (λ (j : ι), well_ordering_rel j i) t, (1 - (fs j) x)
theorem smooth_bump_covering.exists_finset_to_smooth_partition_of_unity_eventually_eq {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) [t2_space M] (i : ι) (x : M) :
∃ (t : finset ι), ((fs.to_smooth_partition_of_unity) i) =ᶠ[𝓝 x] ((fs i)) * ∏ (j : ι) in finset.filter (λ (j : ι), well_ordering_rel j i) t, (1 - (fs j))
theorem smooth_bump_covering.to_smooth_partition_of_unity_zero_of_zero {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) [t2_space M] {i : ι} {x : M} (h : (fs i) x = 0) :
theorem smooth_bump_covering.is_subordinate.to_smooth_partition_of_unity {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} [t2_space M] {f : smooth_bump_covering ι I M s} {U : M → set M} (h : f.is_subordinate U) :
theorem smooth_bump_covering.sum_to_smooth_partition_of_unity_eq {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} (fs : smooth_bump_covering ι I M s) [t2_space M] (x : M) :
∑ᶠ (i : ι), ((fs.to_smooth_partition_of_unity) i) x = 1 - ∏ᶠ (i : ι), (1 - (fs i) x)
theorem exists_smooth_zero_one_of_closed {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] (I : model_with_corners E H) {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] [t2_space M] [sigma_compact_space M] {s t : set M} (hs : is_closed s) (ht : is_closed t) (hd : disjoint s t) :
∃ (f : C^I, M; 𝓘(, ), ), set.eq_on f 0 s set.eq_on f 1 t ∀ (x : M), f x set.Icc 0 1

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.

def smooth_partition_of_unity.single {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] (i : ι) (s : set M) :

A smooth_partition_of_unity that consists of a single function, uniformly equal to one, defined as an example for inhabited instance.

Equations
theorem smooth_partition_of_unity.exists_is_subordinate {ι : Type uι} {E : Type uE} [normed_group E] [normed_space E] [finite_dimensional E] {H : Type uH} [topological_space H] {I : model_with_corners E H} {M : Type uM} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] [t2_space M] [sigma_compact_space M] {s : set M} (hs : is_closed s) (U : ι → set M) (ho : ∀ (i : ι), is_open (U i)) (hU : s ⋃ (i : ι), U i) :

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.