Theorems · Theorem · approximation theory

Asymptotics.IsEquivalent.exists_pos_eq_mul

∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] [inst_1 : LinearOrder β] [IsStrictOrderedRing β] {u v : α → β}
  {l : Filter α} [ClosedIicTopology β], Asymptotics.IsEquivalent l u v → ∃ φ, (∀ᶠ (x : α) in l, 0 < φ x) ∧ u =ᶠ[l] φ * v

Defined in

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedFieldLinearOrderIsStrictOrderedRingClosedIicTopology