Theorems · Theorem · approximation theory

Asymptotics.isBigO_iff_div_isBoundedUnder

∀ {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {α : Type u_17} {l : Filter α} {f g : α → 𝕜},
  (∀ᶠ (x : α) in l, g x = 0 → f 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 119 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedDivisionRing