Theorems · Definition · approximation theory

Asymptotics.IsEquivalent

{α : Type u_1} → {E' : Type u_6} → [SeminormedAddCommGroup E'] → Filter α → (α → E') → (α → E') → Prop

Two functions u and v are said to be asymptotically equivalent along a filter l (denoted as u ~[l] v in the Asymptotics namespace) when u x - v x = o(v x) as x converges along l.

Defined in

Mathlib.Analysis.Asymptotics.Defs

Cited by

98 results in Mathlib

Foundations

Depth 103 from the axioms, rests on 1,973 definitions · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroup