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
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
A version of ContDiffBump.nonneg
with x
explicit
ContDiffBump
is 𝒞ⁿ
in all its arguments.
ContDiffBump
is 𝒞ⁿ
in all its arguments.