Infinitely smooth transition function #
In this file we construct two infinitely smooth functions with properties that an analytic function cannot have:

expNegInvGlue
is equal to zero forx ≤ 0
and is strictly positive otherwise; it is given byx ↦ exp (1/x)
forx > 0
; 
Real.smoothTransition
is equal to zero forx ≤ 0
and is equal to one forx ≥ 1
; it is given byexpNegInvGlue x / (expNegInvGlue x + expNegInvGlue (1  x))
;
expNegInvGlue
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
expNegInvGlue.contDiff
.
Instances For
The function expNegInvGlue
vanishes on (∞, 0]
.
The function expNegInvGlue
is positive on (0, +∞)
.
The function expNegInvGlue
is nonnegative.
Smoothness of expNegInvGlue
#
Porting note: Yury Kudryashov rewrote the proof while porting, generalizing auxiliary lemmas and removing some auxiliary definitions.
In this section we prove that the function f = expNegInvGlue
is infinitely smooth. To do
this, we show that $g_p(x)=p(x^{1})f(x)$ is infinitely smooth for any polynomial p
with real
coefficients. First we show that $g_p(x)$ tends to zero at zero, then we show that it is
differentiable with derivative $g_p'=g_{x^2(pp')}$. Finally, we prove smoothness of $g_p$ by
induction, then deduce smoothness of $f$ by setting $p=1$.
Our function tends to zero at zero faster than any $P(x^{1})$, $P∈ℝ[X]$, tends to infinity.
The function expNegInvGlue
is smooth.
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
.
Instances For
Since Real.smoothTransition
is constant on $(∞, 0]$ and $[1, ∞)$, applying it to the
projection of x : ℝ
to $[0, 1]$ gives the same result as applying it to x
.