tendsto_pow_mul_exp_neg_atTop_nhds_zero

English

For any n ∈ ℕ, exp(x)/x^n → ∞ as x → ∞.

Русский

Для любого n ∈ ℕ, exp(x)/x^n → ∞ при x → ∞.

LaTeX

$$$\\lim_{x \\to +\\infty} \\frac{e^{x}}{x^{n}} = +\\infty\\quad (n\\in\\mathbb{N}).$$$

Lean4

/-- The function `x^n * exp(-x)` tends to `0` at `+∞`, for any natural number `n`. -/
theorem tendsto_pow_mul_exp_neg_atTop_nhds_zero (n : ℕ) : Tendsto (fun x => x ^ n * exp (-x)) atTop (𝓝 0) :=
  (tendsto_inv_atTop_zero.comp (tendsto_exp_div_pow_atTop n)).congr fun x => by
    rw [comp_apply, inv_eq_one_div, div_div_eq_mul_div, one_mul, div_eq_mul_inv, exp_neg]

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