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} [NormedAddCommGroup β] (l : Filter α) (u : α → β) (v : α → β) : Prop

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

• Asymptotics.IsEquivalent l u v = (u - v) =o[l] v

def Asymptotics.«term_~[_]_» : Lean.TrailingParserDescr

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.

theorem Asymptotics.IsEquivalent.isLittleO {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {v : α → β} {l : Filter α} (h : Asymptotics.IsEquivalent l u v) : (u - v) =o[l] v

theorem Asymptotics.IsEquivalent.isBigO {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {v : α → β} {l : Filter α} (h : Asymptotics.IsEquivalent l u v) : u =O[l] v

theorem Asymptotics.IsEquivalent.isBigO_symm {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {v : α → β} {l : Filter α} (h : Asymptotics.IsEquivalent l u v) : v =O[l] u

theorem Asymptotics.IsEquivalent.isTheta {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {v : α → β} {l : Filter α} (h : Asymptotics.IsEquivalent l u v) : u =Θ[l] v

theorem Asymptotics.IsEquivalent.isTheta_symm {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {v : α → β} {l : Filter α} (h : Asymptotics.IsEquivalent l u v) : v =Θ[l] u

theorem Asymptotics.IsEquivalent.refl {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {l : Filter α} : Asymptotics.IsEquivalent l u u

theorem Asymptotics.IsEquivalent.symm {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {v : α → β} {l : Filter α} (h : Asymptotics.IsEquivalent l u v) : Asymptotics.IsEquivalent l v u

theorem Asymptotics.IsEquivalent.trans {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {l : Filter α} {u : α → β} {v : α → β} {w : α → β} (huv : Asymptotics.IsEquivalent l u v) (hvw : Asymptotics.IsEquivalent l v w) : Asymptotics.IsEquivalent l u w

theorem Asymptotics.IsEquivalent.congr_left {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {v : α → β} {w : α → β} {l : Filter α} (huv : Asymptotics.IsEquivalent l u v) (huw : u =ᶠ[l] w) : Asymptotics.IsEquivalent l w v

theorem Asymptotics.IsEquivalent.congr_right {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {v : α → β} {w : α → β} {l : Filter α} (huv : Asymptotics.IsEquivalent l u v) (hvw : v =ᶠ[l] w) : Asymptotics.IsEquivalent l u w

theorem Asymptotics.isEquivalent_zero_iff_eventually_zero {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {l : Filter α} : Asymptotics.IsEquivalent l u 0 ↔ u =ᶠ[l] 0

theorem Asymptotics.isEquivalent_zero_iff_isBigO_zero {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {l : Filter α} : Asymptotics.IsEquivalent l u 0 ↔ u =O[l] 0

theorem Asymptotics.isEquivalent_const_iff_tendsto {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {l : Filter α} {c : β} (h : c ≠ 0) : Asymptotics.IsEquivalent l u (Function.const α c) ↔ Filter.Tendsto u l (nhds c)

theorem Asymptotics.IsEquivalent.tendsto_const {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {l : Filter α} {c : β} (hu : Asymptotics.IsEquivalent l u (Function.const α c)) : Filter.Tendsto u l (nhds c)

theorem Asymptotics.IsEquivalent.tendsto_nhds {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {v : α → β} {l : Filter α} {c : β} (huv : Asymptotics.IsEquivalent l u v) (hu : Filter.Tendsto u l (nhds c)) : Filter.Tendsto v l (nhds c)

theorem Asymptotics.IsEquivalent.tendsto_nhds_iff {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {v : α → β} {l : Filter α} {c : β} (huv : Asymptotics.IsEquivalent l u v) : Filter.Tendsto u l (nhds c) ↔ Filter.Tendsto v l (nhds c)

theorem Asymptotics.IsEquivalent.add_isLittleO {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {v : α → β} {w : α → β} {l : Filter α} (huv : Asymptotics.IsEquivalent l u v) (hwv : w =o[l] v) : Asymptotics.IsEquivalent l (u + w) v

theorem Asymptotics.IsEquivalent.sub_isLittleO {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {v : α → β} {w : α → β} {l : Filter α} (huv : Asymptotics.IsEquivalent l u v) (hwv : w =o[l] v) : Asymptotics.IsEquivalent l (u - w) v

theorem Asymptotics.IsLittleO.add_isEquivalent {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {v : α → β} {w : α → β} {l : Filter α} (hu : u =o[l] w) (hv : Asymptotics.IsEquivalent l v w) : Asymptotics.IsEquivalent l (u + v) w

theorem Asymptotics.IsLittleO.isEquivalent {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {v : α → β} {l : Filter α} (huv : (u - v) =o[l] v) : Asymptotics.IsEquivalent l u v

theorem Asymptotics.IsEquivalent.neg {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u : α → β} {v : α → β} {l : Filter α} (huv : Asymptotics.IsEquivalent l u v) : Asymptotics.IsEquivalent l (fun (x : α) => -u x) fun (x : α) => -v x

theorem Asymptotics.isEquivalent_iff_exists_eq_mul {α : Type u_1} {β : Type u_2} [NormedField β] {u : α → β} {v : α → β} {l : Filter α} : Asymptotics.IsEquivalent l u v ↔ ∃ (φ : α → β) (_ : Filter.Tendsto φ l (nhds 1)), u =ᶠ[l] φ * v

theorem Asymptotics.IsEquivalent.exists_eq_mul {α : Type u_1} {β : Type u_2} [NormedField β] {u : α → β} {v : α → β} {l : Filter α} (huv : Asymptotics.IsEquivalent l u v) : ∃ (φ : α → β) (_ : Filter.Tendsto φ l (nhds 1)), u =ᶠ[l] φ * v

theorem Asymptotics.isEquivalent_of_tendsto_one {α : Type u_1} {β : Type u_2} [NormedField β] {u : α → β} {v : α → β} {l : Filter α} (hz : ∀ᶠ (x : α) in l, v x = 0 → u x = 0) (huv : Filter.Tendsto (u / v) l (nhds 1)) : Asymptotics.IsEquivalent l u v

theorem Asymptotics.isEquivalent_of_tendsto_one' {α : Type u_1} {β : Type u_2} [NormedField β] {u : α → β} {v : α → β} {l : Filter α} (hz : ∀ (x : α), v x = 0 → u x = 0) (huv : Filter.Tendsto (u / v) l (nhds 1)) : Asymptotics.IsEquivalent l u v

theorem Asymptotics.isEquivalent_iff_tendsto_one {α : Type u_1} {β : Type u_2} [NormedField β] {u : α → β} {v : α → β} {l : Filter α} (hz : ∀ᶠ (x : α) in l, v x ≠ 0) : Asymptotics.IsEquivalent l u v ↔ Filter.Tendsto (u / v) l (nhds 1)

theorem Asymptotics.IsEquivalent.smul {α : Type u_1} {E : Type u_2} {𝕜 : Type u_3} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {a : α → 𝕜} {b : α → 𝕜} {u : α → E} {v : α → E} {l : Filter α} (hab : Asymptotics.IsEquivalent l a b) (huv : Asymptotics.IsEquivalent l u v) : 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} [NormedField β] {t : α → β} {u : α → β} {v : α → β} {w : α → β} {l : Filter α} (htu : Asymptotics.IsEquivalent l t u) (hvw : Asymptotics.IsEquivalent l v w) : Asymptotics.IsEquivalent l (t * v) (u * w)

theorem Asymptotics.IsEquivalent.inv {α : Type u_1} {β : Type u_2} [NormedField β] {u : α → β} {v : α → β} {l : Filter α} (huv : Asymptotics.IsEquivalent l u v) : Asymptotics.IsEquivalent l (fun (x : α) => (u x)⁻¹) fun (x : α) => (v x)⁻¹

theorem Asymptotics.IsEquivalent.div {α : Type u_1} {β : Type u_2} [NormedField β] {t : α → β} {u : α → β} {v : α → β} {w : α → β} {l : Filter α} (htu : Asymptotics.IsEquivalent l t u) (hvw : Asymptotics.IsEquivalent l v w) : 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} [NormedLinearOrderedField β] {u : α → β} {v : α → β} {l : Filter α} [OrderTopology β] (huv : Asymptotics.IsEquivalent l u v) (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} [NormedLinearOrderedField β] {u : α → β} {v : α → β} {l : Filter α} [OrderTopology β] (huv : Asymptotics.IsEquivalent l u v) : Filter.Tendsto u l Filter.atTop ↔ Filter.Tendsto v l Filter.atTop

theorem Asymptotics.IsEquivalent.tendsto_atBot {α : Type u_1} {β : Type u_2} [NormedLinearOrderedField β] {u : α → β} {v : α → β} {l : Filter α} [OrderTopology β] (huv : Asymptotics.IsEquivalent l u v) (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} [NormedLinearOrderedField β] {u : α → β} {v : α → β} {l : Filter α} [OrderTopology β] (huv : Asymptotics.IsEquivalent l u v) : Filter.Tendsto u l Filter.atBot ↔ Filter.Tendsto v l Filter.atBot

theorem Filter.EventuallyEq.isEquivalent {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {l : Filter α} {u : α → β} {v : α → β} (h : u =ᶠ[l] v) : Asymptotics.IsEquivalent l u v

theorem Filter.EventuallyEq.trans_isEquivalent {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {l : Filter α} {f : α → β} {g₁ : α → β} {g₂ : α → β} (h : f =ᶠ[l] g₁) (h₂ : Asymptotics.IsEquivalent l g₁ g₂) : Asymptotics.IsEquivalent l f g₂

instance Asymptotics.transIsEquivalentIsEquivalent {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {l : Filter α} : Trans (Asymptotics.IsEquivalent l) (Asymptotics.IsEquivalent l) (Asymptotics.IsEquivalent l)

Equations

• One or more equations did not get rendered due to their size.

instance Asymptotics.transEventuallyEqIsEquivalent {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {l : Filter α} : Trans (Filter.EventuallyEq l) (Asymptotics.IsEquivalent l) (Asymptotics.IsEquivalent l)

Equations

• Asymptotics.transEventuallyEqIsEquivalent = { trans := (_ : ∀ {a b c : α → β}, a =ᶠ[l] b → Asymptotics.IsEquivalent l b c → Asymptotics.IsEquivalent l a c) }

theorem Asymptotics.IsEquivalent.trans_eventuallyEq {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {l : Filter α} {f : α → β} {g₁ : α → β} {g₂ : α → β} (h : Asymptotics.IsEquivalent l f g₁) (h₂ : g₁ =ᶠ[l] g₂) : Asymptotics.IsEquivalent l f g₂

instance Asymptotics.transIsEquivalentEventuallyEq {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {l : Filter α} : Trans (Asymptotics.IsEquivalent l) (Filter.EventuallyEq l) (Asymptotics.IsEquivalent l)

Equations

• Asymptotics.transIsEquivalentEventuallyEq = { trans := (_ : ∀ {a b c : α → β}, Asymptotics.IsEquivalent l a b → b =ᶠ[l] c → Asymptotics.IsEquivalent l a c) }

theorem Asymptotics.IsEquivalent.trans_isBigO {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [NormedAddCommGroup β] [Norm β₂] {l : Filter α} {f : α → β} {g₁ : α → β} {g₂ : α → β₂} (h : Asymptotics.IsEquivalent l f g₁) (h₂ : g₁ =O[l] g₂) : f =O[l] g₂

instance Asymptotics.transIsEquivalentIsBigO {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [NormedAddCommGroup β] [Norm β₂] {l : Filter α} : Trans (Asymptotics.IsEquivalent l) (Asymptotics.IsBigO l) (Asymptotics.IsBigO l)

Equations

• Asymptotics.transIsEquivalentIsBigO = { trans := (_ : ∀ {a b : α → β} {c : α → β₂}, Asymptotics.IsEquivalent l a b → b =O[l] c → a =O[l] c) }

theorem Asymptotics.IsBigO.trans_isEquivalent {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [NormedAddCommGroup β] [Norm β₂] {l : Filter α} {f : α → β₂} {g₁ : α → β} {g₂ : α → β} (h : f =O[l] g₁) (h₂ : Asymptotics.IsEquivalent l g₁ g₂) : f =O[l] g₂

instance Asymptotics.transIsBigOIsEquivalent {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [NormedAddCommGroup β] [Norm β₂] {l : Filter α} : Trans (Asymptotics.IsBigO l) (Asymptotics.IsEquivalent l) (Asymptotics.IsBigO l)

Equations

• Asymptotics.transIsBigOIsEquivalent = { trans := (_ : ∀ {a : α → β₂} {b c : α → β}, a =O[l] b → Asymptotics.IsEquivalent l b c → a =O[l] c) }

theorem Asymptotics.IsEquivalent.trans_isLittleO {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [NormedAddCommGroup β] [Norm β₂] {l : Filter α} {f : α → β} {g₁ : α → β} {g₂ : α → β₂} (h : Asymptotics.IsEquivalent l f g₁) (h₂ : g₁ =o[l] g₂) : f =o[l] g₂

instance Asymptotics.transIsEquivalentIsLittleO {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [NormedAddCommGroup β] [Norm β₂] {l : Filter α} : Trans (Asymptotics.IsEquivalent l) (Asymptotics.IsLittleO l) (Asymptotics.IsLittleO l)

Equations

• Asymptotics.transIsEquivalentIsLittleO = { trans := (_ : ∀ {a b : α → β} {c : α → β₂}, Asymptotics.IsEquivalent l a b → b =o[l] c → a =o[l] c) }

theorem Asymptotics.IsLittleO.trans_isEquivalent {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [NormedAddCommGroup β] [Norm β₂] {l : Filter α} {f : α → β₂} {g₁ : α → β} {g₂ : α → β} (h : f =o[l] g₁) (h₂ : Asymptotics.IsEquivalent l g₁ g₂) : f =o[l] g₂

instance Asymptotics.transIsLittleOIsEquivalent {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [NormedAddCommGroup β] [Norm β₂] {l : Filter α} : Trans (Asymptotics.IsLittleO l) (Asymptotics.IsEquivalent l) (Asymptotics.IsLittleO l)

Equations

• Asymptotics.transIsLittleOIsEquivalent = { trans := (_ : ∀ {a : α → β₂} {b c : α → β}, a =o[l] b → Asymptotics.IsEquivalent l b c → a =o[l] c) }

theorem Asymptotics.IsEquivalent.trans_isTheta {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [NormedAddCommGroup β] [Norm β₂] {l : Filter α} {f : α → β} {g₁ : α → β} {g₂ : α → β₂} (h : Asymptotics.IsEquivalent l f g₁) (h₂ : g₁ =Θ[l] g₂) : f =Θ[l] g₂

instance Asymptotics.transIsEquivalentIsTheta {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [NormedAddCommGroup β] [Norm β₂] {l : Filter α} : Trans (Asymptotics.IsEquivalent l) (Asymptotics.IsTheta l) (Asymptotics.IsTheta l)

Equations

• Asymptotics.transIsEquivalentIsTheta = { trans := (_ : ∀ {a b : α → β} {c : α → β₂}, Asymptotics.IsEquivalent l a b → b =Θ[l] c → a =Θ[l] c) }

theorem Asymptotics.IsTheta.trans_isEquivalent {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [NormedAddCommGroup β] [Norm β₂] {l : Filter α} {f : α → β₂} {g₁ : α → β} {g₂ : α → β} (h : f =Θ[l] g₁) (h₂ : Asymptotics.IsEquivalent l g₁ g₂) : f =Θ[l] g₂

instance Asymptotics.transIsThetaIsEquivalent {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [NormedAddCommGroup β] [Norm β₂] {l : Filter α} : Trans (Asymptotics.IsTheta l) (Asymptotics.IsEquivalent l) (Asymptotics.IsTheta l)

Equations

• Asymptotics.transIsThetaIsEquivalent = { trans := (_ : ∀ {a : α → β₂} {b c : α → β}, a =Θ[l] b → Asymptotics.IsEquivalent l b c → a =Θ[l] c) }