isLittleO_log_rpow_atTop — Mathlib

English

For every positive real r, the natural logarithm grows strictly slower than x^r as x tends to infinity.

Русский

Для любого положительного числа r логарифм растет заметно медленнее степени x^r при x → ∞.

LaTeX

$$$\forall r>0\,\lim_{x\to\infty}\frac{\log x}{x^r}=0$$$

Lean4

theorem isLittleO_log_rpow_atTop {r : ℝ} (hr : 0 < r) : log =o[atTop] fun x => x ^ r :=
  calc
    log =O[atTop] fun x => r * log x := isBigO_self_const_mul hr.ne' _ _
    _ =ᶠ[atTop] fun x => log (x ^ r) := ((eventually_gt_atTop 0).mono fun _ hx => (log_rpow hx _).symm)
    _ =o[atTop] fun x => x ^ r := isLittleO_log_id_atTop.comp_tendsto (tendsto_rpow_atTop hr)

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