Theorems · Theorem · approximation theory

Asymptotics.bound_of_isBigO_cofinite

∀ {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [inst : Norm E] [inst_1 : NormedAddCommGroup F''] {f : α → E}
  {g'' : α → F''}, f =O[Filter.cofinite] g'' → ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

If f x = O(g x) along cofinite, then there exists a positive constant C such that ‖f x‖ ≤ C * ‖g x‖ whenever g x ≠ 0.

Defined in

Mathlib.Analysis.Asymptotics.Lemmas

Cited by

2 results in Mathlib

Foundations

Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormNormedAddCommGroup