refactor(Analysis/Asymptotics): split long file Defs.lean

Mathlib.lean

@@ -1677,12 +1677,16 @@ public import Mathlib.Analysis.Analytic.Uniqueness
 public import Mathlib.Analysis.Analytic.WithLp
 public import Mathlib.Analysis.Analytic.Within
 public import Mathlib.Analysis.AperiodicOrder.Delone.Basic
+public import Mathlib.Analysis.Asymptotics.Arith
 public import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
+public import Mathlib.Analysis.Asymptotics.Basic
 public import Mathlib.Analysis.Asymptotics.Completion
 public import Mathlib.Analysis.Asymptotics.Defs
 public import Mathlib.Analysis.Asymptotics.ExpGrowth
 public import Mathlib.Analysis.Asymptotics.Lemmas
 public import Mathlib.Analysis.Asymptotics.LinearGrowth
+public import Mathlib.Analysis.Asymptotics.Prod
+public import Mathlib.Analysis.Asymptotics.Ring
 public import Mathlib.Analysis.Asymptotics.SpecificAsymptotics
 public import Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
 public import Mathlib.Analysis.Asymptotics.TVS

Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

@@ -5,7 +5,7 @@ Authors: Anatole Dedecker
 -/
 module
 
-public import Mathlib.Analysis.Asymptotics.Defs
+public import Mathlib.Analysis.Asymptotics.Ring
 public import Mathlib.Analysis.Normed.Module.Basic
 import Mathlib.Analysis.Asymptotics.Theta
 
@@ -70,6 +70,14 @@ variable {α β : Type*} [NormedAddCommGroup β]
 
 variable {u v w : α → β} {l : Filter α}
 
+/-- 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`. -/
+@[expose] def IsEquivalent (l : Filter α) (u v : α → β) :=
+  (u - v) =o[l] v
+
+@[inherit_doc] scoped notation:50 u " ~[" l:50 "] " v:50 => Asymptotics.IsEquivalent l u v
+
 theorem IsEquivalent.isLittleO (h : u ~[l] v) : (u - v) =o[l] v := h
 
 nonrec theorem IsEquivalent.isBigO (h : u ~[l] v) : u =O[l] v :=