Infinitely smooth bump function #
In this file we construct several infinitely smooth functions with properties that an analytic function cannot have:
-
exp_neg_inv_glue
is equal to zero forx ≤ 0
and is strictly positive otherwise; it is given byx ↦ exp (-1/x)
forx > 0
; -
real.smooth_transition
is equal to zero forx ≤ 0
and is equal to one forx ≥ 1
; it is given byexp_neg_inv_glue x / (exp_neg_inv_glue x + exp_neg_inv_glue (1 - x))
; -
f : cont_diff_bump_of_inner c
, wherec
is a point in an inner product space, is a bundled smooth function such thatf
is equal to1
inmetric.closed_ball c f.r
;support f = metric.ball c f.R
;0 ≤ f x ≤ 1
for allx
.
The structure
cont_diff_bump_of_inner
contains the data required to construct the function: real numbersr
,R
, and proofs of0 < r < R
. The function itself is available throughcoe_fn
. -
If
f : cont_diff_bump_of_inner c
andμ
is a measure on the domain off
, thenf.normed μ
is a smooth bump function with integral1
w.r.t.μ
. -
f : cont_diff_bump c
, wherec
is a point in a finite dimensional real vector space, is a bundled smooth function such thatf
is equal to1
ineuclidean.closed_ball c f.r
;support f = euclidean.ball c f.R
;0 ≤ f x ≤ 1
for allx
.
The structure
cont_diff_bump
contains the data required to construct the function: real numbersr
,R
, and proofs of0 < r < R
. The function itself is available throughcoe_fn
.
exp_neg_inv_glue
is the real function given by x ↦ exp (-1/x)
for x > 0
and 0
for x ≤ 0
. It is a basic building block to construct smooth partitions of unity. Its main property
is that it vanishes for x ≤ 0
, it is positive for x > 0
, and the junction between the two
behaviors is flat enough to retain smoothness. The fact that this function is C^∞
is proved in
exp_neg_inv_glue.smooth
.
Our goal is to prove that exp_neg_inv_glue
is C^∞
. For this, we compute its successive
derivatives for x > 0
. The n
-th derivative is of the form P_aux n (x) exp(-1/x) / x^(2 n)
,
where P_aux n
is computed inductively.
Equations
- exp_neg_inv_glue.P_aux (n + 1) = polynomial.X ^ 2 * ⇑polynomial.derivative (exp_neg_inv_glue.P_aux n) + (1 - ⇑polynomial.C ↑(2 * n) * polynomial.X) * exp_neg_inv_glue.P_aux n
- exp_neg_inv_glue.P_aux 0 = 1
Formula for the n
-th derivative of exp_neg_inv_glue
, as an auxiliary function f_aux
.
Equations
- exp_neg_inv_glue.f_aux n x = ite (x ≤ 0) 0 (polynomial.eval x (exp_neg_inv_glue.P_aux n) * real.exp (-x⁻¹) / x ^ (2 * n))
The 0
-th auxiliary function f_aux 0
coincides with exp_neg_inv_glue
, by definition.
For positive values, the derivative of the n
-th auxiliary function f_aux n
(given in this statement in unfolded form) is the n+1
-th auxiliary function, since
the polynomial P_aux (n+1)
was chosen precisely to ensure this.
For positive values, the derivative of the n
-th auxiliary function f_aux n
is the n+1
-th auxiliary function.
To get differentiability at 0
of the auxiliary functions, we need to know that their limit
is 0
, to be able to apply general differentiability extension theorems. This limit is checked in
this lemma.
Deduce from the limiting behavior at 0
of its derivative and general differentiability
extension theorems that the auxiliary function f_aux n
is differentiable at 0
,
with derivative 0
.
At every point, the auxiliary function f_aux n
has a derivative which is
equal to f_aux (n+1)
.
The successive derivatives of the auxiliary function f_aux 0
are the
functions f_aux n
, by induction.
The function exp_neg_inv_glue
is smooth.
The function exp_neg_inv_glue
vanishes on (-∞, 0]
.
The function exp_neg_inv_glue
is positive on (0, +∞)
.
The function exp_neg_inv_glue` is nonnegative.
An infinitely smooth function f : ℝ → ℝ
such that f x = 0
for x ≤ 0
,
f x = 1
for 1 ≤ x
, and 0 < f x < 1
for 0 < x < 1
.
Equations
- x.smooth_transition = exp_neg_inv_glue x / (exp_neg_inv_glue x + exp_neg_inv_glue (1 - x))
f : cont_diff_bump_of_inner c
, where c
is a point in an inner product space, is a
bundled smooth function such that
f
is equal to1
inmetric.closed_ball c f.r
;support f = metric.ball c f.R
;0 ≤ f x ≤ 1
for allx
.
The structure cont_diff_bump_of_inner
contains the data required to construct the function:
real numbers r
, R
, and proofs of 0 < r < R
. The function itself is available through
coe_fn
.
Instances for cont_diff_bump_of_inner
- cont_diff_bump_of_inner.has_sizeof_inst
- cont_diff_bump_of_inner.inhabited
- cont_diff_bump_of_inner.has_coe_to_fun
The function defined by f : cont_diff_bump_of_inner c
. Use automatic coercion to
function instead.
Equations
- f.to_fun = λ (x : E), ((f.R - has_dist.dist x c) / (f.R - f.r)).smooth_transition
Equations
A version of cont_diff_bump_of_inner.nonneg
with x
explicit
cont_diff_bump
is 𝒞ⁿ
in all its arguments.
A bump function normed so that ∫ x, f.normed μ x ∂μ = 1
.
- to_cont_diff_bump_of_inner : cont_diff_bump_of_inner (⇑to_euclidean c)
f : cont_diff_bump c
, where c
is a point in a finite dimensional real vector space, is
a bundled smooth function such that
f
is equal to1
ineuclidean.closed_ball c f.r
;support f = euclidean.ball c f.R
;0 ≤ f x ≤ 1
for allx
.
The structure cont_diff_bump
contains the data required to construct the function: real
numbers r
, R
, and proofs of 0 < r < R
. The function itself is available through coe_fn
.
Instances for cont_diff_bump
- cont_diff_bump.has_sizeof_inst
- cont_diff_bump.has_coe_to_fun
- cont_diff_bump.inhabited
The function defined by f : cont_diff_bump c
. Use automatic coercion to function
instead.
Equations
Equations
Equations
If E
is a finite dimensional normed space over ℝ
, then for any point x : E
and its
neighborhood s
there exists an infinitely smooth function with the following properties:
f y = 1
in a neighborhood ofx
;f y = 0
outside ofs
;- moreover,
tsupport f ⊆ s
andf
has compact support; f y ∈ [0, 1]
for ally
.
This lemma is a simple wrapper around lemmas about bundled smooth bump functions, see
cont_diff_bump
.