isBigO_iff_eventually_isBigOWith — Mathlib

English

If f = O[l] g' and l has a basis p, s, then there exists a bound c > 0 and an index i such that for all x ∈ s(i) one has ‖f(x)‖ ≤ c ‖g'(x)‖.

Русский

Если f = O[l] g' и l имеет базис p, s, тогда существует c > 0 и индекс i с условием, что для всех x ∈ s(i) выполняется ‖f(x)‖ ≤ c‖g'(x)‖.

LaTeX

$$$ f =O[l] g' \rightarrow l.HasBasis p s \rightarrow \exists c>0, \exists i, p(i) \land \forall x ∈ s(i), \|f(x)\| ≤ c \|g'(x)\| $$$

Lean4

/-- `f = O(g)` if and only if `IsBigOWith c f g` for all sufficiently large `c`. -/
theorem isBigO_iff_eventually_isBigOWith : f =O[l] g' ↔ ∀ᶠ c in atTop, IsBigOWith c l f g' :=
  isBigO_iff_isBigOWith.trans ⟨fun ⟨c, hc⟩ => mem_atTop_sets.2 ⟨c, fun _c' hc' => hc.weaken hc'⟩, fun h => h.exists⟩

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