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} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] (c : M) extends ContDiffBump (↑(extChartAt I c) c) : Type

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.

• rIn : ℝ
• rOut : ℝ
• rIn_pos : 0 < self.rIn
• rIn_lt_rOut : self.rIn < self.rOut
• closedBall_subset : Metric.closedBall (↑(extChartAt I c) c) self.rOut ∩ Set.range ↑I ⊆ (extChartAt I c).target

def SmoothBumpFunction.toFun {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {c : M} (f : SmoothBumpFunction I c) : M → ℝ

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

Equations

• ↑f = (chartAt H c).source.indicator (↑f.toContDiffBump ∘ ↑(extChartAt I c))

instance SmoothBumpFunction.instCoeFunForallReal {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {c : M} : CoeFun (SmoothBumpFunction I c) fun (x : SmoothBumpFunction I c) => M → ℝ

Equations

• SmoothBumpFunction.instCoeFunForallReal = { coe := SmoothBumpFunction.toFun }

theorem SmoothBumpFunction.coe_def {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {c : M} (f : SmoothBumpFunction I c) : ↑f = (chartAt H c).source.indicator (↑f.toContDiffBump ∘ ↑(extChartAt I c))

theorem SmoothBumpFunction.rOut_pos {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) : 0 < f.rOut

theorem SmoothBumpFunction.ball_subset {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) : Metric.ball (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I ⊆ (extChartAt I c).target

theorem SmoothBumpFunction.ball_inter_range_eq_ball_inter_target {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) : Metric.ball (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I = Metric.ball (↑(extChartAt I c) c) f.rOut ∩ (extChartAt I c).target

theorem SmoothBumpFunction.eqOn_source {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] : Set.EqOn (↑f) (↑f.toContDiffBump ∘ ↑(extChartAt I c)) (chartAt H c).source

theorem SmoothBumpFunction.eventuallyEq_of_mem_source {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) {x : M} [FiniteDimensional ℝ E] (hx : x ∈ (chartAt H c).source) : ↑f =ᶠ[nhds x] ↑f.toContDiffBump ∘ ↑(extChartAt I c)

theorem SmoothBumpFunction.one_of_dist_le {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) {x : M} [FiniteDimensional ℝ E] (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} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] : Function.support ↑f = (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' Metric.ball (↑(extChartAt I c) c) f.rOut

theorem SmoothBumpFunction.isOpen_support {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] : IsOpen (Function.support ↑f)

theorem SmoothBumpFunction.support_eq_symm_image {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] : Function.support ↑f = ↑(extChartAt I c).symm '' (Metric.ball (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I)

theorem SmoothBumpFunction.support_subset_source {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] : Function.support ↑f ⊆ (chartAt H c).source

theorem SmoothBumpFunction.image_eq_inter_preimage_of_subset_support {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] {s : Set M} (hs : s ⊆ Function.support ↑f) : ↑(extChartAt I c) '' s = Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I ∩ ↑(extChartAt I c).symm ⁻¹' s

theorem SmoothBumpFunction.mem_Icc {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) {x : M} [FiniteDimensional ℝ E] : ↑f x ∈ Set.Icc 0 1

theorem SmoothBumpFunction.nonneg {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) {x : M} [FiniteDimensional ℝ E] : 0 ≤ ↑f x

theorem SmoothBumpFunction.le_one {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) {x : M} [FiniteDimensional ℝ E] : ↑f x ≤ 1

theorem SmoothBumpFunction.eventuallyEq_one_of_dist_lt {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) {x : M} [FiniteDimensional ℝ E] (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} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] : ↑f =ᶠ[nhds c] 1

@[simp]

theorem SmoothBumpFunction.eq_one {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] : ↑f c = 1

theorem SmoothBumpFunction.support_mem_nhds {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] : Function.support ↑f ∈ nhds c

theorem SmoothBumpFunction.tsupport_mem_nhds {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] : tsupport ↑f ∈ nhds c

theorem SmoothBumpFunction.c_mem_support {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] : c ∈ Function.support ↑f

theorem SmoothBumpFunction.nonempty_support {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] : (Function.support ↑f).Nonempty

theorem SmoothBumpFunction.isCompact_symm_image_closedBall {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] : IsCompact (↑(extChartAt I c).symm '' (Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I))

theorem SmoothBumpFunction.nhdsWithin_range_basis {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} : (nhdsWithin (↑(extChartAt I c) c) (Set.range ↑I)).HasBasis (fun (x : SmoothBumpFunction I c) => True) fun (f : SmoothBumpFunction I c) => Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I

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} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] {s : Set M} (hsc : IsClosed s) (hs : s ⊆ Function.support ↑f) : IsClosed (↑(extChartAt I c) '' s)

theorem SmoothBumpFunction.exists_r_pos_lt_subset_ball {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] {s : Set M} (hsc : IsClosed s) (hs : s ⊆ Function.support ↑f) : ∃ r ∈ Set.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.

def SmoothBumpFunction.updateRIn {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) (r : ℝ) (hr : r ∈ Set.Ioo 0 f.rOut) : SmoothBumpFunction I c

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 := ⋯ }

@[simp]

theorem SmoothBumpFunction.updateRIn_rOut {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) (r : ℝ) (hr : r ∈ Set.Ioo 0 f.rOut) : (f.updateRIn r hr).rOut = f.rOut

@[simp]

theorem SmoothBumpFunction.updateRIn_rIn {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) (r : ℝ) (hr : r ∈ Set.Ioo 0 f.rOut) : (f.updateRIn r hr).rIn = r

@[simp]

theorem SmoothBumpFunction.support_updateRIn {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] {r : ℝ} (hr : r ∈ Set.Ioo 0 f.rOut) : Function.support ↑(f.updateRIn r hr) = Function.support ↑f

instance SmoothBumpFunction.instNonempty {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} : Nonempty (SmoothBumpFunction I c)

theorem SmoothBumpFunction.isClosed_symm_image_closedBall {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] [T2Space M] : IsClosed (↑(extChartAt I c).symm '' (Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I))

theorem SmoothBumpFunction.tsupport_subset_symm_image_closedBall {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] [T2Space M] : tsupport ↑f ⊆ ↑(extChartAt I c).symm '' (Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I)

theorem SmoothBumpFunction.tsupport_subset_extChartAt_source {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] [T2Space M] : tsupport ↑f ⊆ (extChartAt I c).source

theorem SmoothBumpFunction.tsupport_subset_chartAt_source {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] [T2Space M] : tsupport ↑f ⊆ (chartAt H c).source

theorem SmoothBumpFunction.hasCompactSupport {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] [T2Space M] : HasCompactSupport ↑f

theorem SmoothBumpFunction.nhds_basis_tsupport {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] (c : M) [FiniteDimensional ℝ E] [T2Space M] : (nhds c).HasBasis (fun (x : SmoothBumpFunction I c) => True) fun (f : SmoothBumpFunction 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 : SmoothBumpFunction I c.

theorem SmoothBumpFunction.nhds_basis_support {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} [FiniteDimensional ℝ E] [T2Space M] {s : Set M} (hs : s ∈ nhds c) : (nhds c).HasBasis (fun (f : SmoothBumpFunction I c) => tsupport ↑f ⊆ s) fun (f : SmoothBumpFunction I c) => Function.support ↑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.contMDiff {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] : ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ ↑f

A smooth bump function is infinitely smooth.

theorem SmoothBumpFunction.contMDiffAt {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] {x : M} : ContMDiffAt I (modelWithCornersSelf ℝ ℝ) (↑⊤) (↑f) x

theorem SmoothBumpFunction.continuous {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] : Continuous ↑f

theorem SmoothBumpFunction.contMDiff_smul {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] {G : Type u_1} [NormedAddCommGroup G] [NormedSpace ℝ G] {g : M → G} (hg : ContMDiffOn I (modelWithCornersSelf ℝ G) (↑⊤) g (chartAt H c).source) : ContMDiff I (modelWithCornersSelf ℝ G) ↑⊤ 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.