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:
f x = 1 in the closed euclidean ball of radius f.r centered at c;
f x = 0 outside of the euclidean ball of radius f.R centered at c;
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 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
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.
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 tsupport 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
tsupport 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 tsupport f ⊆ s.