Documentation

Mathlib.Geometry.Manifold.BumpFunction

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:

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 :

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} [NormedAddCommGroup E] [NormedSpace E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (self : SmoothBumpFunction I c) :
    Metric.closedBall ((extChartAt I c) c) self.rOut Set.range I (extChartAt I c).target

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

    Equations
    Instances For
      Equations
      • SmoothBumpFunction.instCoeFunForallReal = { coe := SmoothBumpFunction.toFun }
      theorem SmoothBumpFunction.coe_def {E : Type uE} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {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.eqOn_source {E : Type uE} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) :
      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] [FiniteDimensional 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} (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] [FiniteDimensional 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} (hs : x (chartAt H c).source) (hd : dist ((extChartAt I c) x) ((extChartAt I c) c) f.rIn) :
      f x = 1
      theorem SmoothBumpFunction.mem_Icc {E : Type uE} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional 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} :
      f x Set.Icc 0 1
      theorem SmoothBumpFunction.nonneg {E : Type uE} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional 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} :
      0 f x
      theorem SmoothBumpFunction.le_one {E : Type uE} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional 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} :
      f x 1
      theorem SmoothBumpFunction.eventuallyEq_one_of_dist_lt {E : Type uE} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional 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} (hs : x (chartAt H c).source) (hd : dist ((extChartAt I c) x) ((extChartAt I c) c) < f.rIn) :
      f =ᶠ[nhds x] 1
      @[simp]
      theorem SmoothBumpFunction.eq_one {E : Type uE} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) :
      f c = 1
      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.exists_r_pos_lt_subset_ball {E : Type uE} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) {s : Set M} (hsc : IsClosed s) (hs : s Function.support f) :
      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_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
      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.support_updateRIn {E : Type uE} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional 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) :
        Function.support (f.updateRIn r hr) = Function.support f
        theorem SmoothBumpFunction.nhds_basis_tsupport {E : Type uE} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] (c : M) [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] [FiniteDimensional E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} [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.

        A smooth bump function is infinitely smooth.

        theorem SmoothBumpFunction.smooth_smul {E : Type uE} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [T2Space M] [SmoothManifoldWithCorners I M] {G : Type u_1} [NormedAddCommGroup G] [NormedSpace G] {g : MG} (hg : SmoothOn I (modelWithCornersSelf G) g (chartAt H c).source) :
        Smooth 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.