Documentation

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

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.

Notation #

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 : α → β) :

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.

Equations

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

Instances For

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

Lean.TrailingParserDescr

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.

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

v =O[l] u

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

u =Θ[l] v

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

v =Θ[l] u

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

IsEquivalent l u u

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

IsEquivalent l v u

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

IsEquivalent l u w

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

IsEquivalent l w v

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

IsEquivalent l u w

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

IsEquivalent l u 0 ↔ u =ᶠ[l] 0

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

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) :

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 : 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 : 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 : 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 : IsEquivalent l u v) (hwv : w =o[l] v) :

IsEquivalent l (u + w) v

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

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 : IsEquivalent l v w) :

IsEquivalent l (u + v) w

theorem Asymptotics.IsEquivalent.add_const_of_norm_tendsto_atTop {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u v : α → β} {l : Filter α} {c : β} (huv : IsEquivalent l u v) (hv : Filter.Tendsto (norm ∘ v) l Filter.atTop) :

IsEquivalent l (fun (x : α) => u x + c) v

theorem Asymptotics.IsEquivalent.const_add_of_norm_tendsto_atTop {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u v : α → β} {l : Filter α} {c : β} (huv : IsEquivalent l u v) (hv : Filter.Tendsto (norm ∘ v) l Filter.atTop) :

IsEquivalent l (fun (x : α) => c + u x) v

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

IsEquivalent l u v

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

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 α} :

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 : 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)) :

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)) :

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) :

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 v : α → E} {l : Filter α} (hab : IsEquivalent l a b) (huv : IsEquivalent l u v) :

IsEquivalent l (fun (x : α) => a x • u x) fun (x : α) => b x • v x

theorem Asymptotics.IsEquivalent.mul {α : Type u_1} {β : Type u_3} [NormedField β] {t u v w : α → β} {l : Filter α} (htu : IsEquivalent l t u) (hvw : IsEquivalent l v w) :

IsEquivalent l (t * v) (u * w)

theorem Asymptotics.IsEquivalent.listProd {α : Type u_1} {ι : Type u_2} {β : Type u_3} [NormedField β] {l : Filter α} {L : List ι} {f g : ι → α → β} (h : ∀ i ∈ L, IsEquivalent l (f i) (g i)) :

IsEquivalent l (fun (x : α) => (List.map (fun (x_1 : ι) => f x_1 x) L).prod) fun (x : α) => (List.map (fun (x_1 : ι) => g x_1 x) L).prod

theorem Asymptotics.IsEquivalent.multisetProd {α : Type u_1} {ι : Type u_2} {β : Type u_3} [NormedField β] {l : Filter α} {s : Multiset ι} {f g : ι → α → β} (h : ∀ i ∈ s, IsEquivalent l (f i) (g i)) :

IsEquivalent l (fun (x : α) => (Multiset.map (fun (x_1 : ι) => f x_1 x) s).prod) fun (x : α) => (Multiset.map (fun (x_1 : ι) => g x_1 x) s).prod

theorem Asymptotics.IsEquivalent.finsetProd {α : Type u_1} {ι : Type u_2} {β : Type u_3} [NormedField β] {l : Filter α} {s : Finset ι} {f g : ι → α → β} (h : ∀ i ∈ s, IsEquivalent l (f i) (g i)) :

IsEquivalent l (fun (x : α) => ∏ i ∈ s, f i x) fun (x : α) => ∏ i ∈ s, g i x

theorem Asymptotics.IsEquivalent.inv {α : Type u_1} {β : Type u_3} [NormedField β] {u v : α → β} {l : Filter α} (huv : IsEquivalent l u v) :

IsEquivalent l u⁻¹ v⁻¹

theorem Asymptotics.IsEquivalent.div {α : Type u_1} {β : Type u_3} [NormedField β] {t u v w : α → β} {l : Filter α} (htu : IsEquivalent l t u) (hvw : IsEquivalent l v w) :

IsEquivalent l (t / v) (u / w)

theorem Asymptotics.IsEquivalent.pow {α : Type u_1} {β : Type u_3} [NormedField β] {t u : α → β} {l : Filter α} (h : IsEquivalent l t u) (n : ℕ) :

IsEquivalent l (t ^ n) (u ^ n)

theorem Asymptotics.IsEquivalent.zpow {α : Type u_1} {β : Type u_3} [NormedField β] {t u : α → β} {l : Filter α} (h : IsEquivalent l t u) (z : ℤ) :

IsEquivalent l (t ^ z) (u ^ z)

