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.
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_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.