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 = 1in the closed ball of radiusf.rIncentered atc;f x = 0outside of the ball of radiusf.rOutcentered atc;0 ≤ f x ≤ 1for allx.
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) :
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 = 1in the closed ball of radiusf.rIncentered atf.c;f x = 0outside of the ball of radiusf.rOutcentered 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 extChartAt I f.c and are given as lemmas in the SmoothBumpFunction
namespace.
- rIn_lt_rOut : self.rIn < self.rOut
- closedBall_subset : Metric.closedBall (↑(extChartAt I c) c) self.rOut ∩ Set.range ↑I ⊆ (extChartAt I c).target
Instances For
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))
Instances For
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]
:
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)
:
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]
:
@[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]
:
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)
:
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.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.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.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]
:
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]
:
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]
[SmoothManifoldWithCorners I M]
:
ContMDiff I (modelWithCornersSelf ℝ ℝ) ⊤ ↑f
A smooth bump function is infinitely smooth.
@[deprecated SmoothBumpFunction.contMDiff]
theorem
SmoothBumpFunction.smooth
{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]
[SmoothManifoldWithCorners I M]
:
ContMDiff I (modelWithCornersSelf ℝ ℝ) ⊤ ↑f
Alias of SmoothBumpFunction.contMDiff.
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]
[SmoothManifoldWithCorners I M]
{x : M}
:
ContMDiffAt I (modelWithCornersSelf ℝ ℝ) ⊤ (↑f) x
@[deprecated SmoothBumpFunction.contMDiffAt]
theorem
SmoothBumpFunction.smoothAt
{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]
[SmoothManifoldWithCorners I M]
{x : M}
:
ContMDiffAt I (modelWithCornersSelf ℝ ℝ) ⊤ (↑f) x
Alias of SmoothBumpFunction.contMDiffAt.
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]
[SmoothManifoldWithCorners 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]
[SmoothManifoldWithCorners 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.
@[deprecated SmoothBumpFunction.contMDiff_smul]
theorem
SmoothBumpFunction.smooth_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]
[SmoothManifoldWithCorners 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
Alias of SmoothBumpFunction.contMDiff_smul.
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.