isLittleO_pow_log_id_atTop — Mathlib

English

For any fixed natural n, (log x)^n is little-o of x as x → ∞; i.e., log(x)^n / x → 0.

Русский

Для любого фиксированного натурального n, (log x)^n = o(x) при x → ∞; то есть log(x)^n / x → 0.

LaTeX

$$$$ (\\log x)^n = o(x) \\quad \\text{as } x \\to \\infty. $$$$

Lean4

theorem isLittleO_pow_log_id_atTop {n : ℕ} : (fun x => log x ^ n) =o[atTop] id :=
  by
  rw [Asymptotics.isLittleO_iff_tendsto']
  · simpa using tendsto_pow_log_div_mul_add_atTop 1 0 n one_ne_zero
  filter_upwards [eventually_ne_atTop (0 : ℝ)] with x h₁ h₂ using (h₁ h₂).elim

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