feat(Analysis/Asymptotics/AsymptoticEquivalent): add Trans instance…

…s for `IsEquivalent` (#5572)

This PR adds several `Trans` instances for the `IsEquivalent` relation, and a few missing lemmas on the same topic.



Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

@@ -9,6 +9,7 @@ Authors: Anatole Dedecker
 ! if you have ported upstream changes.
 -/
 import Mathlib.Analysis.Asymptotics.Asymptotics
+import Mathlib.Analysis.Asymptotics.Theta
 import Mathlib.Analysis.Normed.Order.Basic
 
 /-!
@@ -94,6 +95,12 @@ theorem IsEquivalent.isBigO_symm (h : u ~[l] v) : v =O[l] u := by
 set_option linter.uppercaseLean3 false in
 #align asymptotics.is_equivalent.is_O_symm Asymptotics.IsEquivalent.isBigO_symm
 
+theorem IsEquivalent.isTheta (h : u ~[l] v) : u =Θ[l] v :=
+  ⟨h.isBigO, h.isBigO_symm⟩
+
+theorem IsEquivalent.isTheta_symm (h : u ~[l] v) : v =Θ[l] u :=
+  ⟨h.isBigO_symm, h.isBigO⟩
+
 @[refl]
 theorem IsEquivalent.refl : u ~[l] u := by
   rw [IsEquivalent, sub_self]
@@ -338,8 +345,88 @@ open Filter Asymptotics
 
 open Asymptotics
 
-variable {α β : Type _} [NormedAddCommGroup β]
+variable {α β β₂ : Type _} [NormedAddCommGroup β] [Norm β₂] {l : Filter α}
 
-theorem Filter.EventuallyEq.isEquivalent {u v : α → β} {l : Filter α} (h : u =ᶠ[l] v) : u ~[l] v :=
+theorem Filter.EventuallyEq.isEquivalent {u v : α → β} (h : u =ᶠ[l] v) : u ~[l] v :=
   IsEquivalent.congr_right (isLittleO_refl_left _ _) h
 #align filter.eventually_eq.is_equivalent Filter.EventuallyEq.isEquivalent
+
+@[trans]
+theorem Filter.EventuallyEq.trans_isEquivalent {f g₁ g₂ : α → β} (h : f =ᶠ[l] g₁)
+    (h₂ : g₁ ~[l] g₂) : f ~[l] g₂ :=
+  h.isEquivalent.trans h₂
+
+namespace Asymptotics
+
+instance transIsEquivalentIsEquivalent :
+    @Trans (α → β) (α → β) (α → β) (IsEquivalent l) (IsEquivalent l) (IsEquivalent l) where
+  trans := IsEquivalent.trans
+
+instance transEventuallyEqIsEquivalent :
+    @Trans (α → β) (α → β) (α → β) (EventuallyEq l) (IsEquivalent l) (IsEquivalent l) where
+  trans := EventuallyEq.trans_isEquivalent
+
+@[trans]
+theorem IsEquivalent.trans_eventuallyEq {f g₁ g₂ : α → β} (h : f ~[l] g₁)
+    (h₂ : g₁ =ᶠ[l] g₂) : f ~[l] g₂ :=
+  h.trans h₂.isEquivalent
+
+instance transIsEquivalentEventuallyEq :
+    @Trans (α → β) (α → β) (α → β) (IsEquivalent l) (EventuallyEq l) (IsEquivalent l) where
+  trans := IsEquivalent.trans_eventuallyEq
+
+@[trans]
+theorem IsEquivalent.trans_isBigO {f g₁ : α → β} {g₂ : α → β₂} (h : f ~[l] g₁) (h₂ : g₁ =O[l] g₂) :
+    f =O[l] g₂ :=
+  IsBigO.trans h.isBigO h₂
+
+instance transIsEquivalentIsBigO :
+    @Trans (α → β) (α → β) (α → β₂) (IsEquivalent l) (IsBigO l) (IsBigO l) where
+  trans := IsEquivalent.trans_isBigO
+
+@[trans]
+theorem IsBigO.trans_isEquivalent {f : α → β₂} {g₁ g₂ : α → β} (h : f =O[l] g₁) (h₂ : g₁ ~[l] g₂) :
+    f =O[l] g₂ :=
+  IsBigO.trans h h₂.isBigO
+
+instance transIsBigOIsEquivalent :
+    @Trans (α → β₂) (α → β) (α → β) (IsBigO l) (IsEquivalent l) (IsBigO l) where
+  trans := IsBigO.trans_isEquivalent
+
+@[trans]
+theorem IsEquivalent.trans_isLittleO {f g₁ : α → β} {g₂ : α → β₂} (h : f ~[l] g₁)
+    (h₂ : g₁ =o[l] g₂) : f =o[l] g₂ :=
+  IsBigO.trans_isLittleO h.isBigO h₂
+
+instance transIsEquivalentIsLittleO :
+    @Trans (α → β) (α → β) (α → β₂) (IsEquivalent l) (IsLittleO l) (IsLittleO l) where
+  trans := IsEquivalent.trans_isLittleO
+
+@[trans]
+theorem IsLittleO.trans_isEquivalent {f : α → β₂} {g₁ g₂ : α → β} (h : f =o[l] g₁)
+    (h₂ : g₁ ~[l] g₂) : f =o[l] g₂ :=
+  IsLittleO.trans_isBigO h h₂.isBigO
+
+instance transIsLittleOIsEquivalent :
+    @Trans (α → β₂) (α → β) (α → β) (IsLittleO l) (IsEquivalent l) (IsLittleO l) where
+  trans := IsLittleO.trans_isEquivalent
+
+@[trans]
+theorem IsEquivalent.trans_isTheta {f g₁ : α → β} {g₂ : α → β₂} (h : f ~[l] g₁)
+    (h₂ : g₁ =Θ[l] g₂) : f =Θ[l] g₂ :=
+  IsTheta.trans h.isTheta h₂
+
+instance transIsEquivalentIsTheta :
+    @Trans (α → β) (α → β) (α → β₂) (IsEquivalent l) (IsTheta l) (IsTheta l) where
+  trans := IsEquivalent.trans_isTheta
+
+@[trans]
+theorem IsTheta.trans_isEquivalent {f : α → β₂} {g₁ g₂ : α → β} (h : f =Θ[l] g₁)
+    (h₂ : g₁ ~[l] g₂) : f =Θ[l] g₂ :=
+  IsTheta.trans h h₂.isTheta
+
+instance transIsThetaIsEquivalent :
+    @Trans (α → β₂) (α → β) (α → β) (IsTheta l) (IsEquivalent l) (IsTheta l) where
+  trans := IsTheta.trans_isEquivalent
+
+end Asymptotics