# 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 for`x ≤ 0`

and is strictly positive otherwise; it is given by`x ↦ exp (-1/x)`

for`x > 0`

;`Real.smoothTransition`

is equal to zero for`x ≤ 0`

and is equal to one for`x ≥ 1`

; it is given by`expNegInvGlue 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`

.

## Equations

- expNegInvGlue x = if x ≤ 0 then 0 else (-x⁻¹).exp

## 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(p-p')}$. 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`

.

## Equations

- x.smoothTransition = expNegInvGlue x / (expNegInvGlue x + expNegInvGlue (1 - x))

## 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`

.