isBigO_atTop_iff_eventually_exists_pos

English

Let f: α → G and g: α → G' with α as above. Then f = O_{atTop} g if and only if there exists an eventually positive constant c such that on some tail ∥f(n)∥ ≤ c ∥g(n)∥ for all n beyond that tail.

Русский

Пусть f: α → G и g: α → G' с тем же свойством. Тогда f = O_{atTop} g эквивалентно существованию в хвосте произвольной положительной константы c, такой что для больших n выполняется ∥f(n)∥ ≤ c ∥g(n)∥.

LaTeX

$$$ f =O_{atTop} g \\iff \\forall^\\infty n_0 \\in atTop, \\exists c>0, \\forall n \\ge n_0, c \\|f(n)\\| \\le \\|g(n)\\| $$$

Lean4

theorem isBigO_atTop_iff_eventually_exists_pos {α : Type*} [SemilatticeSup α] [Nonempty α] {f : α → G} {g : α → G'} :
    f =O[atTop] g ↔ ∀ᶠ n₀ in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖ := by
  simp_rw [isBigO_iff'', ← exists_prop, Subtype.exists', exists_eventually_atTop]

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