isLittleO_pow_exp_atTop — Mathlib

English

For every n, x^n = o(exp) as x → +∞; polynomials grow more slowly than the exponential.

Русский

Для каждого n, x^n = o(exp) при x → +∞; полиномиалы растут медленнее экспоненты.

LaTeX

$$$\\displaystyle x^{n} = o\\left( e^{x} \\right) \\quad \\text{при } x \\to +\\infty.$$$

Lean4

theorem isLittleO_pow_exp_atTop {n : ℕ} : (fun x : ℝ => x ^ n) =o[atTop] Real.exp := by
  simpa [isLittleO_iff_tendsto fun x hx => ((exp_pos x).ne' hx).elim] using
    tendsto_div_pow_mul_exp_add_atTop 1 0 n zero_ne_one

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