English
Let f: α → E and g: α → F with α a directed set having a top element. Then f = O_{atTop} g if and only if there exists a bound that holds eventually: there is some tail after which ∥f(n)∥ ≤ C ∥g(n)∥ for some constant C.
Русский
Пусть f: α → E и g: α → F, где α — направленный множество с верхней границей. Тогда f = O_{atTop} g тогда и только тогда, когда существует предел по хвосту: после некоторого момента найдётся константа C, такая что ∥f(n)∥ ≤ C∥g(n)∥ для всех n дальше по порядку.
LaTeX
$$$ f =O_{atTop} g \\iff \\forall^\\infty n_0 \\in atTop, \\exists c, \\forall n \\ge n_0, \\|f(n)\\| \\le c \\|g(n)\\| $$$
Lean4
theorem isBigO_atTop_iff_eventually_exists {α : Type*} [SemilatticeSup α] [Nonempty α] {f : α → E} {g : α → F} :
f =O[atTop] g ↔ ∀ᶠ n₀ in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖ := by rw [isBigO_iff, exists_eventually_atTop]
