isLittleO_const_log_atTop — Mathlib

English

Any constant function c is little-o of log at infinity; i.e., c = o(log x) as x → ∞.

Русский

Любая константа c является mалый-o от log при x → бесконечность; то есть c / log x → 0.

LaTeX

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

Lean4

theorem isLittleO_const_log_atTop {c : ℝ} : (fun _ => c) =o[atTop] log :=
  by
  refine Asymptotics.isLittleO_of_tendsto' ?_ <| Tendsto.div_atTop (a := c) (by simp) tendsto_log_atTop
  filter_upwards [eventually_gt_atTop 1] with x hx
  aesop (add safe forward log_pos)

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