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:
f x = 1
in the closed euclidean ball of radiusf.r
centered atc
;f x = 0
outside of the euclidean ball of radiusf.R
centered atc
;0 ≤ f x ≤ 1
for allx
.
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.
- to_cont_diff_bump : cont_diff_bump (⇑(ext_chart_at I c) c)
- closed_ball_subset : euclidean.closed_ball (⇑(ext_chart_at I c) c) self.to_cont_diff_bump.to_cont_diff_bump_of_inner.R ∩ set.range ⇑I ⊆ (ext_chart_at I c).target
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 radiusf.r
centered atf.c
;f x = 0
outside of the euclidean ball of radiusf.R
centered atf.c
;0 ≤ f x ≤ 1
for allx
.
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.
Instances for smooth_bump_function
- smooth_bump_function.has_sizeof_inst
- smooth_bump_function.has_coe_to_fun
- smooth_bump_function.inhabited
The function defined by f : smooth_bump_function c
. Use automatic coercion to function
instead.
Equations
- f.to_fun = (charted_space.chart_at H c).to_local_equiv.source.indicator (⇑(f.to_cont_diff_bump) ∘ ⇑(ext_chart_at I c))
Equations
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
.
Replace r
with another value in the interval (0, f.R)
.
Equations
- f.update_r r hr = {to_cont_diff_bump := {to_cont_diff_bump_of_inner := {r := r, R := f.to_cont_diff_bump.to_cont_diff_bump_of_inner.R, r_pos := _, r_lt_R := _}}, closed_ball_subset := _}
Equations
- smooth_bump_function.inhabited = classical.inhabited_of_nonempty smooth_bump_function.inhabited._proof_1
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
.
A smooth bump function is infinitely smooth.
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.