bound_of_isBigO_nat_atTop — Mathlib

English

There is an equivalence between Big-O along atTop and the existence of a uniform bound on natural-number inputs.

Русский

Существует эквивалентность между Big-O вдоль atTop и существованием единого верхнего предела для натуральных аргументов.

LaTeX

$$$\\displaystyle f = O[atTop] g \\iff \\exists C>0, \\forall n: \\|f(n)\\| ≤ C\\|g(n)\\|.$$$

Lean4

theorem bound_of_isBigO_nat_atTop {f : ℕ → E} {g'' : ℕ → E''} (h : f =O[atTop] g'') :
    ∃ C > 0, ∀ ⦃x⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖ :=
  bound_of_isBigO_cofinite <| by rwa [Nat.cofinite_eq_atTop]

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