Theorems · Theorem · approximation theory

Asymptotics.isBigOWith_of_eq_mul

∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {c : ℝ} {l : Filter α} {u v : α → R} (φ : α → R),
  (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) → u =ᶠ[l] φ * v → Asymptotics.IsBigOWith c l u v

If ‖φ‖ is eventually bounded by c, and u =ᶠ[l] φ * v, then we have IsBigOWith c u v l. This does not require any assumptions on c, which is why we keep this version along with IsBigOWith_iff_exists_eq_mul.

Defined in

Mathlib.Analysis.Asymptotics.Lemmas

Cited by

3 results in Mathlib

Foundations

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

Assumes

SeminormedRing