theorem Asymptotics.IsEquivalent.tendsto_atTop {α : Type u_1} {β : Type u_2} [NormedField β] [LinearOrder β] [IsStrictOrderedRing β] {u v : α → β} {l : Filter α} [OrderTopology β] (huv : 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} [NormedField β] [LinearOrder β] [IsStrictOrderedRing β] {u v : α → β} {l : Filter α} [OrderTopology β] (huv : 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} [NormedField β] [LinearOrder β] [IsStrictOrderedRing β] {u v : α → β} {l : Filter α} [OrderTopology β] (huv : 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} [NormedField β] [LinearOrder β] [IsStrictOrderedRing β] {u v : α → β} {l : Filter α} [OrderTopology β] (huv : IsEquivalent l u v) :

Filter.Tendsto u l Filter.atBot ↔ Filter.Tendsto v l Filter.atBot

theorem Asymptotics.IsEquivalent.add_add_of_nonneg {α : Type u_1} {u v t w : α → ℝ} {l : Filter α} (hu : 0 ≤ v) (hw : 0 ≤ w) (htu : IsEquivalent l u v) (hvw : IsEquivalent l t w) :

IsEquivalent l (u + t) (v + w)

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 (IsEquivalent l) (IsEquivalent l) (IsEquivalent l)

Equations

Asymptotics.transIsEquivalentIsEquivalent = { trans := ⋯ }

instance Asymptotics.transEventuallyEqIsEquivalent {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {l : Filter α} :

Trans l.EventuallyEq (IsEquivalent l) (IsEquivalent l)

Equations

Asymptotics.transEventuallyEqIsEquivalent = { trans := ⋯ }

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

IsEquivalent l f g₂

instance Asymptotics.transIsEquivalentEventuallyEq {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {l : Filter α} :

Trans (IsEquivalent l) l.EventuallyEq (IsEquivalent l)

Equations

Asymptotics.transIsEquivalentEventuallyEq = { trans := ⋯ }

theorem Asymptotics.IsEquivalent.trans_isBigO {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [NormedAddCommGroup β] [Norm β₂] {l : Filter α} {f g₁ : α → β} {g₂ : α → β₂} (h : 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 (IsEquivalent l) (IsBigO l) (IsBigO l)

Equations

Asymptotics.transIsEquivalentIsBigO = { trans := ⋯ }

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₂ : 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 (IsBigO l) (IsEquivalent l) (IsBigO l)

Equations

Asymptotics.transIsBigOIsEquivalent = { trans := ⋯ }

theorem Asymptotics.IsEquivalent.trans_isLittleO {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [NormedAddCommGroup β] [Norm β₂] {l : Filter α} {f g₁ : α → β} {g₂ : α → β₂} (h : 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 (IsEquivalent l) (IsLittleO l) (IsLittleO l)

Equations

Asymptotics.transIsEquivalentIsLittleO = { trans := ⋯ }

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₂ : 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 (IsLittleO l) (IsEquivalent l) (IsLittleO l)

Equations

Asymptotics.transIsLittleOIsEquivalent = { trans := ⋯ }

theorem Asymptotics.IsEquivalent.trans_isTheta {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [NormedAddCommGroup β] [Norm β₂] {l : Filter α} {f g₁ : α → β} {g₂ : α → β₂} (h : 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 (IsEquivalent l) (IsTheta l) (IsTheta l)

Equations

Asymptotics.transIsEquivalentIsTheta = { trans := ⋯ }

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₂ : IsEquivalent l g₁ g₂) :

f =Θ[l] g₂

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

Trans (IsTheta l) (IsEquivalent l) (IsTheta l)

Equations

Asymptotics.transIsThetaIsEquivalent = { trans := ⋯ }

theorem Asymptotics.IsEquivalent.comp_tendsto {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {l : Filter α} {α₂ : Type u_4} {f g : α₂ → β} {l' : Filter α₂} (hfg : IsEquivalent l' f g) {k : α → α₂} (hk : Filter.Tendsto k l l') :

IsEquivalent l (f ∘ k) (g ∘ k)

@[simp]

theorem Asymptotics.isEquivalent_map {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {l : Filter α} {α₂ : Type u_4} {f g : α₂ → β} {k : α → α₂} :

IsEquivalent (Filter.map k l) f g ↔ IsEquivalent l (f ∘ k) (g ∘ k)

theorem Asymptotics.IsEquivalent.mono {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {l : Filter α} {f g : α → β} {l' : Filter α} (h : IsEquivalent l' f g) (hl : l ≤ l') :

IsEquivalent l f g