Infinitely smooth transition function #

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

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

    theorem expNegInvGlue.pos_of_pos {x : } (hx : 0 < x) :

    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.

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

    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.