Smoothness of specific functions

The real function exp_neg_inv_glue given by x ↦ exp (-1/x) for x > 0 and 0 for x ≤ 0 is a basic building block to construct smooth partitions of unity. We prove that it is C^∞ in exp_neg_inv_glue.smooth.

source

def exp_neg_inv_glue :

ℝ → ℝ

exp_neg_inv_glue is the real function given by x ↦ exp (-1/x) for x > 0 and 0 for x ≤ 0. 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 exp_neg_inv_glue.smooth.

Equations

exp_neg_inv_glue x = ite (x ≤ 0) 0 (real.exp (-x⁻¹))

source

def exp_neg_inv_glue.P_aux :

ℕ → polynomial ℝ

Our goal is to prove that exp_neg_inv_glue is C^∞. For this, we compute its successive derivatives for x > 0. The n-th derivative is of the form P_aux n (x) exp(-1/x) / x^(2 n), where P_aux n is computed inductively.

Equations

exp_neg_inv_glue.P_aux (n + 1) = polynomial.X ^ 2 * (exp_neg_inv_glue.P_aux n).derivative + (1 - ⇑polynomial.C ↑(2 * n) * polynomial.X) * exp_neg_inv_glue.P_aux n
exp_neg_inv_glue.P_aux 0 = 1

source

def exp_neg_inv_glue.f_aux :

ℕ → ℝ → ℝ

Formula for the n-th derivative of exp_neg_inv_glue, as an auxiliary function f_aux.

Equations

exp_neg_inv_glue.f_aux n x = ite (x ≤ 0) 0 (polynomial.eval x (exp_neg_inv_glue.P_aux n) * real.exp (-x⁻¹) / x ^ (2 * n))

source

theorem exp_neg_inv_glue.f_aux_zero_eq :

exp_neg_inv_glue.f_aux 0 = exp_neg_inv_glue

The 0-th auxiliary function f_aux 0 coincides with exp_neg_inv_glue, by definition.

source

theorem exp_neg_inv_glue.f_aux_deriv (n : ℕ) (x : ℝ) :

x ≠ 0 → has_deriv_at (λ (x : ℝ), polynomial.eval x (exp_neg_inv_glue.P_aux n) * real.exp (-x⁻¹) / x ^ (2 * n)) (polynomial.eval x (exp_neg_inv_glue.P_aux (n + 1)) * real.exp (-x⁻¹) / x ^ (2 * (n + 1))) x

For positive values, the derivative of the n-th auxiliary function f_aux n (given in this statement in unfolded form) is the n+1-th auxiliary function, since the polynomial P_aux (n+1) was chosen precisely to ensure this.

source

theorem exp_neg_inv_glue.f_aux_deriv_pos (n : ℕ) (x : ℝ) :

0 < x → has_deriv_at (exp_neg_inv_glue.f_aux n) (polynomial.eval x (exp_neg_inv_glue.P_aux (n + 1)) * real.exp (-x⁻¹) / x ^ (2 * (n + 1))) x

For positive values, the derivative of the n-th auxiliary function f_aux n is the n+1-th auxiliary function.

source

theorem exp_neg_inv_glue.f_aux_limit (n : ℕ) :

filter.tendsto (λ (x : ℝ), polynomial.eval x (exp_neg_inv_glue.P_aux n) * real.exp (-x⁻¹) / x ^ (2 * n)) (nhds_within 0 (set.Ioi 0)) (nhds 0)

To get differentiability at 0 of the auxiliary functions, we need to know that their limit is 0, to be able to apply general differentiability extension theorems. This limit is checked in this lemma.

source

theorem exp_neg_inv_glue.f_aux_deriv_zero (n : ℕ) :

has_deriv_at (exp_neg_inv_glue.f_aux n) 0 0

Deduce from the limiting behavior at 0 of its derivative and general differentiability extension theorems that the auxiliary function f_aux n is differentiable at 0, with derivative 0.

source

theorem exp_neg_inv_glue.f_aux_has_deriv_at (n : ℕ) (x : ℝ) :

has_deriv_at (exp_neg_inv_glue.f_aux n) (exp_neg_inv_glue.f_aux (n + 1) x) x

At every point, the auxiliary function f_aux n has a derivative which is equal to f_aux (n+1).

source

theorem exp_neg_inv_glue.f_aux_iterated_deriv (n : ℕ) :

iterated_deriv n (exp_neg_inv_glue.f_aux 0) = exp_neg_inv_glue.f_aux n

The successive derivatives of the auxiliary function f_aux 0 are the functions f_aux n, by induction.

source

theorem exp_neg_inv_glue.smooth :

times_cont_diff ℝ ⊤ exp_neg_inv_glue

The function exp_neg_inv_glue is smooth.