Theorems · Theorem · approximation theory

Asymptotics.isBigO_iff_isBoundedUnder_le_div

∀ {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [inst : Norm E] [inst_1 : NormedAddCommGroup F''] {f : α → E}
  {g'' : α → F''} {l : Filter α},
  (∀ᶠ (x : α) in l, g'' x ≠ 0) → (f =O[l] g'' ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f x‖ / ‖g'' x‖)

Defined in

Mathlib.Analysis.Asymptotics.Lemmas

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormNormedAddCommGroup