# Documentation

Mathlib.Analysis.SpecialFunctions.SmoothTransition

# 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));

def expNegInvGlue (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
theorem expNegInvGlue.zero_of_nonpos {x : } (hx : x 0) :

The function expNegInvGlue vanishes on (-∞, 0].

@[simp]
theorem expNegInvGlue.pos_of_pos {x : } (hx : 0 < x) :

The function expNegInvGlue is positive on (0, +∞).

theorem expNegInvGlue.nonneg (x : ) :

The function expNegInvGlue is nonnegative.

@[simp]

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

theorem expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul (p : ) (x : ) :
HasDerivAt (fun x => ) (Polynomial.eval x⁻¹ (Polynomial.X ^ 2 * (p - Polynomial.derivative p)) * ) x

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
@[simp]

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.

theorem Real.smoothTransition.pos_of_pos {x : } (h : 0 < x) :