English
For every ENat n and polynomial p, the function x ↦ p(x^{-1}) expNegInvGlue x is ContDiff Real of order n.
Русский
Для каждого n ∈ ℕ∞ и многочлена p функция x ↦ p(x^{-1}) expNegInvGlue x имеет свойство ContDiff Real порядка n.
LaTeX
$$$\forall n:\mathbb{N}_\infty,\ \text{ContDiff}_{\mathbb{R}}(n)\bigl(x\mapsto p(x^{-1}) \exp(-1/x)\bigr)$$$
Lean4
theorem contDiff_polynomial_eval_inv_mul {n : ℕ∞} (p : ℝ[X]) : ContDiff ℝ n (fun x ↦ p.eval x⁻¹ * expNegInvGlue x) :=
by
apply contDiff_all_iff_nat.2 (fun m => ?_) n
induction m generalizing p with
| zero => exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _
| succ m ihm =>
rw [show ((m + 1 : ℕ) : WithTop ℕ∞) = m + 1 from rfl]
refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, by simp, ?_⟩
convert ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv
