# Smooth bump functions on a smooth manifold #

In this file we define SmoothBumpFunction I c to be a bundled smooth "bump" function centered at c. It is a structure that consists of two real numbers 0 < rIn < rOut with small enough rOut. We define a coercion to function for this type, and for f : SmoothBumpFunction 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.rIn centered at c;
• f x = 0 outside of the ball of radius f.rOut centered at c;
• 0 ≤ f x ≤ 1 for all x.

The actual statements involve (pre)images under extChartAt I f and are given as lemmas in the SmoothBumpFunction 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 SmoothBumpFunction {E : Type uE} [] {H : Type uH} [] (I : ) {M : Type uM} [] [] (c : M) extends :

Given a smooth manifold modelled on a finite dimensional space E, f : SmoothBumpFunction 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.rIn centered at f.c;
• f x = 0 outside of the ball of radius f.rOut 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 extChartAt I f.c and are given as lemmas in the SmoothBumpFunction namespace.

Instances For
theorem SmoothBumpFunction.closedBall_subset {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (self : ) :
Metric.closedBall ((extChartAt I c) c) self.rOut (extChartAt I c).target
def SmoothBumpFunction.toFun {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] {c : M} (f : ) :
M

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

Equations
Instances For
instance SmoothBumpFunction.instCoeFunForallReal {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] {c : M} :
CoeFun fun (x : ) => M
Equations
• SmoothBumpFunction.instCoeFunForallReal = { coe := SmoothBumpFunction.toFun }
theorem SmoothBumpFunction.coe_def {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] [] {c : M} (f : ) :
f = (chartAt H c).source.indicator (f.toContDiffBump (extChartAt I c))
theorem SmoothBumpFunction.rOut_pos {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) :
0 < f.rOut
theorem SmoothBumpFunction.ball_subset {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) :
Metric.ball ((extChartAt I c) c) f.rOut (extChartAt I c).target
theorem SmoothBumpFunction.ball_inter_range_eq_ball_inter_target {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) :
Metric.ball ((extChartAt I c) c) f.rOut = Metric.ball ((extChartAt I c) c) f.rOut (extChartAt I c).target
theorem SmoothBumpFunction.eqOn_source {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] :
Set.EqOn (↑f) (f.toContDiffBump (extChartAt I c)) (chartAt H c).source
theorem SmoothBumpFunction.eventuallyEq_of_mem_source {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) {x : M} [] (hx : x (chartAt H c).source) :
f =ᶠ[nhds x] f.toContDiffBump (extChartAt I c)
theorem SmoothBumpFunction.one_of_dist_le {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) {x : M} [] (hs : x (chartAt H c).source) (hd : dist ((extChartAt I c) x) ((extChartAt I c) c) f.rIn) :
f x = 1
theorem SmoothBumpFunction.support_eq_inter_preimage {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] :
= (chartAt H c).source (extChartAt I c) ⁻¹' Metric.ball ((extChartAt I c) c) f.rOut
theorem SmoothBumpFunction.isOpen_support {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] :
theorem SmoothBumpFunction.support_eq_symm_image {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] :
= (extChartAt I c).symm '' (Metric.ball ((extChartAt I c) c) f.rOut )
theorem SmoothBumpFunction.support_subset_source {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] :
(chartAt H c).source
theorem SmoothBumpFunction.image_eq_inter_preimage_of_subset_support {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] {s : Set M} (hs : ) :
(extChartAt I c) '' s = Metric.closedBall ((extChartAt I c) c) f.rOut (extChartAt I c).symm ⁻¹' s
theorem SmoothBumpFunction.mem_Icc {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) {x : M} [] :
f x Set.Icc 0 1
theorem SmoothBumpFunction.nonneg {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) {x : M} [] :
0 f x
theorem SmoothBumpFunction.le_one {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) {x : M} [] :
f x 1
theorem SmoothBumpFunction.eventuallyEq_one_of_dist_lt {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) {x : M} [] (hs : x (chartAt H c).source) (hd : dist ((extChartAt I c) x) ((extChartAt I c) c) < f.rIn) :
f =ᶠ[nhds x] 1
theorem SmoothBumpFunction.eventuallyEq_one {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] :
f =ᶠ[nhds c] 1
@[simp]
theorem SmoothBumpFunction.eq_one {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] :
f c = 1
theorem SmoothBumpFunction.support_mem_nhds {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] :
theorem SmoothBumpFunction.tsupport_mem_nhds {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] :
theorem SmoothBumpFunction.c_mem_support {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] :
theorem SmoothBumpFunction.nonempty_support {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] :
(Function.support f).Nonempty
theorem SmoothBumpFunction.isCompact_symm_image_closedBall {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] :
IsCompact ((extChartAt I c).symm '' (Metric.closedBall ((extChartAt I c) c) f.rOut ))
theorem SmoothBumpFunction.nhdsWithin_range_basis {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} :
(nhdsWithin ((extChartAt I c) c) (Set.range I)).HasBasis (fun (x : ) => True) fun (f : ) => Metric.closedBall ((extChartAt I c) c) f.rOut

Given a smooth bump function f : SmoothBumpFunction 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] (extChartAt I c c).

