isBigO_iff_eventually — Mathlib

English

If f = OWith c l f g' for some c, then there exists c' > 0 such that f = OWith c' l f g'.

Русский

Если f = OWith c l f g', то существует c' > 0, такое что f = OWith c' l f g'.

LaTeX

$$$ IsBigOWith c l f g' \rightarrow \exists c'>0, IsBigOWith c' l f g' $$$

Lean4

/-- `f = O(g)` if and only if `∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖` for all sufficiently large `c`. -/
theorem isBigO_iff_eventually : f =O[l] g' ↔ ∀ᶠ c in atTop, ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g' x‖ :=
  isBigO_iff_eventually_isBigOWith.trans <| by simp only [IsBigOWith_def]

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