tendsto_polynomial_inv_mul_zero — Mathlib

English

For any polynomial p, the function x ↦ p(x^{-1}) expNegInvGlue x tends to 0 as x → 0.

Русский

Для любого многочлена p, функция x ↦ p(x^{-1}) expNegInvGlue x стремится к 0 при x → 0.

LaTeX

$$$\lim_{x\to 0} p(x^{-1}) e^{-1/x} = 0$$

Lean4

/-- Our function tends to zero at zero faster than any $P(x^{-1})$, $P∈ℝ[X]$, tends to infinity. -/
theorem tendsto_polynomial_inv_mul_zero (p : ℝ[X]) : Tendsto (fun x ↦ p.eval x⁻¹ * expNegInvGlue x) (𝓝 0) (𝓝 0) :=
  by
  simp only [expNegInvGlue, mul_ite, mul_zero]
  refine tendsto_const_nhds.if ?_
  simp only [not_le]
  have : Tendsto (fun x ↦ p.eval x⁻¹ / exp x⁻¹) (𝓝[>] 0) (𝓝 0) := p.tendsto_div_exp_atTop.comp tendsto_inv_nhdsGT_zero
  refine this.congr' <| mem_of_superset self_mem_nhdsWithin fun x hx ↦ ?_
  simp [exp_neg, div_eq_mul_inv]

Похожие утверждения