Theorems · Theorem · approximation theory

Asymptotics.isBigOWith_iff_exists_eq_mul

∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {c : ℝ} {l : Filter α} {u v : α → 𝕜},
  0 ≤ c → (Asymptotics.IsBigOWith c l u v ↔ ∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v)

Defined in

Mathlib.Analysis.Asymptotics.Lemmas

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedDivisionRing