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 = 1in the closed euclidean ball of radiusf.rcentered atc;f x = 0outside of the euclidean ball of radiusf.Rcentered atc;0 ≤ f x ≤ 1for 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.
structure
smooth_bump_function
{E : Type uE}
[normed_add_comm_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
- 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 = 1in the closed euclidean ball of radiusf.rcentered atf.c;f x = 0outside of the euclidean ball of radiusf.Rcentered atf.c;0 ≤ f x ≤ 1for 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
noncomputable
def
smooth_bump_function.to_fun
{E : Type uE}
[normed_add_comm_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
- f.to_fun = (charted_space.chart_at H c).to_local_equiv.source.indicator (⇑(f.to_cont_diff_bump) ∘ ⇑(ext_chart_at I c))
@[protected, instance]
noncomputable
def
smooth_bump_function.has_coe_to_fun
{E : Type uE}
[normed_add_comm_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} :
has_coe_to_fun (smooth_bump_function I c) (λ (_x : smooth_bump_function I c), M → ℝ)
Equations
theorem
smooth_bump_function.coe_def
{E : Type uE}
[normed_add_comm_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 = (charted_space.chart_at H c).to_local_equiv.source.indicator (⇑(f.to_cont_diff_bump) ∘ ⇑(ext_chart_at I c))
theorem
smooth_bump_function.R_pos
{E : Type uE}
[normed_add_comm_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) :
theorem
smooth_bump_function.ball_subset
{E : Type uE}
[normed_add_comm_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) :
euclidean.ball (⇑(ext_chart_at I c) c) f.to_cont_diff_bump.to_cont_diff_bump_of_inner.R ∩ set.range ⇑I ⊆ (ext_chart_at I c).target
theorem
smooth_bump_function.eq_on_source
{E : Type uE}
[normed_add_comm_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) :
set.eq_on ⇑f (⇑(f.to_cont_diff_bump) ∘ ⇑(ext_chart_at I c)) (charted_space.chart_at H c).to_local_equiv.source
theorem
smooth_bump_function.eventually_eq_of_mem_source
{E : Type uE}
[normed_add_comm_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}
(hx : x ∈ (charted_space.chart_at H c).to_local_equiv.source) :
⇑f =ᶠ[nhds x] ⇑(f.to_cont_diff_bump) ∘ ⇑(ext_chart_at I c)
theorem
smooth_bump_function.one_of_dist_le
{E : Type uE}
[normed_add_comm_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}
(hs : x ∈ (charted_space.chart_at H c).to_local_equiv.source)
(hd : euclidean.dist (⇑(ext_chart_at I c) x) (⇑(ext_chart_at I c) c) ≤ f.to_cont_diff_bump.to_cont_diff_bump_of_inner.r) :
theorem
smooth_bump_function.support_eq_inter_preimage
{E : Type uE}
[normed_add_comm_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) :
function.support ⇑f = (charted_space.chart_at H c).to_local_equiv.source ∩ ⇑(ext_chart_at I c) ⁻¹' euclidean.ball (⇑(ext_chart_at I c) c) f.to_cont_diff_bump.to_cont_diff_bump_of_inner.R
theorem
smooth_bump_function.open_support
{E : Type uE}
[normed_add_comm_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) :
theorem
smooth_bump_function.support_eq_symm_image
{E : Type uE}
[normed_add_comm_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) :
function.support ⇑f = ⇑((ext_chart_at I c).symm) '' (euclidean.ball (⇑(ext_chart_at I c) c) f.to_cont_diff_bump.to_cont_diff_bump_of_inner.R ∩ set.range ⇑I)
theorem
smooth_bump_function.support_subset_source
{E : Type uE}
[normed_add_comm_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) :
theorem
smooth_bump_function.image_eq_inter_preimage_of_subset_support
{E : Type uE}
[normed_add_comm_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)
{s : set M}
(hs : s ⊆ function.support ⇑f) :
⇑(ext_chart_at I c) '' s = euclidean.closed_ball (⇑(ext_chart_at I c) c) f.to_cont_diff_bump.to_cont_diff_bump_of_inner.R ∩ set.range ⇑I ∩ ⇑((ext_chart_at I c).symm) ⁻¹' s
theorem
smooth_bump_function.mem_Icc
{E : Type uE}
[normed_add_comm_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} :
theorem
smooth_bump_function.nonneg
{E : Type uE}
[normed_add_comm_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} :
theorem
smooth_bump_function.le_one
{E : Type uE}
[normed_add_comm_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} :
theorem
smooth_bump_function.eventually_eq_one_of_dist_lt
{E : Type uE}
[normed_add_comm_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}
(hs : x ∈ (charted_space.chart_at H c).to_local_equiv.source)
(hd : euclidean.dist (⇑(ext_chart_at I c) x) (⇑(ext_chart_at I c) c) < f.to_cont_diff_bump.to_cont_diff_bump_of_inner.r) :
theorem
smooth_bump_function.eventually_eq_one
{E : Type uE}
[normed_add_comm_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) :
@[simp]
theorem
smooth_bump_function.eq_one
{E : Type uE}
[normed_add_comm_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) :
theorem
smooth_bump_function.support_mem_nhds
{E : Type uE}
[normed_add_comm_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) :
function.support ⇑f ∈ nhds c
theorem
smooth_bump_function.tsupport_mem_nhds
{E : Type uE}
[normed_add_comm_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) :
theorem
smooth_bump_function.c_mem_support
{E : Type uE}
[normed_add_comm_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) :
c ∈ function.support ⇑f
theorem
smooth_bump_function.nonempty_support
{E : Type uE}
[normed_add_comm_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) :
theorem
smooth_bump_function.compact_symm_image_closed_ball
{E : Type uE}
[normed_add_comm_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) :
is_compact (⇑((ext_chart_at I c).symm) '' (euclidean.closed_ball (⇑(ext_chart_at I c) c) f.to_cont_diff_bump.to_cont_diff_bump_of_inner.R ∩ set.range ⇑I))
theorem
smooth_bump_function.nhds_within_range_basis
{E : Type uE}
[normed_add_comm_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} :
(nhds_within (⇑(ext_chart_at I c) c) (set.range ⇑I)).has_basis (λ (f : smooth_bump_function I c), true) (λ (f : smooth_bump_function I c), euclidean.closed_ball (⇑(ext_chart_at I c) c) f.to_cont_diff_bump.to_cont_diff_bump_of_inner.R ∩ set.range ⇑I)
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).
theorem
smooth_bump_function.closed_image_of_closed
{E : Type uE}
[normed_add_comm_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)
{s : set M}
(hsc : is_closed s)
(hs : s ⊆ function.support ⇑f) :
is_closed (⇑(ext_chart_at I c) '' s)
theorem
smooth_bump_function.exists_r_pos_lt_subset_ball
{E : Type uE}
[normed_add_comm_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)
{s : set M}
(hsc : is_closed s)
(hs : s ⊆ function.support ⇑f) :
∃ (r : ℝ) (hr : r ∈ set.Ioo 0 f.to_cont_diff_bump.to_cont_diff_bump_of_inner.R), s ⊆ (charted_space.chart_at H c).to_local_equiv.source ∩ ⇑(ext_chart_at I c) ⁻¹' euclidean.ball (⇑(ext_chart_at I c) c) r
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.
noncomputable
def
smooth_bump_function.update_r
{E : Type uE}
[normed_add_comm_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)
(r : ℝ)
(hr : r ∈ set.Ioo 0 f.to_cont_diff_bump.to_cont_diff_bump_of_inner.R) :
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 := _}
@[simp]
theorem
smooth_bump_function.update_r_R
{E : Type uE}
[normed_add_comm_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)
{r : ℝ}
(hr : r ∈ set.Ioo 0 f.to_cont_diff_bump.to_cont_diff_bump_of_inner.R) :
@[simp]
theorem
smooth_bump_function.update_r_r
{E : Type uE}
[normed_add_comm_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)
{r : ℝ}
(hr : r ∈ set.Ioo 0 f.to_cont_diff_bump.to_cont_diff_bump_of_inner.R) :
(f.update_r r hr).to_cont_diff_bump.to_cont_diff_bump_of_inner.r = r
@[simp]
theorem
smooth_bump_function.support_update_r
{E : Type uE}
[normed_add_comm_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)
{r : ℝ}
(hr : r ∈ set.Ioo 0 f.to_cont_diff_bump.to_cont_diff_bump_of_inner.R) :
function.support ⇑(f.update_r r hr) = function.support ⇑f
@[protected, instance]
noncomputable
def
smooth_bump_function.inhabited
{E : Type uE}
[normed_add_comm_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} :
Equations
- smooth_bump_function.inhabited = classical.inhabited_of_nonempty smooth_bump_function.inhabited._proof_1
theorem
smooth_bump_function.closed_symm_image_closed_ball
{E : Type uE}
[normed_add_comm_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] :
is_closed (⇑((ext_chart_at I c).symm) '' (euclidean.closed_ball (⇑(ext_chart_at I c) c) f.to_cont_diff_bump.to_cont_diff_bump_of_inner.R ∩ set.range ⇑I))
theorem
smooth_bump_function.tsupport_subset_symm_image_closed_ball
{E : Type uE}
[normed_add_comm_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] :
tsupport ⇑f ⊆ ⇑((ext_chart_at I c).symm) '' (euclidean.closed_ball (⇑(ext_chart_at I c) c) f.to_cont_diff_bump.to_cont_diff_bump_of_inner.R ∩ set.range ⇑I)
theorem
smooth_bump_function.tsupport_subset_ext_chart_at_source
{E : Type uE}
[normed_add_comm_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] :
tsupport ⇑f ⊆ (ext_chart_at I c).source
theorem
smooth_bump_function.tsupport_subset_chart_at_source
{E : Type uE}
[normed_add_comm_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] :
@[protected]
theorem
smooth_bump_function.has_compact_support
{E : Type uE}
[normed_add_comm_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] :
theorem
smooth_bump_function.nhds_basis_tsupport
{E : Type uE}
[normed_add_comm_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)
[t2_space M] :
(nhds c).has_basis (λ (f : smooth_bump_function I c), true) (λ (f : smooth_bump_function I c), tsupport ⇑f)
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.
theorem
smooth_bump_function.nhds_basis_support
{E : Type uE}
[normed_add_comm_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}
[t2_space M]
{s : set M}
(hs : s ∈ nhds c) :
(nhds c).has_basis (λ (f : smooth_bump_function I c), tsupport ⇑f ⊆ s) (λ (f : smooth_bump_function I c), function.support ⇑f)
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.
@[protected]
theorem
smooth_bump_function.smooth
{E : Type uE}
[normed_add_comm_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] :
smooth I (model_with_corners_self ℝ ℝ) ⇑f
A smooth bump function is infinitely smooth.
@[protected]
theorem
smooth_bump_function.smooth_at
{E : Type uE}
[normed_add_comm_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]
{x : M} :
smooth_at I (model_with_corners_self ℝ ℝ) ⇑f x
@[protected]
theorem
smooth_bump_function.continuous
{E : Type uE}
[normed_add_comm_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] :
theorem
smooth_bump_function.smooth_smul
{E : Type uE}
[normed_add_comm_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_add_comm_group G]
[normed_space ℝ G]
{g : M → G}
(hg : smooth_on I (model_with_corners_self ℝ G) g (charted_space.chart_at H c).to_local_equiv.source) :
smooth I (model_with_corners_self ℝ 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.