isLittleO_log_id_atTop — Mathlib

English

The logarithm function log x is little-o of the identity function id as x → ∞; equivalently log x / x → 0.

Русский

Функция логарифм log x растёт медленнее функции идентичности: log x = o(x) при x → ∞; то есть log x / x → 0.

LaTeX

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

Lean4

theorem isLittleO_log_id_atTop : log =o[atTop] id :=
  isLittleO_pow_log_id_atTop.congr_left fun _ => pow_one _

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