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.

theorem expNegInvGlue.zero_of_nonpos {x : ℝ} (hx : x ≤ 0) : expNegInvGlue x = 0

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

@[simp]

theorem expNegInvGlue.zero : expNegInvGlue 0 = 0

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

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

theorem expNegInvGlue.nonneg (x : ℝ) : 0 ≤ expNegInvGlue x

The function expNegInvGlue is nonnegative.

@[simp]

theorem expNegInvGlue.zero_iff_nonpos {x : ℝ} : expNegInvGlue x = 0 ↔ x ≤ 0

theorem expNegInvGlue.monotone : Monotone expNegInvGlue

theorem expNegInvGlue.not_analyticAt_zero : ¬AnalyticAt ℝ expNegInvGlue 0

The function expNegInvGlue is not analytic at 0.

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

theorem expNegInvGlue.tendsto_polynomial_inv_mul_zero (p : Polynomial ℝ) : Filter.Tendsto (fun (x : ℝ) => Polynomial.eval x⁻¹ p * expNegInvGlue x) (nhds 0) (nhds 0)

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

theorem expNegInvGlue.differentiable_polynomial_eval_inv_mul (p : Polynomial ℝ) : Differentiable ℝ fun (x : ℝ) => Polynomial.eval x⁻¹ p * expNegInvGlue x

theorem expNegInvGlue.continuous_polynomial_eval_inv_mul (p : Polynomial ℝ) : Continuous fun (x : ℝ) => Polynomial.eval x⁻¹ p * expNegInvGlue x

theorem expNegInvGlue.contDiff_polynomial_eval_inv_mul {n : ℕ∞} (p : Polynomial ℝ) : ContDiff ℝ ↑n fun (x : ℝ) => Polynomial.eval x⁻¹ p * expNegInvGlue x

theorem expNegInvGlue.contDiff {n : ℕ∞} : ContDiff ℝ (↑n) expNegInvGlue

The function expNegInvGlue is smooth.

def Real.smoothTransition (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.

theorem Real.smoothTransition.pos_denom (x : ℝ) : 0 < expNegInvGlue x + expNegInvGlue (1 - x)

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.zero : smoothTransition 0 = 0

@[simp]

theorem Real.smoothTransition.one : smoothTransition 1 = 1

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

@[simp]

theorem Real.smoothTransition.eq_one_iff_one_le {x : ℝ} : x.smoothTransition = 1 ↔ 1 ≤ x

theorem Real.smoothTransition.contDiff {n : ℕ∞} : ContDiff ℝ (↑n) smoothTransition

theorem Real.smoothTransition.contDiffAt {x : ℝ} {n : ℕ∞} : ContDiffAt ℝ (↑n) smoothTransition x

theorem Real.smoothTransition.continuous : Continuous smoothTransition

theorem Real.smoothTransition.continuousAt {x : ℝ} : ContinuousAt smoothTransition x

theorem Real.smoothTransition.monotone : Monotone smoothTransition