theorem SmoothBumpFunction.isClosed_image_of_isClosed {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] {s : Set M} (hsc : ) (hs : ) :
IsClosed ((extChartAt I c) '' s)
theorem SmoothBumpFunction.exists_r_pos_lt_subset_ball {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] {s : Set M} (hsc : ) (hs : ) :
rSet.Ioo 0 f.rOut, s (chartAt H c).source (extChartAt I c) ⁻¹' Metric.ball ((extChartAt 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.rOut), then there exists 0 < r < f.rOut such that s is a subset of the open ball of radius r. Formally, s ⊆ e.source ∩ e ⁻¹' (ball (e c) r), where e = extChartAt I c.

@[simp]
theorem SmoothBumpFunction.updateRIn_rOut {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) (r : ) (hr : r Set.Ioo 0 f.rOut) :
(f.updateRIn r hr).rOut = f.rOut
@[simp]
theorem SmoothBumpFunction.updateRIn_rIn {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) (r : ) (hr : r Set.Ioo 0 f.rOut) :
(f.updateRIn r hr).rIn = r
def SmoothBumpFunction.updateRIn {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) (r : ) (hr : r Set.Ioo 0 f.rOut) :

Replace rIn with another value in the interval (0, f.rOut).

Equations
• f.updateRIn r hr = { rIn := r, rOut := f.rOut, rIn_pos := , rIn_lt_rOut := , closedBall_subset := }
Instances For
@[simp]
theorem SmoothBumpFunction.support_updateRIn {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] {r : } (hr : r Set.Ioo 0 f.rOut) :
Function.support (f.updateRIn r hr) =
instance SmoothBumpFunction.instNonempty {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} :
Equations
• =
theorem SmoothBumpFunction.isClosed_symm_image_closedBall {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] [] :
IsClosed ((extChartAt I c).symm '' (Metric.closedBall ((extChartAt I c) c) f.rOut ))
theorem SmoothBumpFunction.tsupport_subset_symm_image_closedBall {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] [] :
tsupport f (extChartAt I c).symm '' (Metric.closedBall ((extChartAt I c) c) f.rOut )
theorem SmoothBumpFunction.tsupport_subset_extChartAt_source {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] [] :
tsupport f (extChartAt I c).source
theorem SmoothBumpFunction.tsupport_subset_chartAt_source {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] [] :
tsupport f (chartAt H c).source
theorem SmoothBumpFunction.hasCompactSupport {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] [] :
theorem SmoothBumpFunction.nhds_basis_tsupport {E : Type uE} [] {H : Type uH} [] (I : ) {M : Type uM} [] [] (c : M) [] [] :
(nhds c).HasBasis (fun (x : ) => True) fun (f : ) => 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 : SmoothBumpFunction I c.

theorem SmoothBumpFunction.nhds_basis_support {E : Type uE} [] {H : Type uH} [] (I : ) {M : Type uM} [] [] {c : M} [] [] {s : Set M} (hs : s nhds c) :
(nhds c).HasBasis (fun (f : ) => tsupport f s) fun (f : ) =>

Given s ∈ 𝓝 c, the supports of smooth bump functions f : SmoothBumpFunction 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 : SmoothBumpFunction I c such that tsupport f ⊆ s.

theorem SmoothBumpFunction.smooth {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] [] :
Smooth I f

A smooth bump function is infinitely smooth.

theorem SmoothBumpFunction.smoothAt {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] [] {x : M} :
SmoothAt I (↑f) x
theorem SmoothBumpFunction.continuous {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] [] :
theorem SmoothBumpFunction.smooth_smul {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {c : M} (f : ) [] [] {G : Type u_1} [] {g : MG} (hg : SmoothOn I g (chartAt H c).source) :
Smooth I fun (x : M) => f x g x

If f : SmoothBumpFunction 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.