Documentation

Mathlib.Analysis.Asymptotics.Theta

Asymptotic equivalence up to a constant #

In this file we define Asymptotics.IsTheta l f g (notation: f =Θ[l] g) as f =O[l] g ∧ g =O[l] f, then prove basic properties of this equivalence relation.

def Asymptotics.IsTheta {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] (l : Filter α) (f : αE) (g : αF) :

We say that f is Θ(g) along a filter l (notation: f =Θ[l] g) if f =O[l] g and g =O[l] f.

Equations
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem Asymptotics.IsBigO.antisymm {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} (h₁ : f =O[l] g) (h₂ : g =O[l] f) :
      f =Θ[l] g
      theorem Asymptotics.IsTheta.isBigO {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} (h : f =Θ[l] g) :
      f =O[l] g
      theorem Asymptotics.IsTheta.isBigO_symm {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} (h : f =Θ[l] g) :
      g =O[l] f
      theorem Asymptotics.isTheta_refl {α : Type u_1} {E : Type u_3} [Norm E] (f : αE) (l : Filter α) :
      f =Θ[l] f
      theorem Asymptotics.isTheta_rfl {α : Type u_1} {E : Type u_3} [Norm E] {f : αE} {l : Filter α} :
      f =Θ[l] f
      theorem Asymptotics.IsTheta.symm {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} (h : f =Θ[l] g) :
      g =Θ[l] f
      theorem Asymptotics.isTheta_comm {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} :
      f =Θ[l] g g =Θ[l] f
      theorem Asymptotics.IsTheta.trans {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} {f : αE} {g : αF'} {k : αG} (h₁ : f =Θ[l] g) (h₂ : g =Θ[l] k) :
      f =Θ[l] k
      Equations
      • Asymptotics.instTransForAllForAllForAllIsThetaToNormIsThetaIsTheta = { trans := (_ : ∀ {a : αE} {b : αF'} {c : αG}, a =Θ[l] bb =Θ[l] ca =Θ[l] c) }
      theorem Asymptotics.IsBigO.trans_isTheta {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} {f : αE} {g : αF'} {k : αG} (h₁ : f =O[l] g) (h₂ : g =Θ[l] k) :
      f =O[l] k
      Equations
      • Asymptotics.instTransForAllForAllForAllIsBigOToNormIsThetaIsBigO = { trans := (_ : ∀ {a : αE} {b : αF'} {c : αG}, a =O[l] bb =Θ[l] ca =O[l] c) }
      theorem Asymptotics.IsTheta.trans_isBigO {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} {f : αE} {g : αF'} {k : αG} (h₁ : f =Θ[l] g) (h₂ : g =O[l] k) :
      f =O[l] k
      Equations
      • Asymptotics.instTransForAllForAllForAllIsThetaToNormIsBigOIsBigO = { trans := (_ : ∀ {a : αE} {b : αF'} {c : αG}, a =Θ[l] bb =O[l] ca =O[l] c) }
      theorem Asymptotics.IsLittleO.trans_isTheta {α : Type u_1} {E : Type u_3} {F : Type u_4} {G' : Type u_8} [Norm E] [Norm F] [SeminormedAddCommGroup G'] {l : Filter α} {f : αE} {g : αF} {k : αG'} (h₁ : f =o[l] g) (h₂ : g =Θ[l] k) :
      f =o[l] k
      Equations
      • Asymptotics.instTransForAllForAllForAllIsLittleOToNormIsThetaToNormIsLittleO = { trans := (_ : ∀ {a : αE} {b : αF'} {c : αG'}, a =o[l] bb =Θ[l] ca =o[l] c) }
      theorem Asymptotics.IsTheta.trans_isLittleO {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} {f : αE} {g : αF'} {k : αG} (h₁ : f =Θ[l] g) (h₂ : g =o[l] k) :
      f =o[l] k
      Equations
      • Asymptotics.instTransForAllForAllForAllIsThetaToNormIsLittleOIsLittleO = { trans := (_ : ∀ {a : αE} {b : αF'} {c : αG}, a =Θ[l] bb =o[l] ca =o[l] c) }
      theorem Asymptotics.IsTheta.trans_eventuallyEq {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f : αE} {g₁ : αF} {g₂ : αF} (h : f =Θ[l] g₁) (hg : g₁ =ᶠ[l] g₂) :
      f =Θ[l] g₂
      Equations
      • Asymptotics.instTransForAllForAllIsThetaEventuallyEq = { trans := (_ : ∀ {a : αE} {b c : αF}, a =Θ[l] bb =ᶠ[l] ca =Θ[l] c) }
      theorem Filter.EventuallyEq.trans_isTheta {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f₁ : αE} {f₂ : αE} {g : αF} (hf : f₁ =ᶠ[l] f₂) (h : f₂ =Θ[l] g) :
      f₁ =Θ[l] g
      Equations
      • Asymptotics.instTransForAllForAllEventuallyEqIsTheta = { trans := (_ : ∀ {a b : αE} {c : αF}, a =ᶠ[l] bb =Θ[l] ca =Θ[l] c) }
      @[simp]
      theorem Asymptotics.isTheta_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {f' : αE'} {l : Filter α} :
      (fun x => f' x) =Θ[l] g f' =Θ[l] g
      @[simp]
      theorem Asymptotics.isTheta_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : αE} {g' : αF'} {l : Filter α} :
      (f =Θ[l] fun x => g' x) f =Θ[l] g'
      theorem Asymptotics.IsTheta.of_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {f' : αE'} {l : Filter α} :
      (fun x => f' x) =Θ[l] gf' =Θ[l] g

      Alias of the forward direction of Asymptotics.isTheta_norm_left.

      theorem Asymptotics.IsTheta.norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {f' : αE'} {l : Filter α} :
      f' =Θ[l] g(fun x => f' x) =Θ[l] g

      Alias of the reverse direction of Asymptotics.isTheta_norm_left.

      theorem Asymptotics.IsTheta.of_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : αE} {g' : αF'} {l : Filter α} :
      (f =Θ[l] fun x => g' x) → f =Θ[l] g'

      Alias of the forward direction of Asymptotics.isTheta_norm_right.

      theorem Asymptotics.IsTheta.norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : αE} {g' : αF'} {l : Filter α} :
      f =Θ[l] g'f =Θ[l] fun x => g' x

      Alias of the reverse direction of Asymptotics.isTheta_norm_right.

      theorem Asymptotics.isTheta_of_norm_eventuallyEq {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} (h : (fun x => f x) =ᶠ[l] fun x => g x) :
      f =Θ[l] g
      theorem Asymptotics.isTheta_of_norm_eventuallyEq' {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {f' : αE'} {l : Filter α} {g : α} (h : (fun x => f' x) =ᶠ[l] g) :
      f' =Θ[l] g
      theorem Asymptotics.IsTheta.isLittleO_congr_left {α : Type u_1} {G : Type u_5} {E' : Type u_6} {F' : Type u_7} [Norm G] [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {k : αG} {f' : αE'} {g' : αF'} {l : Filter α} (h : f' =Θ[l] g') :
      f' =o[l] k g' =o[l] k
      theorem Asymptotics.IsTheta.isLittleO_congr_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [Norm E] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f : αE} {g' : αF'} {k' : αG'} {l : Filter α} (h : g' =Θ[l] k') :
      f =o[l] g' f =o[l] k'
      theorem Asymptotics.IsTheta.isBigO_congr_left {α : Type u_1} {G : Type u_5} {E' : Type u_6} {F' : Type u_7} [Norm G] [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {k : αG} {f' : αE'} {g' : αF'} {l : Filter α} (h : f' =Θ[l] g') :
      f' =O[l] k g' =O[l] k
      theorem Asymptotics.IsTheta.isBigO_congr_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [Norm E] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f : αE} {g' : αF'} {k' : αG'} {l : Filter α} (h : g' =Θ[l] k') :
      f =O[l] g' f =O[l] k'
      theorem Asymptotics.IsTheta.mono {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} {l' : Filter α} (h : f =Θ[l] g) (hl : l' l) :
      f =Θ[l'] g
      theorem Asymptotics.IsTheta.sup {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : αE'} {g' : αF'} {l : Filter α} {l' : Filter α} (h : f' =Θ[l] g') (h' : f' =Θ[l'] g') :
      f' =Θ[l l'] g'
      @[simp]
      theorem Asymptotics.isTheta_sup {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : αE'} {g' : αF'} {l : Filter α} {l' : Filter α} :
      f' =Θ[l l'] g' f' =Θ[l] g' f' =Θ[l'] g'
      theorem Asymptotics.IsTheta.eq_zero_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : αE''} {g'' : αF''} {l : Filter α} (h : f'' =Θ[l] g'') :
      ∀ᶠ (x : α) in l, f'' x = 0 g'' x = 0
      theorem Asymptotics.IsTheta.tendsto_zero_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : αE''} {g'' : αF''} {l : Filter α} (h : f'' =Θ[l] g'') :
      theorem Asymptotics.IsTheta.tendsto_norm_atTop_iff {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : αE'} {g' : αF'} {l : Filter α} (h : f' =Θ[l] g') :
      Filter.Tendsto (norm f') l Filter.atTop Filter.Tendsto (norm g') l Filter.atTop
      theorem Asymptotics.IsTheta.isBoundedUnder_le_iff {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : αE'} {g' : αF'} {l : Filter α} (h : f' =Θ[l] g') :
      Filter.IsBoundedUnder (fun x x_1 => x x_1) l (norm f') Filter.IsBoundedUnder (fun x x_1 => x x_1) l (norm g')
      theorem Asymptotics.IsTheta.smul {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {𝕜 : Type u_14} {𝕜' : Type u_15} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} [NormedSpace 𝕜 E'] [NormedSpace 𝕜' F'] {f₁ : α𝕜} {f₂ : α𝕜'} {g₁ : αE'} {g₂ : αF'} (hf : f₁ =Θ[l] f₂) (hg : g₁ =Θ[l] g₂) :
      (fun x => f₁ x g₁ x) =Θ[l] fun x => f₂ x g₂ x
      theorem Asymptotics.IsTheta.mul {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} {f₁ : α𝕜} {f₂ : α𝕜} {g₁ : α𝕜'} {g₂ : α𝕜'} (h₁ : f₁ =Θ[l] g₁) (h₂ : f₂ =Θ[l] g₂) :
      (fun x => f₁ x * f₂ x) =Θ[l] fun x => g₁ x * g₂ x
      theorem Asymptotics.IsTheta.inv {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} {f : α𝕜} {g : α𝕜'} (h : f =Θ[l] g) :
      (fun x => (f x)⁻¹) =Θ[l] fun x => (g x)⁻¹
      @[simp]
      theorem Asymptotics.isTheta_inv {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} {f : α𝕜} {g : α𝕜'} :
      ((fun x => (f x)⁻¹) =Θ[l] fun x => (g x)⁻¹) f =Θ[l] g
      theorem Asymptotics.IsTheta.div {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} {f₁ : α𝕜} {f₂ : α𝕜} {g₁ : α𝕜'} {g₂ : α𝕜'} (h₁ : f₁ =Θ[l] g₁) (h₂ : f₂ =Θ[l] g₂) :
      (fun x => f₁ x / f₂ x) =Θ[l] fun x => g₁ x / g₂ x
      theorem Asymptotics.IsTheta.pow {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} {f : α𝕜} {g : α𝕜'} (h : f =Θ[l] g) (n : ) :
      (fun x => f x ^ n) =Θ[l] fun x => g x ^ n
      theorem Asymptotics.IsTheta.zpow {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [NormedField 𝕜] [NormedField 𝕜'] {l : Filter α} {f : α𝕜} {g : α𝕜'} (h : f =Θ[l] g) (n : ) :
      (fun x => f x ^ n) =Θ[l] fun x => g x ^ n
      theorem Asymptotics.isTheta_const_const {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {l : Filter α} {c₁ : E''} {c₂ : F''} (h₁ : c₁ 0) (h₂ : c₂ 0) :
      (fun x => c₁) =Θ[l] fun x => c₂
      @[simp]
      theorem Asymptotics.isTheta_const_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {l : Filter α} [Filter.NeBot l] {c₁ : E''} {c₂ : F''} :
      ((fun x => c₁) =Θ[l] fun x => c₂) (c₁ = 0 c₂ = 0)
      @[simp]
      theorem Asymptotics.isTheta_zero_left {α : Type u_1} {E' : Type u_6} {F'' : Type u_10} [SeminormedAddCommGroup E'] [NormedAddCommGroup F''] {g'' : αF''} {l : Filter α} :
      (fun x => 0) =Θ[l] g'' g'' =ᶠ[l] 0
      @[simp]
      theorem Asymptotics.isTheta_zero_right {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {f'' : αE''} {l : Filter α} :
      (f'' =Θ[l] fun x => 0) f'' =ᶠ[l] 0
      theorem Asymptotics.isTheta_const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_14} [Norm F] [SeminormedAddCommGroup E'] [NormedField 𝕜] {g : αF} {f' : αE'} {l : Filter α} [NormedSpace 𝕜 E'] {c : 𝕜} (hc : c 0) :
      (fun x => c f' x) =Θ[l] g f' =Θ[l] g
      theorem Asymptotics.IsTheta.const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_14} [Norm F] [SeminormedAddCommGroup E'] [NormedField 𝕜] {g : αF} {f' : αE'} {l : Filter α} [NormedSpace 𝕜 E'] {c : 𝕜} (hc : c 0) :
      f' =Θ[l] g(fun x => c f' x) =Θ[l] g

      Alias of the reverse direction of Asymptotics.isTheta_const_smul_left.

      theorem Asymptotics.IsTheta.of_const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_14} [Norm F] [SeminormedAddCommGroup E'] [NormedField 𝕜] {g : αF} {f' : αE'} {l : Filter α} [NormedSpace 𝕜 E'] {c : 𝕜} (hc : c 0) :
      (fun x => c f' x) =Θ[l] gf' =Θ[l] g

      Alias of the forward direction of Asymptotics.isTheta_const_smul_left.

      theorem Asymptotics.isTheta_const_smul_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} {𝕜 : Type u_14} [Norm E] [SeminormedAddCommGroup F'] [NormedField 𝕜] {f : αE} {g' : αF'} {l : Filter α} [NormedSpace 𝕜 F'] {c : 𝕜} (hc : c 0) :
      (f =Θ[l] fun x => c g' x) f =Θ[l] g'
      theorem Asymptotics.IsTheta.const_smul_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} {𝕜 : Type u_14} [Norm E] [SeminormedAddCommGroup F'] [NormedField 𝕜] {f : αE} {g' : αF'} {l : Filter α} [NormedSpace 𝕜 F'] {c : 𝕜} (hc : c 0) :
      f =Θ[l] g'f =Θ[l] fun x => c g' x

      Alias of the reverse direction of Asymptotics.isTheta_const_smul_right.

      theorem Asymptotics.IsTheta.of_const_smul_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} {𝕜 : Type u_14} [Norm E] [SeminormedAddCommGroup F'] [NormedField 𝕜] {f : αE} {g' : αF'} {l : Filter α} [NormedSpace 𝕜 F'] {c : 𝕜} (hc : c 0) :
      (f =Θ[l] fun x => c g' x) → f =Θ[l] g'

      Alias of the forward direction of Asymptotics.isTheta_const_smul_right.

      theorem Asymptotics.isTheta_const_mul_left {α : Type u_1} {F : Type u_4} {𝕜 : Type u_14} [Norm F] [NormedField 𝕜] {g : αF} {l : Filter α} {c : 𝕜} {f : α𝕜} (hc : c 0) :
      (fun x => c * f x) =Θ[l] g f =Θ[l] g
      theorem Asymptotics.IsTheta.of_const_mul_left {α : Type u_1} {F : Type u_4} {𝕜 : Type u_14} [Norm F] [NormedField 𝕜] {g : αF} {l : Filter α} {c : 𝕜} {f : α𝕜} (hc : c 0) :
      (fun x => c * f x) =Θ[l] gf =Θ[l] g

      Alias of the forward direction of Asymptotics.isTheta_const_mul_left.

      theorem Asymptotics.IsTheta.const_mul_left {α : Type u_1} {F : Type u_4} {𝕜 : Type u_14} [Norm F] [NormedField 𝕜] {g : αF} {l : Filter α} {c : 𝕜} {f : α𝕜} (hc : c 0) :
      f =Θ[l] g(fun x => c * f x) =Θ[l] g

      Alias of the reverse direction of Asymptotics.isTheta_const_mul_left.

      theorem Asymptotics.isTheta_const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_14} [Norm E] [NormedField 𝕜] {f : αE} {l : Filter α} {c : 𝕜} {g : α𝕜} (hc : c 0) :
      (f =Θ[l] fun x => c * g x) f =Θ[l] g
      theorem Asymptotics.IsTheta.of_const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_14} [Norm E] [NormedField 𝕜] {f : αE} {l : Filter α} {c : 𝕜} {g : α𝕜} (hc : c 0) :
      (f =Θ[l] fun x => c * g x) → f =Θ[l] g

      Alias of the forward direction of Asymptotics.isTheta_const_mul_right.

      theorem Asymptotics.IsTheta.const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_14} [Norm E] [NormedField 𝕜] {f : αE} {l : Filter α} {c : 𝕜} {g : α𝕜} (hc : c 0) :
      f =Θ[l] gf =Θ[l] fun x => c * g x

      Alias of the reverse direction of Asymptotics.isTheta_const_mul_right.

      theorem Asymptotics.IsTheta.add_isLittleO {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h : f₂ =o[l] f₁) :
      (f₁ + f₂) =Θ[l] f₁