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 c has the following properties:

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

Tags #

manifold, smooth bump function

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 smooth_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.