Theorems · Theorem · approximation theory

Asymptotics.isBigO_cofinite_iff

∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {f'' : α → E''} {g'' : α → F''},
  (∀ (x : α), g'' x = 0 → f'' x = 0) → (f'' =O[Filter.cofinite] g'' ↔ ∃ C, ∀ (x : α), ‖f'' x‖ ≤ C * ‖g'' x‖)

Defined in

Mathlib.Analysis.Asymptotics.Lemmas

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroup