# mathlib3documentation

geometry.manifold.bump_function

# Smooth bump functions on a smooth manifold #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 ball of radius f.r centered at c;
• f x = 0 outside of the ball of radius f.R centered at c;
• 0 ≤ f x ≤ 1 for all x.

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} [ E] {H : Type uH} (I : H) {M : Type uM} [ M] (c : M) :

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 ball of radius f.r centered at f.c;
• f x = 0 outside of the 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.

Instances for smooth_bump_function
noncomputable def smooth_bump_function.to_fun {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :

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

Equations
@[protected, instance]
noncomputable def smooth_bump_function.has_coe_to_fun {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} :
(λ (_x : , M )
Equations
theorem smooth_bump_function.coe_def {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :
theorem smooth_bump_function.R_pos {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :
theorem smooth_bump_function.ball_subset {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :
theorem smooth_bump_function.eq_on_source {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :
theorem smooth_bump_function.eventually_eq_of_mem_source {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) {x : M} (hx : x ) :
theorem smooth_bump_function.one_of_dist_le {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) {x : M} (hs : x ) (hd : has_dist.dist ( c) x) ( c) c) f.to_cont_diff_bump.r) :
f x = 1
theorem smooth_bump_function.support_eq_inter_preimage {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :
theorem smooth_bump_function.is_open_support {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :
theorem smooth_bump_function.support_eq_symm_image {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :
theorem smooth_bump_function.support_subset_source {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :
theorem smooth_bump_function.image_eq_inter_preimage_of_subset_support {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) {s : set M} (hs : s ) :
theorem smooth_bump_function.mem_Icc {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) {x : M} :
f x 1
theorem smooth_bump_function.nonneg {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) {x : M} :
0 f x
theorem smooth_bump_function.le_one {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) {x : M} :
f x 1
theorem smooth_bump_function.eventually_eq_one_of_dist_lt {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) {x : M} (hs : x ) (hd : has_dist.dist ( c) x) ( c) c) < f.to_cont_diff_bump.r) :
theorem smooth_bump_function.eventually_eq_one {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :
@[simp]
theorem smooth_bump_function.eq_one {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :
f c = 1
theorem smooth_bump_function.support_mem_nhds {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :
theorem smooth_bump_function.tsupport_mem_nhds {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :
theorem smooth_bump_function.c_mem_support {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :
theorem smooth_bump_function.nonempty_support {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :
theorem smooth_bump_function.is_compact_symm_image_closed_ball {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) :
theorem smooth_bump_function.nhds_within_range_basis {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} :
(nhds_within ( c) c) (set.range I)).has_basis (λ (f : , true) (λ (f : , metric.closed_ball ( c) c) f.to_cont_diff_bump.R

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.is_closed_image_of_is_closed {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) {s : set M} (hsc : is_closed s) (hs : s ) :
theorem smooth_bump_function.exists_r_pos_lt_subset_ball {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) {s : set M} (hsc : is_closed s) (hs : s ) :
(r : ) (hr : r , s c) ⁻¹' metric.ball ( 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} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) (r : ) (hr : r ) :

Replace r with another value in the interval (0, f.R).

Equations
@[simp]
theorem smooth_bump_function.update_r_R {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) {r : } (hr : r ) :
@[simp]
theorem smooth_bump_function.update_r_r {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) {r : } (hr : r ) :
@[simp]
theorem smooth_bump_function.support_update_r {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) {r : } (hr : r ) :
@[protected, instance]
noncomputable def smooth_bump_function.inhabited {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} :
Equations
theorem smooth_bump_function.is_closed_symm_image_closed_ball {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) [t2_space M] :
theorem smooth_bump_function.tsupport_subset_symm_image_closed_ball {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) [t2_space M] :
theorem smooth_bump_function.tsupport_subset_ext_chart_at_source {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) [t2_space M] :
theorem smooth_bump_function.tsupport_subset_chart_at_source {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) [t2_space M] :
@[protected]
theorem smooth_bump_function.has_compact_support {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) [t2_space M] :
theorem smooth_bump_function.nhds_basis_tsupport {E : Type uE} [ E] {H : Type uH} (I : H) {M : Type uM} [ M] (c : M) [t2_space M] :
(nhds c).has_basis (λ (f : , true) (λ (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} [ E] {H : Type uH} (I : H) {M : Type uM} [ M] {c : M} [t2_space M] {s : set M} (hs : s nhds c) :
(nhds c).has_basis (λ (f : , s) (λ (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} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) [t2_space M]  :
f

A smooth bump function is infinitely smooth.

@[protected]
theorem smooth_bump_function.smooth_at {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) [t2_space M] {x : M} :
x
@[protected]
theorem smooth_bump_function.continuous {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) [t2_space M]  :
theorem smooth_bump_function.smooth_smul {E : Type uE} [ E] {H : Type uH} {I : H} {M : Type uM} [ M] {c : M} (f : c) [t2_space M] {G : Type u_1} [ G] {g : M G} (hg : 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.