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.,

• they can be used to construct a smooth partition of unity which is a very useful tool;
• they can be used to approximate a continuous function by infinitely smooth functions.

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

• f is equal to 1 in Metric.closedBall c f.rIn;
• support f = Metric.ball c f.rOut;
• 0 ≤ f x ≤ 1 for all x.

Main Definitions

• ContDiffBump (c : E): a structure holding data needed to construct an infinitely smooth bump function.
• ContDiffBumpBase (E : Type*): a family of infinitely smooth bump functions that can be used to construct coercion of a ContDiffBump (c : E) to a function.
• HasContDiffBump (E : Type*): a typeclass saying that E has a ContDiffBumpBase. Two instances of this typeclass (for inner product spaces and for finite dimensional spaces) are provided elsewhere.

Keywords

smooth function, smooth bump function

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

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

• f is equal to 1 in Metric.closedBall c f.rIn;
• support f = Metric.ball c f.rOut;
• 0 ≤ f x ≤ 1 for all x.

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.

• rIn : ℝ

  real numbers 0 < rIn < rOut

• rOut : ℝ

  real numbers 0 < rIn < rOut

• rIn_pos : 0 < self.rIn
• rIn_lt_rOut : self.rIn < self.rOut

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?

• toFun : ℝ → E → ℝ

  The function underlying this family of bump functions

• mem_Icc : ∀ (R : ℝ) (x : E), self.toFun R x ∈ Set.Icc 0 1
• symmetric : ∀ (R : ℝ) (x : E), self.toFun R (-x) = self.toFun R x
• smooth : ContDiffOn ℝ ⊤ (Function.uncurry self.toFun) (Set.Ioi 1 ×ˢ Set.univ)
• eq_one : ∀ (R : ℝ), 1 < R → ∀ (x : E), ‖x‖ ≤ 1 → self.toFun R x = 1
• support : ∀ (R : ℝ), 1 < R → Function.support (self.toFun R) = Metric.ball 0 R

class HasContDiffBump (E : Type u_3) [NormedAddCommGroup E] [NormedSpace ℝ E] : Prop

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.

• out : Nonempty (ContDiffBumpBase E)

def someContDiffBumpBase (E : Type u_3) [NormedAddCommGroup E] [NormedSpace ℝ E] [hb : HasContDiffBump E] : ContDiffBumpBase E

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

• someContDiffBumpBase E = ⋯.some

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) : Inhabited (ContDiffBump c)

Equations

• ContDiffBump.instInhabited c = { default := { rIn := 1, rOut := 2, rIn_pos := ContDiffBump.instInhabited.proof_2, rIn_lt_rOut := ContDiffBump.instInhabited.proof_3 } }

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

• ↑f = (someContDiffBumpBase E).toFun (f.rOut / f.rIn) ∘ fun (x : E) => f.rIn⁻¹ • (x - c)

instance ContDiffBump.instCoeFunForallReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] {c : E} : CoeFun (ContDiffBump c) fun (x : ContDiffBump c) => E → ℝ

Equations

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

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.support_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) : Function.support ↑f = Metric.ball c f.rOut

theorem ContDiffBump.tsupport_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) : tsupport ↑f = Metric.closedBall c f.rOut

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 ContDiffBump.hasCompactSupport {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) [FiniteDimensional ℝ E] : HasCompactSupport ↑f

theorem ContDiffBump.eventuallyEq_one_of_mem_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) {x : E} (h : x ∈ Metric.ball c f.rIn) : ↑f =ᶠ[nhds x] 1

theorem ContDiffBump.eventuallyEq_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) : ↑f =ᶠ[nhds c] 1

theorem ContDiffWithinAt.contDiffBump {E : Type u_1} {X : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup X] [NormedSpace ℝ X] [HasContDiffBump E] {n : ℕ∞} {c g : X → E} {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 : X → E} {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 : X → E} {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

theorem ContDiffBump.continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) : Continuous ↑f