Documentation

Mathlib.Analysis.Calculus.BumpFunction.Basic

Infinitely smooth "bump" functions #

A smooth bump function is an infinitely smooth function f : E → ℝ supported on a ball that is equal to 1 on a ball of smaller radius.

These functions have many uses in real analysis. E.g.,

There are two classes of spaces where bump functions are guaranteed to exist: inner product spaces and finite-dimensional spaces.

In this file we define a typeclass HasContDiffBump saying that a normed space has a family of smooth bump functions with certain properties.

We also define a structure ContDiffBump that holds the center and radii of the balls from above. An element f : ContDiffBump c can be coerced to a function which is an infinitely smooth function such that

Main Definitions #

Keywords #

smooth function, smooth bump function

structure ContDiffBump {E : Type u_1} (c : E) :

f : ContDiffBump c, where c is a point in a normed vector space, is a bundled smooth function such that

The structure ContDiffBump contains the data required to construct the function: real numbers rIn, rOut, and proofs of 0 < rIn < rOut. The function itself is available through CoeFun when the space is nice enough, i.e., satisfies the HasContDiffBump typeclass.

Instances For
    structure ContDiffBumpBase (E : Type u_3) [NormedAddCommGroup E] [NormedSpace E] :
    Type u_3

    The base function from which one will construct a family of bump functions. One could add more properties if they are useful and satisfied in the examples of inner product spaces and finite-dimensional vector spaces, notably derivative norm control in terms of R - 1.

    TODO: do we ever need f x = 1 ↔ ‖x‖ ≤ 1?

    Instances For

      A class registering that a real vector space admits bump functions. This will be instantiated first for inner product spaces, and then for finite-dimensional normed spaces. We use a specific class instead of Nonempty (ContDiffBumpBase E) for performance reasons.

      Instances

        In a space with C^∞ bump functions, register some function that will be used as a basis to construct bump functions of arbitrary size around any point.

        Equations
        Instances For
          theorem ContDiffBump.rOut_pos {E : Type u_1} {c : E} (f : ContDiffBump c) :
          0 < f.rOut
          theorem ContDiffBump.one_lt_rOut_div_rIn {E : Type u_1} {c : E} (f : ContDiffBump c) :
          1 < f.rOut / f.rIn
          instance ContDiffBump.instInhabited {E : Type u_1} (c : E) :
          Equations
          def ContDiffBump.toFun {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) :
          E

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

          Equations
          Instances For
            theorem ContDiffBump.apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) (x : E) :
            f x = (someContDiffBumpBase E).toFun (f.rOut / f.rIn) (f.rIn⁻¹ (x - c))
            theorem ContDiffBump.sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) (x : E) :
            f (c - x) = f (c + x)
            theorem ContDiffBump.neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] (f : ContDiffBump 0) (x : E) :
            f (-x) = f x
            theorem ContDiffBump.one_of_mem_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) {x : E} (hx : x Metric.closedBall c f.rIn) :
            f x = 1
            theorem ContDiffBump.nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) {x : E} :
            0 f x
            theorem ContDiffBump.nonneg' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) (x : E) :
            0 f x

            A version of ContDiffBump.nonneg with x explicit

            theorem ContDiffBump.le_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) {x : E} :
            f x 1
            theorem ContDiffBump.pos_of_mem_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) {x : E} (hx : x Metric.ball c f.rOut) :
            0 < f x
            theorem ContDiffBump.zero_of_le_dist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) {x : E} (hx : f.rOut dist x c) :
            f x = 0
            theorem ContDiffWithinAt.contDiffBump {E : Type u_1} {X : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup X] [NormedSpace X] [HasContDiffBump E] {n : ℕ∞} {c g : XE} {s : Set X} {f : (x : X) → ContDiffBump (c x)} {x : X} (hc : ContDiffWithinAt (↑n) c s x) (hr : ContDiffWithinAt (↑n) (fun (x : X) => (f x).rIn) s x) (hR : ContDiffWithinAt (↑n) (fun (x : X) => (f x).rOut) s x) (hg : ContDiffWithinAt (↑n) g s x) :
            ContDiffWithinAt (↑n) (fun (x : X) => (f x) (g x)) s x

            ContDiffBump is 𝒞ⁿ in all its arguments.

            theorem ContDiffAt.contDiffBump {E : Type u_1} {X : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup X] [NormedSpace X] [HasContDiffBump E] {n : ℕ∞} {c g : XE} {f : (x : X) → ContDiffBump (c x)} {x : X} (hc : ContDiffAt (↑n) c x) (hr : ContDiffAt (↑n) (fun (x : X) => (f x).rIn) x) (hR : ContDiffAt (↑n) (fun (x : X) => (f x).rOut) x) (hg : ContDiffAt (↑n) g x) :
            ContDiffAt (↑n) (fun (x : X) => (f x) (g x)) x

            ContDiffBump is 𝒞ⁿ in all its arguments.

            theorem ContDiff.contDiffBump {E : Type u_1} {X : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup X] [NormedSpace X] [HasContDiffBump E] {n : ℕ∞} {c g : XE} {f : (x : X) → ContDiffBump (c x)} (hc : ContDiff (↑n) c) (hr : ContDiff n fun (x : X) => (f x).rIn) (hR : ContDiff n fun (x : X) => (f x).rOut) (hg : ContDiff (↑n) g) :
            ContDiff n fun (x : X) => (f x) (g x)
            theorem ContDiffBump.contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) {n : ℕ∞} :
            ContDiff n f
            theorem ContDiffBump.contDiffAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) {x : E} {n : ℕ∞} :
            ContDiffAt (↑n) (↑f) x
            theorem ContDiffBump.contDiffWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) {x : E} {n : ℕ∞} {s : Set E} :
            ContDiffWithinAt (↑n) (↑f) s x