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.

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)

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.

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

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