isBigOWith_iff — Mathlib

English

The Big-O relation f =O[l] g is defined via the existence of a constant c and eventual bound: there exists c with the property that eventually ||f(x)|| ≤ c ||g(x)||.

Русский

Отношение Big-O: существует константа c такая, что по сути выполняется неравенство ||f(x)|| ≤ c ||g(x)||.

LaTeX

$$$ f =O[l] g \;\Longleftrightarrow\; \exists c \in \mathbb{R}, \; \forall^\! x \in l, \; \|f(x)\| \le c \|g(x)\|.$$$

Lean4

/-- Definition of `IsBigOWith`. We record it in a lemma as `IsBigOWith` is irreducible. -/
theorem isBigOWith_iff : IsBigOWith c l f g ↔ ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ := by rw [IsBigOWith_def]

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