isBigO_nat_atTop_iff — Mathlib

English

Characterization of Big-O atTop for f: ℕ → E'' and g: ℕ → E'': f = O[atTop] g iff there exists C with ∀ n, ‖f(n)‖ ≤ C‖g(n)‖.

Русский

Характеризация Big-O вдоль atTop для f: ℕ → E'' и g: ℕ → E'': f = O[atTop] g тогда и только тогда, когда существует C, для всех n выполняется ‖f(n)‖ ≤ C‖g(n)‖.

LaTeX

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

Lean4

theorem isBigO_nat_atTop_iff {f : ℕ → E''} {g : ℕ → F''} (h : ∀ x, g x = 0 → f x = 0) :
    f =O[atTop] g ↔ ∃ C, ∀ x, ‖f x‖ ≤ C * ‖g x‖ := by rw [← Nat.cofinite_eq_atTop, isBigO_cofinite_iff h]

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