Asymptotic equivalence up to a constant #
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.
theorem
asymptotics.is_Theta.of_norm_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{g : α → F}
{f' : α → E'}
{l : filter α} :
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]
[seminormed_add_comm_group E']
{g : α → F}
{f' : α → E'}
{l : filter α} :
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]
[seminormed_add_comm_group F']
{f : α → E}
{g' : α → F'}
{l : filter α} :
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]
[seminormed_add_comm_group F']
{f : α → E}
{g' : α → F'}
{l : filter α} :
Alias of the reverse direction of asymptotics.is_Theta_norm_right.
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]
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{k : α → G}
{f' : α → E'}
{g' : α → F'}
{l : filter α}
(h : f' =Θ[l] g') :
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]
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{f : α → E}
{g' : α → F'}
{k' : α → G'}
{l : filter α}
(h : g' =Θ[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]
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{k : α → G}
{f' : α → E'}
{g' : α → F'}
{l : filter α}
(h : f' =Θ[l] g') :
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]
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{f : α → E}
{g' : α → F'}
{k' : α → G'}
{l : filter α}
(h : g' =Θ[l] k') :
theorem
asymptotics.is_Theta.sup
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{f' : α → E'}
{g' : α → F'}
{l l' : filter α}
(h : f' =Θ[l] g')
(h' : f' =Θ[l'] g') :
@[simp]
theorem
asymptotics.is_Theta_sup
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{f' : α → E'}
{g' : α → F'}
{l l' : filter α} :
theorem
asymptotics.is_Theta.eq_zero_iff
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
{f'' : α → E''}
{g'' : α → F''}
{l : filter α}
(h : f'' =Θ[l] g'') :
theorem
asymptotics.is_Theta.tendsto_zero_iff
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
{f'' : α → E''}
{g'' : α → F''}
{l : filter α}
(h : f'' =Θ[l] g'') :
filter.tendsto f'' l (nhds 0) ↔ filter.tendsto g'' l (nhds 0)
theorem
asymptotics.is_Theta.tendsto_norm_at_top_iff
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α}
(h : f' =Θ[l] g') :
filter.tendsto (has_norm.norm ∘ f') l filter.at_top ↔ filter.tendsto (has_norm.norm ∘ g') l filter.at_top
theorem
asymptotics.is_Theta.is_bounded_under_le_iff
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{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}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[normed_field 𝕜]
[normed_field 𝕜']
{l : filter α}
[normed_space 𝕜 E']
[normed_space 𝕜' F']
{f₁ : α → 𝕜}
{f₂ : α → 𝕜'}
{g₁ : α → E'}
{g₂ : α → F'}
(hf : f₁ =Θ[l] f₂)
(hg : g₁ =Θ[l] g₂) :
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₂) :
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) :
@[simp]
theorem
asymptotics.is_Theta_inv
{α : Type u_1}
{𝕜 : Type u_14}
{𝕜' : Type u_15}
[normed_field 𝕜]
[normed_field 𝕜']
{l : filter α}
{f : α → 𝕜}
{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₂) :
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 : ℕ) :
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 : ℤ) :
theorem
asymptotics.is_Theta_const_const
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
{l : filter α}
{c₁ : E''}
{c₂ : F''}
(h₁ : c₁ ≠ 0)
(h₂ : c₂ ≠ 0) :
@[simp]
theorem
asymptotics.is_Theta_const_const_iff
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
{l : filter α}
[l.ne_bot]
{c₁ : E''}
{c₂ : F''} :
@[simp]
theorem
asymptotics.is_Theta_zero_left
{α : Type u_1}
{E' : Type u_6}
{F'' : Type u_10}
[seminormed_add_comm_group E']
[normed_add_comm_group F'']
{g'' : α → F''}
{l : filter α} :
@[simp]
theorem
asymptotics.is_Theta_zero_right
{α : Type u_1}
{F' : Type u_7}
{E'' : Type u_9}
[seminormed_add_comm_group F']
[normed_add_comm_group E'']
{f'' : α → E''}
{l : filter α} :
theorem
asymptotics.is_Theta_const_smul_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
{𝕜 : Type u_14}
[has_norm F]
[seminormed_add_comm_group E']
[normed_field 𝕜]
{g : α → F}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
{c : 𝕜}
(hc : c ≠ 0) :
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]
[seminormed_add_comm_group E']
[normed_field 𝕜]
{g : α → F}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
{c : 𝕜}
(hc : c ≠ 0) :
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]
[seminormed_add_comm_group E']
[normed_field 𝕜]
{g : α → F}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
{c : 𝕜}
(hc : c ≠ 0) :
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]
[seminormed_add_comm_group F']
[normed_field 𝕜]
{f : α → E}
{g' : α → F'}
{l : filter α}
[normed_space 𝕜 F']
{c : 𝕜}
(hc : c ≠ 0) :
theorem
asymptotics.is_Theta.const_smul_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
{𝕜 : Type u_14}
[has_norm E]
[seminormed_add_comm_group F']
[normed_field 𝕜]
{f : α → E}
{g' : α → F'}
{l : filter α}
[normed_space 𝕜 F']
{c : 𝕜}
(hc : c ≠ 0) :
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]
[seminormed_add_comm_group F']
[normed_field 𝕜]
{f : α → E}
{g' : α → F'}
{l : filter α}
[normed_space 𝕜 F']
{c : 𝕜}
(hc : c ≠ 0) :
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) :
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) :
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) :
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) :
Alias of the forward direction of asymptotics.is_Theta_const_mul_right.