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:

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.

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

    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.

    Equations
    Instances For
      theorem Real.smoothTransition.one_of_one_le {x : } (h : 1 x) :
      x.smoothTransition = 1
      @[simp]
      theorem Real.smoothTransition.zero_iff_nonpos {x : } :
      x.smoothTransition = 0 x 0
      theorem Real.smoothTransition.zero_of_nonpos {x : } (h : x 0) :
      x.smoothTransition = 0
      @[simp]
      theorem Real.smoothTransition.projIcc {x : } :
      (↑(Set.projIcc 0 1 x)).smoothTransition = x.smoothTransition

      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.le_one (x : ) :
      x.smoothTransition 1
      theorem Real.smoothTransition.nonneg (x : ) :
      0 x.smoothTransition
      theorem Real.smoothTransition.lt_one_of_lt_one {x : } (h : x < 1) :
      x.smoothTransition < 1
      theorem Real.smoothTransition.pos_of_pos {x : } (h : 0 < x) :
      0 < x.smoothTransition