mathlib documentation

geometry.manifold.bump_function

Smooth bump functions on a smooth manifold #

In this file we define smooth_bump_function I c to be a bundled smooth "bump" function centered at c. It is a structure that consists of two real numbers 0 < r < R with small enough R. We define a coercion to function for this type, and for f : smooth_bump_function I c, the function ⇑f written in the extended chart at f.c has the following properties:

The actual statements involve (pre)images under ext_chart_at I f.c and are given as lemmas in the smooth_bump_function namespace.

We also define smooth_bump_covering of a set s : set M to be a collection of smooth_bump_functions such that their supports is a locally finite family of sets, and for each point x ∈ s there exists a bump function f i in the collection such that f i =ᶠ[𝓝 x] 1. This structure is the main building block in the construction of a smooth partition of unity (see TODO), and can be used instead of a partition of unity in some proofs.

We say that f : smooth_bump_covering I 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 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.

TODO #

Tags #

manifold, smooth bump function, partition of unity, Whitney theorem

Smooth bump function #

In this section we define a structure for a bundled smooth bump function and prove its properties.

structure smooth_bump_function {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] (c : M) :
Type

Given a smooth manifold modelled on a finite dimensional space E, f : smooth_bump_function I M is a smooth function on M such that in the extended chart e at f.c:

  • f x = 1 in the closed euclidean ball of radius f.r centered at f.c;
  • f x = 0 outside of the euclidean ball of radius f.R centered at f.c;
  • 0 ≤ f x ≤ 1 for all x.

The structure contains data required to construct a function with these properties. The function is available as ⇑f or f x. Formal statements of the properties listed above involve some (pre)images under ext_chart_at I f.c and are given as lemmas in the msmooth_bump_function namespace.

def smooth_bump_function.to_fun {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] {c : M} (f : smooth_bump_function I c) :
M →

The function defined by f : smooth_bump_function c. Use automatic coercion to function instead.

Equations
theorem smooth_bump_function.mem_Icc {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] {c : M} (f : smooth_bump_function I c) {x : M} :
f x set.Icc 0 1
theorem smooth_bump_function.nonneg {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] {c : M} (f : smooth_bump_function I c) {x : M} :
0 f x
theorem smooth_bump_function.le_one {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] {c : M} (f : smooth_bump_function I c) {x : M} :
f x 1
@[simp]
theorem smooth_bump_function.eq_one {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] {c : M} (f : smooth_bump_function I c) :
f c = 1

Given a smooth bump function f : smooth_bump_function I c, the closed ball of radius f.R is known to include the support of f. These closed balls (in the model normed space E) intersected with set.range I form a basis of 𝓝[range I] (ext_chart_at I c c).

If f is a smooth bump function and s closed subset of the support of f (i.e., of the open ball of radius f.R), then there exists 0 < r < f.R such that s is a subset of the open ball of radius r. Formally, s ⊆ e.source ∩ e ⁻¹' (ball (e c) r), where e = ext_chart_at I c.

@[instance]
Equations

The closures of supports of smooth bump functions centered at c form a basis of 𝓝 c. In other words, each of these closures is a neighborhood of c and each neighborhood of c includes closure (support f) for some f : smooth_bump_function I c.

Given s ∈ 𝓝 c, the supports of smooth bump functions f : smooth_bump_function I c such that closure (support f) ⊆ s form a basis of 𝓝 c. In other words, each of these supports is a neighborhood of c and each neighborhood of c includes support f for some f : smooth_bump_function I c such that closure (support f) ⊆ s.

A smooth bump function is infinitely smooth.

theorem smooth_bump_function.smooth_smul {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] {c : M} (f : smooth_bump_function I c) [t2_space M] [smooth_manifold_with_corners I M] {G : Type u_1} [normed_group G] [normed_space G] {g : M → G} (hg : smooth_on I 𝓘(, G) g (chart_at H c).to_local_equiv.source) :
smooth I 𝓘(, G) (λ (x : M), f x g x)

If f : smooth_bump_function I c is a smooth bump function and g : M → G is a function smooth on the source of the chart at c, then f • g is smooth on the whole manifold.

Covering by supports of smooth bump functions #

In this section we define smooth_bump_covering I 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 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.

structure smooth_bump_covering {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) :
Type (uM+1)

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 a choice of smooth_bump_covering is available as smooth_bump_covering.choice_set, see also smooth_bump_covering.choice for the case s = univ and smooth_bump_covering.exists_is_subordinate for a lemma providing a covering subordinate to a given U : M → set M.

This covering can be used, e.g., to construct a partition of unity and to prove the weak Whitney embedding theorem.

@[simp]
theorem smooth_bump_covering.coe_mk {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} (ι : Type uM) (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 {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 s) (U : M → set M) :
Prop

We say that f : smooth_bump_covering I 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.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) :

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.

Choice of a covering of a closed set s by supports of smooth bump functions.

Equations

Choice of a covering of a manifold by supports of smooth bump functions.

Equations
theorem smooth_bump_covering.point_finite {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 s) (x : M) :
{i : fs.ι | (fs i) x 0}.finite
theorem smooth_bump_covering.mem_chart_at_source_of_eq_one {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 s) {i : fs.ι} {x : M} (h : (fs i) x = 1) :
theorem smooth_bump_covering.mem_ext_chart_at_source_of_eq_one {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 s) {i : fs.ι} {x : M} (h : (fs i) x = 1) :
x (ext_chart_at I (fs.c i)).source
def smooth_bump_covering.ind {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 s) (x : M) (hx : x s) :
fs.ι

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

Equations
theorem smooth_bump_covering.eventually_eq_one {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 s) (x : M) (hx : x s) :
(fs (fs.ind x hx)) =ᶠ[𝓝 x] 1
theorem smooth_bump_covering.apply_ind {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 s) (x : M) (hx : x s) :
(fs (fs.ind x hx)) x = 1
theorem smooth_bump_covering.mem_support_ind {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 s) (x : M) (hx : x s) :
x function.support (fs (fs.ind x hx))
theorem smooth_bump_covering.mem_chart_at_ind_source {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 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 {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 s) (x : M) (hx : x s) :
x (ext_chart_at I (fs.c (fs.ind x hx))).source

Whitney embedding theorem #

In this section we prove a version of the Whitney embedding theorem: for any compact real manifold M, for sufficiently large n there exists a smooth embedding M → ℝ^n.

Smooth embedding of M into (E × ℝ) ^ f.ι.

Equations
theorem smooth_bump_covering.embedding_pi_tangent_coe {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 s) [t2_space M] [fintype fs.ι] :
(fs.embedding_pi_tangent) = λ (x : M) (i : fs.ι), ((fs i) x (ext_chart_at I (fs.c i)) x, (fs i) x)

Baby version of the Whitney weak embedding theorem: if M admits a finite covering by supports of bump functions, then for some n it can be immersed into the n-dimensional Euclidean space.

Baby version of the Whitney weak embedding theorem: if M admits a finite covering by supports of bump functions, then for some n it can be embedded into the n-dimensional Euclidean space.