# Asymptotic equivalence #

In this file, we define the relation IsEquivalent l u v, which means that u-v is little o of v along the filter l.

Unlike Is(Little|Big)O relations, this one requires u and v to have the same codomain β. While the definition only requires β to be a NormedAddCommGroup, most interesting properties require it to be a NormedField.

## Notations #

We introduce the notation u ~[l] v := IsEquivalent l u v, which you can use by opening the Asymptotics locale.

## Main results #

If β is a NormedAddCommGroup :

• _ ~[l] _ is an equivalence relation
• Equivalent statements for u ~[l] const _ c :
• If c ≠ 0, this is true iff Tendsto u l (𝓝 c) (see isEquivalent_const_iff_tendsto)
• For c = 0, this is true iff u =ᶠ[l] 0 (see isEquivalent_zero_iff_eventually_zero)

If β is a NormedField :

• Alternative characterization of the relation (see isEquivalent_iff_exists_eq_mul) :

u ~[l] v ↔ ∃ (φ : α → β) (hφ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

• Provided some non-vanishing hypothesis, this can be seen as u ~[l] v ↔ Tendsto (u/v) l (𝓝 1) (see isEquivalent_iff_tendsto_one)

• For any constant c, u ~[l] v implies Tendsto u l (𝓝 c) ↔ Tendsto v l (𝓝 c) (see IsEquivalent.tendsto_nhds_iff)

• * and / are compatible with _ ~[l] _ (see IsEquivalent.mul and IsEquivalent.div)

If β is a NormedLinearOrderedField :

• If u ~[l] v, we have Tendsto u l atTop ↔ Tendsto v l atTop (see IsEquivalent.tendsto_atTop_iff)

## Implementation Notes #

Note that IsEquivalent takes the parameters (l : Filter α) (u v : α → β) in that order. This is to enable calc support, as calc requires that the last two explicit arguments are u v.

def Asymptotics.IsEquivalent {α : Type u_1} {β : Type u_2} (l : ) (u : αβ) (v : αβ) :

Two functions u and v are said to be asymptotically equivalent along a filter l when u x - v x = o(v x) as x converges along l.

Equations
Instances For

Two functions u and v are said to be asymptotically equivalent along a filter l when u x - v x = o(v x) as x converges along l.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Asymptotics.IsEquivalent.isLittleO {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {l : } (h : ) :
(u - v) =o[l] v
theorem Asymptotics.IsEquivalent.isBigO {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {l : } (h : ) :
u =O[l] v
theorem Asymptotics.IsEquivalent.isBigO_symm {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {l : } (h : ) :
v =O[l] u
theorem Asymptotics.IsEquivalent.isTheta {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {l : } (h : ) :
u =Θ[l] v
theorem Asymptotics.IsEquivalent.isTheta_symm {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {l : } (h : ) :
v =Θ[l] u
theorem Asymptotics.IsEquivalent.refl {α : Type u_1} {β : Type u_2} {u : αβ} {l : } :
theorem Asymptotics.IsEquivalent.symm {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {l : } (h : ) :
theorem Asymptotics.IsEquivalent.trans {α : Type u_1} {β : Type u_2} {l : } {u : αβ} {v : αβ} {w : αβ} (huv : ) (hvw : ) :
theorem Asymptotics.IsEquivalent.congr_left {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {w : αβ} {l : } (huv : ) (huw : u =ᶠ[l] w) :
theorem Asymptotics.IsEquivalent.congr_right {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {w : αβ} {l : } (huv : ) (hvw : v =ᶠ[l] w) :
theorem Asymptotics.isEquivalent_zero_iff_eventually_zero {α : Type u_1} {β : Type u_2} {u : αβ} {l : } :
u =ᶠ[l] 0
theorem Asymptotics.isEquivalent_zero_iff_isBigO_zero {α : Type u_1} {β : Type u_2} {u : αβ} {l : } :
u =O[l] 0
theorem Asymptotics.isEquivalent_const_iff_tendsto {α : Type u_1} {β : Type u_2} {u : αβ} {l : } {c : β} (h : c 0) :
theorem Asymptotics.IsEquivalent.tendsto_const {α : Type u_1} {β : Type u_2} {u : αβ} {l : } {c : β} (hu : ) :
theorem Asymptotics.IsEquivalent.tendsto_nhds {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {l : } {c : β} (huv : ) (hu : Filter.Tendsto u l (nhds c)) :
theorem Asymptotics.IsEquivalent.tendsto_nhds_iff {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {l : } {c : β} (huv : ) :
theorem Asymptotics.IsEquivalent.add_isLittleO {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {w : αβ} {l : } (huv : ) (hwv : w =o[l] v) :
theorem Asymptotics.IsEquivalent.sub_isLittleO {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {w : αβ} {l : } (huv : ) (hwv : w =o[l] v) :
theorem Asymptotics.IsLittleO.add_isEquivalent {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {w : αβ} {l : } (hu : u =o[l] w) (hv : ) :
theorem Asymptotics.IsLittleO.isEquivalent {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {l : } (huv : (u - v) =o[l] v) :
theorem Asymptotics.IsEquivalent.neg {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {l : } (huv : ) :
Asymptotics.IsEquivalent l (fun (x : α) => -u x) fun (x : α) => -v x
theorem Asymptotics.isEquivalent_iff_exists_eq_mul {α : Type u_1} {β : Type u_2} [] {u : αβ} {v : αβ} {l : } :
∃ (φ : αβ) (_ : Filter.Tendsto φ l (nhds 1)), u =ᶠ[l] φ * v
theorem Asymptotics.IsEquivalent.exists_eq_mul {α : Type u_1} {β : Type u_2} [] {u : αβ} {v : αβ} {l : } (huv : ) :
∃ (φ : αβ) (_ : Filter.Tendsto φ l (nhds 1)), u =ᶠ[l] φ * v
theorem Asymptotics.isEquivalent_of_tendsto_one {α : Type u_1} {β : Type u_2} [] {u : αβ} {v : αβ} {l : } (hz : ∀ᶠ (x : α) in l, v x = 0u x = 0) (huv : Filter.Tendsto (u / v) l (nhds 1)) :
theorem Asymptotics.isEquivalent_of_tendsto_one' {α : Type u_1} {β : Type u_2} [] {u : αβ} {v : αβ} {l : } (hz : ∀ (x : α), v x = 0u x = 0) (huv : Filter.Tendsto (u / v) l (nhds 1)) :
theorem Asymptotics.isEquivalent_iff_tendsto_one {α : Type u_1} {β : Type u_2} [] {u : αβ} {v : αβ} {l : } (hz : ∀ᶠ (x : α) in l, v x 0) :
Filter.Tendsto (u / v) l (nhds 1)
theorem Asymptotics.IsEquivalent.smul {α : Type u_1} {E : Type u_2} {𝕜 : Type u_3} [] [] {a : α𝕜} {b : α𝕜} {u : αE} {v : αE} {l : } (hab : ) (huv : ) :
Asymptotics.IsEquivalent l (fun (x : α) => a x u x) fun (x : α) => b x v x
theorem Asymptotics.IsEquivalent.mul {α : Type u_1} {β : Type u_2} [] {t : αβ} {u : αβ} {v : αβ} {w : αβ} {l : } (htu : ) (hvw : ) :
theorem Asymptotics.IsEquivalent.inv {α : Type u_1} {β : Type u_2} [] {u : αβ} {v : αβ} {l : } (huv : ) :
Asymptotics.IsEquivalent l (fun (x : α) => (u x)⁻¹) fun (x : α) => (v x)⁻¹
theorem Asymptotics.IsEquivalent.div {α : Type u_1} {β : Type u_2} [] {t : αβ} {u : αβ} {v : αβ} {w : αβ} {l : } (htu : ) (hvw : ) :
Asymptotics.IsEquivalent l (fun (x : α) => t x / v x) fun (x : α) => u x / w x
theorem Asymptotics.IsEquivalent.tendsto_atTop {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {l : } [] (huv : ) (hu : Filter.Tendsto u l Filter.atTop) :
Filter.Tendsto v l Filter.atTop
theorem Asymptotics.IsEquivalent.tendsto_atTop_iff {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {l : } [] (huv : ) :
Filter.Tendsto u l Filter.atTop Filter.Tendsto v l Filter.atTop
theorem Asymptotics.IsEquivalent.tendsto_atBot {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {l : } [] (huv : ) (hu : Filter.Tendsto u l Filter.atBot) :
Filter.Tendsto v l Filter.atBot
theorem Asymptotics.IsEquivalent.tendsto_atBot_iff {α : Type u_1} {β : Type u_2} {u : αβ} {v : αβ} {l : } [] (huv : ) :
Filter.Tendsto u l Filter.atBot Filter.Tendsto v l Filter.atBot
theorem Filter.EventuallyEq.isEquivalent {α : Type u_1} {β : Type u_2} {l : } {u : αβ} {v : αβ} (h : u =ᶠ[l] v) :
theorem Filter.EventuallyEq.trans_isEquivalent {α : Type u_1} {β : Type u_2} {l : } {f : αβ} {g₁ : αβ} {g₂ : αβ} (h : f =ᶠ[l] g₁) (h₂ : ) :
instance Asymptotics.transIsEquivalentIsEquivalent {α : Type u_1} {β : Type u_2} {l : } :
Equations
• Asymptotics.transIsEquivalentIsEquivalent = { trans := }
instance Asymptotics.transEventuallyEqIsEquivalent {α : Type u_1} {β : Type u_2} {l : } :
Trans l.EventuallyEq
Equations
• Asymptotics.transEventuallyEqIsEquivalent = { trans := }
theorem Asymptotics.IsEquivalent.trans_eventuallyEq {α : Type u_1} {β : Type u_2} {l : } {f : αβ} {g₁ : αβ} {g₂ : αβ} (h : ) (h₂ : g₁ =ᶠ[l] g₂) :
instance Asymptotics.transIsEquivalentEventuallyEq {α : Type u_1} {β : Type u_2} {l : } :
Trans l.EventuallyEq
Equations
• Asymptotics.transIsEquivalentEventuallyEq = { trans := }
theorem Asymptotics.IsEquivalent.trans_isBigO {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [Norm β₂] {l : } {f : αβ} {g₁ : αβ} {g₂ : αβ₂} (h : ) (h₂ : g₁ =O[l] g₂) :
f =O[l] g₂
instance Asymptotics.transIsEquivalentIsBigO {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [Norm β₂] {l : } :
Equations
• Asymptotics.transIsEquivalentIsBigO = { trans := }
theorem Asymptotics.IsBigO.trans_isEquivalent {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [Norm β₂] {l : } {f : αβ₂} {g₁ : αβ} {g₂ : αβ} (h : f =O[l] g₁) (h₂ : ) :
f =O[l] g₂
instance Asymptotics.transIsBigOIsEquivalent {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [Norm β₂] {l : } :
Equations
• Asymptotics.transIsBigOIsEquivalent = { trans := }
theorem Asymptotics.IsEquivalent.trans_isLittleO {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [Norm β₂] {l : } {f : αβ} {g₁ : αβ} {g₂ : αβ₂} (h : ) (h₂ : g₁ =o[l] g₂) :
f =o[l] g₂
instance Asymptotics.transIsEquivalentIsLittleO {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [Norm β₂] {l : } :
Equations
• Asymptotics.transIsEquivalentIsLittleO = { trans := }
theorem Asymptotics.IsLittleO.trans_isEquivalent {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [Norm β₂] {l : } {f : αβ₂} {g₁ : αβ} {g₂ : αβ} (h : f =o[l] g₁) (h₂ : ) :
f =o[l] g₂
instance Asymptotics.transIsLittleOIsEquivalent {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [Norm β₂] {l : } :
Equations
• Asymptotics.transIsLittleOIsEquivalent = { trans := }
theorem Asymptotics.IsEquivalent.trans_isTheta {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [Norm β₂] {l : } {f : αβ} {g₁ : αβ} {g₂ : αβ₂} (h : ) (h₂ : g₁ =Θ[l] g₂) :
f =Θ[l] g₂
instance Asymptotics.transIsEquivalentIsTheta {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [Norm β₂] {l : } :
Equations
• Asymptotics.transIsEquivalentIsTheta = { trans := }
theorem Asymptotics.IsTheta.trans_isEquivalent {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [Norm β₂] {l : } {f : αβ₂} {g₁ : αβ} {g₂ : αβ} (h : f =Θ[l] g₁) (h₂ : ) :
f =Θ[l] g₂
instance Asymptotics.transIsThetaIsEquivalent {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [Norm β₂] {l : } :
Equations
• Asymptotics.transIsThetaIsEquivalent = { trans := }