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 to1
inMetric.closedBall c f.rIn
;support f = Metric.ball c f.rOut
;0 ≤ f x ≤ 1
for allx
.
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 aContDiffBump (c : E)
to a function.HasContDiffBump (E : Type*)
: a typeclass saying thatE
has aContDiffBumpBase
. Two instances of this typeclass (for inner product spaces and for finite dimensional spaces) are provided elsewhere.
Keywords #
smooth function, smooth bump function
f : ContDiffBump c
, where c
is a point in a normed vector space, is a
bundled smooth function such that
f
is equal to1
inMetric.closedBall c f.rIn
;support f = Metric.ball c f.rOut
;0 ≤ f x ≤ 1
for allx
.
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
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
?
The function underlying this family of bump functions
- smooth : ContDiffOn ℝ (↑⊤) (Function.uncurry self.toFun) (Set.Ioi 1 ×ˢ Set.univ)
- support (R : ℝ) : 1 < R → Function.support (self.toFun R) = Metric.ball 0 R
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.
- out : Nonempty (ContDiffBumpBase E)
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
- someContDiffBumpBase E = ⋯.some
Instances For
Equations
- ContDiffBump.instInhabited c = { default := { rIn := 1, rOut := 2, rIn_pos := ContDiffBump.instInhabited.proof_2, rIn_lt_rOut := ContDiffBump.instInhabited.proof_3 } }
The function defined by f : ContDiffBump c
. Use automatic coercion to
function instead.
Instances For
Equations
- ContDiffBump.instCoeFunForallReal = { coe := ContDiffBump.toFun }
A version of ContDiffBump.nonneg
with x
explicit
ContDiffBump
is 𝒞ⁿ
in all its arguments.
ContDiffBump
is 𝒞ⁿ
in all its arguments.