# mathlib3documentation

analysis.asymptotics.theta

# Asymptotic equivalence up to a constant #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define asymptotics.is_Theta 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.is_Theta {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] (l : filter α) (f : α E) (g : α F) :
Prop

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
theorem asymptotics.is_O.antisymm {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α E} {g : α F} {l : filter α} (h₁ : f =O[l] g) (h₂ : g =O[l] f) :
f =Θ[l] g
@[refl]
theorem asymptotics.is_Theta_refl {α : Type u_1} {E : Type u_3} [has_norm E] (f : α E) (l : filter α) :
f =Θ[l] f
theorem asymptotics.is_Theta_rfl {α : Type u_1} {E : Type u_3} [has_norm E] {f : α E} {l : filter α} :
f =Θ[l] f
@[symm]
theorem asymptotics.is_Theta.symm {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α E} {g : α F} {l : filter α} (h : f =Θ[l] g) :
g =Θ[l] f
theorem asymptotics.is_Theta_comm {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α E} {g : α F} {l : filter α} :
f =Θ[l] g g =Θ[l] f
@[trans]
theorem asymptotics.is_Theta.trans {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [has_norm E] [has_norm G] {l : filter α} {f : α E} {g : α F'} {k : α G} (h₁ : f =Θ[l] g) (h₂ : g =Θ[l] k) :
f =Θ[l] k
@[trans]
theorem asymptotics.is_O.trans_is_Theta {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [has_norm E] [has_norm G] {l : filter α} {f : α E} {g : α F'} {k : α G} (h₁ : f =O[l] g) (h₂ : g =Θ[l] k) :
f =O[l] k
@[trans]
theorem asymptotics.is_Theta.trans_is_O {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [has_norm E] [has_norm G] {l : filter α} {f : α E} {g : α F'} {k : α G} (h₁ : f =Θ[l] g) (h₂ : g =O[l] k) :
f =O[l] k
@[trans]
theorem asymptotics.is_o.trans_is_Theta {α : Type u_1} {E : Type u_3} {F : Type u_4} {G' : Type u_8} [has_norm E] [has_norm F] {l : filter α} {f : α E} {g : α F} {k : α G'} (h₁ : f =o[l] g) (h₂ : g =Θ[l] k) :
f =o[l] k
@[trans]
theorem asymptotics.is_Theta.trans_is_o {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [has_norm E] [has_norm G] {l : filter α} {f : α E} {g : α F'} {k : α G} (h₁ : f =Θ[l] g) (h₂ : g =o[l] k) :
f =o[l] k
@[trans]
theorem asymptotics.is_Theta.trans_eventually_eq {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {l : filter α} {f : α E} {g₁ g₂ : α F} (h : f =Θ[l] g₁) (hg : g₁ =ᶠ[l] g₂) :
f =Θ[l] g₂
@[trans]
theorem filter.eventually_eq.trans_is_Theta {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {l : filter α} {f₁ f₂ : α E} {g : α F} (hf : f₁ =ᶠ[l] f₂) (h : f₂ =Θ[l] g) :
f₁ =Θ[l] g
@[simp]
theorem asymptotics.is_Theta_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {f' : α E'} {l : filter α} :
(λ (x : α), f' x) =Θ[l] g f' =Θ[l] g
@[simp]
theorem asymptotics.is_Theta_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l : filter α} :
(f =Θ[l] λ (x : α), g' x) f =Θ[l] g'
theorem asymptotics.is_Theta.of_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {f' : α E'} {l : filter α} :
(λ (x : α), f' x) =Θ[l] g f' =Θ[l] g

Alias of the forward direction of asymptotics.is_Theta_norm_left.

theorem asymptotics.is_Theta.norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {f' : α E'} {l : filter α} :
f' =Θ[l] g (λ (x : α), f' x) =Θ[l] g

Alias of the reverse direction of asymptotics.is_Theta_norm_left.

theorem asymptotics.is_Theta.of_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l : filter α} :
(f =Θ[l] λ (x : α), g' x) f =Θ[l] g'

Alias of the forward direction of asymptotics.is_Theta_norm_right.

theorem asymptotics.is_Theta.norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l : filter α} :
f =Θ[l] g' (f =Θ[l] λ (x : α), g' x)

Alias of the reverse direction of asymptotics.is_Theta_norm_right.

theorem asymptotics.is_Theta_of_norm_eventually_eq {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α E} {g : α F} {l : filter α} (h : (λ (x : α), f x) =ᶠ[l] λ (x : α), g x) :
f =Θ[l] g
theorem asymptotics.is_Theta_of_norm_eventually_eq' {α : Type u_1} {E' : Type u_6} {f' : α E'} {l : filter α} {g : α } (h : (λ (x : α), f' x) =ᶠ[l] g) :
f' =Θ[l] g
theorem asymptotics.is_Theta.is_o_congr_left {α : Type u_1} {G : Type u_5} {E' : Type u_6} {F' : Type u_7} [has_norm G] {k : α G} {f' : α E'} {g' : α F'} {l : filter α} (h : f' =Θ[l] g') :
f' =o[l] k g' =o[l] k
theorem asymptotics.is_Theta.is_o_congr_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [has_norm E] {f : α E} {g' : α F'} {k' : α G'} {l : filter α} (h : g' =Θ[l] k') :
f =o[l] g' f =o[l] k'
theorem asymptotics.is_Theta.is_O_congr_left {α : Type u_1} {G : Type u_5} {E' : Type u_6} {F' : Type u_7} [has_norm G] {k : α G} {f' : α E'} {g' : α F'} {l : filter α} (h : f' =Θ[l] g') :
f' =O[l] k g' =O[l] k
theorem asymptotics.is_Theta.is_O_congr_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [has_norm E] {f : α E} {g' : α F'} {k' : α G'} {l : filter α} (h : g' =Θ[l] k') :
f =O[l] g' f =O[l] k'
theorem asymptotics.is_Theta.mono {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α E} {g : α F} {l l' : filter α} (h : f =Θ[l] g) (hl : l' l) :
f =Θ[l'] g
theorem asymptotics.is_Theta.sup {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : α E'} {g' : α F'} {l l' : filter α} (h : f' =Θ[l] g') (h' : f' =Θ[l'] g') :
f' =Θ[l l'] g'
@[simp]
theorem asymptotics.is_Theta_sup {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : α E'} {g' : α F'} {l l' : filter α} :
f' =Θ[l l'] g' f' =Θ[l] g' f' =Θ[l'] g'
theorem asymptotics.is_Theta.eq_zero_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} {f'' : α E''} {g'' : α F''} {l : filter α} (h : f'' =Θ[l] g'') :
∀ᶠ (x : α) in l, f'' x = 0 g'' x = 0
theorem asymptotics.is_Theta.tendsto_zero_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} {f'' : α E''} {g'' : α F''} {l : filter α} (h : f'' =Θ[l] g'') :
l (nhds 0) l (nhds 0)
theorem asymptotics.is_Theta.tendsto_norm_at_top_iff {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : α E'} {g' : α F'} {l : filter α} (h : f' =Θ[l] g') :
theorem asymptotics.is_Theta.is_bounded_under_le_iff {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : α E'} {g' : α F'} {l : filter α} (h : f' =Θ[l] g') :
theorem asymptotics.is_Theta.smul {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {𝕜 : Type u_14} {𝕜' : Type u_15} [normed_field 𝕜] [normed_field 𝕜'] {l : filter α} [ E'] [ F'] {f₁ : α 𝕜} {f₂ : α 𝕜'} {g₁ : α E'} {g₂ : α F'} (hf : f₁ =Θ[l] f₂) (hg : g₁ =Θ[l] g₂) :
(λ (x : α), f₁ x g₁ x) =Θ[l] λ (x : α), f₂ x g₂ x
theorem asymptotics.is_Theta.mul {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [normed_field 𝕜] [normed_field 𝕜'] {l : filter α} {f₁ f₂ : α 𝕜} {g₁ g₂ : α 𝕜'} (h₁ : f₁ =Θ[l] g₁) (h₂ : f₂ =Θ[l] g₂) :
(λ (x : α), f₁ x * f₂ x) =Θ[l] λ (x : α), g₁ x * g₂ x
theorem asymptotics.is_Theta.inv {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [normed_field 𝕜] [normed_field 𝕜'] {l : filter α} {f : α 𝕜} {g : α 𝕜'} (h : f =Θ[l] g) :
(λ (x : α), (f x)⁻¹) =Θ[l] λ (x : α), (g x)⁻¹
@[simp]
theorem asymptotics.is_Theta_inv {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [normed_field 𝕜] [normed_field 𝕜'] {l : filter α} {f : α 𝕜} {g : α 𝕜'} :
((λ (x : α), (f x)⁻¹) =Θ[l] λ (x : α), (g x)⁻¹) f =Θ[l] g
theorem asymptotics.is_Theta.div {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [normed_field 𝕜] [normed_field 𝕜'] {l : filter α} {f₁ f₂ : α 𝕜} {g₁ g₂ : α 𝕜'} (h₁ : f₁ =Θ[l] g₁) (h₂ : f₂ =Θ[l] g₂) :
(λ (x : α), f₁ x / f₂ x) =Θ[l] λ (x : α), g₁ x / g₂ x
theorem asymptotics.is_Theta.pow {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [normed_field 𝕜] [normed_field 𝕜'] {l : filter α} {f : α 𝕜} {g : α 𝕜'} (h : f =Θ[l] g) (n : ) :
(λ (x : α), f x ^ n) =Θ[l] λ (x : α), g x ^ n
theorem asymptotics.is_Theta.zpow {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [normed_field 𝕜] [normed_field 𝕜'] {l : filter α} {f : α 𝕜} {g : α 𝕜'} (h : f =Θ[l] g) (n : ) :
(λ (x : α), f x ^ n) =Θ[l] λ (x : α), g x ^ n
theorem asymptotics.is_Theta_const_const {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} {l : filter α} {c₁ : E''} {c₂ : F''} (h₁ : c₁ 0) (h₂ : c₂ 0) :
(λ (x : α), c₁) =Θ[l] λ (x : α), c₂
@[simp]
theorem asymptotics.is_Theta_const_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} {l : filter α} [l.ne_bot] {c₁ : E''} {c₂ : F''} :
((λ (x : α), c₁) =Θ[l] λ (x : α), c₂) (c₁ = 0 c₂ = 0)
@[simp]
theorem asymptotics.is_Theta_zero_left {α : Type u_1} {E' : Type u_6} {F'' : Type u_10} {g'' : α F''} {l : filter α} :
(λ (x : α), 0) =Θ[l] g'' g'' =ᶠ[l] 0
@[simp]
theorem asymptotics.is_Theta_zero_right {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} {f'' : α E''} {l : filter α} :
(f'' =Θ[l] λ (x : α), 0) f'' =ᶠ[l] 0
theorem asymptotics.is_Theta_const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_14} [has_norm F] [normed_field 𝕜] {g : α F} {f' : α E'} {l : filter α} [ E'] {c : 𝕜} (hc : c 0) :
(λ (x : α), c f' x) =Θ[l] g f' =Θ[l] g
theorem asymptotics.is_Theta.of_const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_14} [has_norm F] [normed_field 𝕜] {g : α F} {f' : α E'} {l : filter α} [ E'] {c : 𝕜} (hc : c 0) :
(λ (x : α), c f' x) =Θ[l] g f' =Θ[l] g

Alias of the forward direction of asymptotics.is_Theta_const_smul_left.

theorem asymptotics.is_Theta.const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_14} [has_norm F] [normed_field 𝕜] {g : α F} {f' : α E'} {l : filter α} [ E'] {c : 𝕜} (hc : c 0) :
f' =Θ[l] g (λ (x : α), c f' x) =Θ[l] g

Alias of the reverse direction of asymptotics.is_Theta_const_smul_left.

theorem asymptotics.is_Theta_const_smul_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} {𝕜 : Type u_14} [has_norm E] [normed_field 𝕜] {f : α E} {g' : α F'} {l : filter α} [ F'] {c : 𝕜} (hc : c 0) :
(f =Θ[l] λ (x : α), c g' x) f =Θ[l] g'
theorem asymptotics.is_Theta.const_smul_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} {𝕜 : Type u_14} [has_norm E] [normed_field 𝕜] {f : α E} {g' : α F'} {l : filter α} [ F'] {c : 𝕜} (hc : c 0) :
f =Θ[l] g' (f =Θ[l] λ (x : α), c g' x)

Alias of the reverse direction of asymptotics.is_Theta_const_smul_right.

theorem asymptotics.is_Theta.of_const_smul_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} {𝕜 : Type u_14} [has_norm E] [normed_field 𝕜] {f : α E} {g' : α F'} {l : filter α} [ F'] {c : 𝕜} (hc : c 0) :
(f =Θ[l] λ (x : α), c g' x) f =Θ[l] g'

Alias of the forward direction of asymptotics.is_Theta_const_smul_right.

theorem asymptotics.is_Theta_const_mul_left {α : Type u_1} {F : Type u_4} {𝕜 : Type u_14} [has_norm F] [normed_field 𝕜] {g : α F} {l : filter α} {c : 𝕜} {f : α 𝕜} (hc : c 0) :
(λ (x : α), c * f x) =Θ[l] g f =Θ[l] g
theorem asymptotics.is_Theta.const_mul_left {α : Type u_1} {F : Type u_4} {𝕜 : Type u_14} [has_norm F] [normed_field 𝕜] {g : α F} {l : filter α} {c : 𝕜} {f : α 𝕜} (hc : c 0) :
f =Θ[l] g (λ (x : α), c * f x) =Θ[l] g

Alias of the reverse direction of asymptotics.is_Theta_const_mul_left.

theorem asymptotics.is_Theta.of_const_mul_left {α : Type u_1} {F : Type u_4} {𝕜 : Type u_14} [has_norm F] [normed_field 𝕜] {g : α F} {l : filter α} {c : 𝕜} {f : α 𝕜} (hc : c 0) :
(λ (x : α), c * f x) =Θ[l] g f =Θ[l] g

Alias of the forward direction of asymptotics.is_Theta_const_mul_left.

theorem asymptotics.is_Theta_const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_14} [has_norm E] [normed_field 𝕜] {f : α E} {l : filter α} {c : 𝕜} {g : α 𝕜} (hc : c 0) :
(f =Θ[l] λ (x : α), c * g x) f =Θ[l] g
theorem asymptotics.is_Theta.const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_14} [has_norm E] [normed_field 𝕜] {f : α E} {l : filter α} {c : 𝕜} {g : α 𝕜} (hc : c 0) :
f =Θ[l] g (f =Θ[l] λ (x : α), c * g x)

Alias of the reverse direction of asymptotics.is_Theta_const_mul_right.

theorem asymptotics.is_Theta.of_const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_14} [has_norm E] [normed_field 𝕜] {f : α E} {l : filter α} {c : 𝕜} {g : α 𝕜} (hc : c 0) :
(f =Θ[l] λ (x : α), c * g x) f =Θ[l] g

Alias of the forward direction of asymptotics.is_Theta_const_mul_right.