Asymptotic equivalence up to a constant #
In this file we prove basic properties of the equivalence relation
given by f =Θ[l] g ↔ f =O[l] g ∧ g =O[l] f.
instance
Asymptotics.instTransForallIsLittleOIsTheta
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
{G' : Type u_8}
[Norm E]
[SeminormedAddCommGroup F']
[SeminormedAddCommGroup G']
{l : Filter α}
:
Equations
- Asymptotics.instTransForallIsLittleOIsTheta = { trans := ⋯ }
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 α}
:
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 α}
:
Alias of the reverse direction of Asymptotics.isTheta_norm_left.
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 α}
:
Alias of the reverse direction of Asymptotics.isTheta_norm_right.
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 α}
:
Alias of the forward direction of Asymptotics.isTheta_norm_right.
theorem
Asymptotics.IsTheta.sup
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{f' : α → E'}
{g' : α → F'}
{l l' : Filter α}
(h : f' =Θ[l] g')
(h' : f' =Θ[l'] g')
:
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')
:
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')
:
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₂)
:
theorem
Asymptotics.IsTheta.listProd
{α : Type u_1}
{𝕜 : Type u_14}
{𝕜' : Type u_15}
[NormedField 𝕜]
[NormedField 𝕜']
{l : Filter α}
{ι : Type u_16}
{L : List ι}
{f : ι → α → 𝕜}
{g : ι → α → 𝕜'}
(h : ∀ i ∈ L, f i =Θ[l] g i)
:
theorem
Asymptotics.IsTheta.multisetProd
{α : Type u_1}
{𝕜 : Type u_14}
{𝕜' : Type u_15}
[NormedField 𝕜]
[NormedField 𝕜']
{l : Filter α}
{ι : Type u_16}
{s : Multiset ι}
{f : ι → α → 𝕜}
{g : ι → α → 𝕜'}
(h : ∀ i ∈ s, f i =Θ[l] g i)
:
(fun (x : α) => (Multiset.map (fun (x_1 : ι) => f x_1 x) s).prod) =Θ[l] fun (x : α) =>
(Multiset.map (fun (x_1 : ι) => g x_1 x) s).prod
theorem
Asymptotics.IsTheta.finsetProd
{α : Type u_1}
{𝕜 : Type u_14}
{𝕜' : Type u_15}
[NormedField 𝕜]
[NormedField 𝕜']
{l : Filter α}
{ι : Type u_16}
{s : Finset ι}
{f : ι → α → 𝕜}
{g : ι → α → 𝕜'}
(h : ∀ i ∈ s, f i =Θ[l] g i)
:
theorem
Asymptotics.IsTheta.inv
{α : Type u_1}
{𝕜 : Type u_14}
{𝕜' : Type u_15}
[NormedField 𝕜]
[NormedField 𝕜']
{l : Filter α}
{f : α → 𝕜}
{g : α → 𝕜'}
(h : f =Θ[l] g)
:
@[simp]
theorem
Asymptotics.isTheta_inv
{α : Type u_1}
{𝕜 : Type u_14}
{𝕜' : Type u_15}
[NormedField 𝕜]
[NormedField 𝕜']
{l : Filter α}
{f : α → 𝕜}
{g : α → 𝕜'}
:
theorem
Asymptotics.IsTheta.pow
{α : Type u_1}
{𝕜 : Type u_14}
{𝕜' : Type u_15}
[NormedField 𝕜]
[NormedField 𝕜']
{l : Filter α}
{f : α → 𝕜}
{g : α → 𝕜'}
(h : f =Θ[l] g)
(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 : ℤ)
:
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)
:
@[simp]
theorem
Asymptotics.isTheta_const_const_iff
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{l : Filter α}
[l.NeBot]
{c₁ : E''}
{c₂ : F''}
:
@[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 α}
:
@[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 α}
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
Alias of the reverse direction of Asymptotics.isTheta_const_mul_left.
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)
:
Alias of the forward direction of Asymptotics.isTheta_const_mul_left.
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)
:
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)
:
Alias of the reverse direction of Asymptotics.isTheta_const_mul_right.
theorem
Asymptotics.isTheta_of_div_tendsto_nhds_ne_zero
{α : Type u_1}
{𝕜 : Type u_14}
[NormedField 𝕜]
{l : Filter α}
{c : 𝕜}
{f g : α → 𝕜}
(h : Filter.Tendsto (fun (x : α) => g x / f x) l (nhds c))
(hc : c ≠ 0)
:
theorem
ContinuousOn.isTheta_principal
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddGroup E]
[SeminormedAddGroup F]
[TopologicalSpace α]
{s : Set α}
{f : α → E}
{c : F}
(hf : ContinuousOn f s)
(hs : IsCompact s)
(hc : ‖c‖ ≠ 0)
(hC : ∀ i ∈ s, f i ≠ 0)
: