isBigO_iff — Mathlib

English

A variant of IsBigO with a positive constant; f =O[l] g iff there exists c > 0 such that the eventual bound holds.

Русский

Вариант IsBigO с положительной константой: f =O[l] g эквивалентно существованию c > 0, для которого выполняется неравенство в пределе.

LaTeX

$$$ f =O[l] g \iff \exists c > 0, \forall^\! x \in l, \|f(x)\| ≤ c \|g(x)\|$$$

Lean4

/-- Definition of `IsBigO` in terms of filters. -/
theorem isBigO_iff : f =O[l] g ↔ ∃ c : ℝ, ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ := by simp only [IsBigO_def, IsBigOWith_def]

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