Ring and field operations on asymptotic relations #
This file develops the behavior of IsBigOWith, IsBigO, and IsLittleO under
multiplication by constants, multiplication of functions, powers, inversion, and division.
Multiplication by a constant #
theorem
Asymptotics.isBigOWith_const_mul_self
{α : Type u_1}
{R : Type u_4}
[SeminormedRing R]
(c : R)
(f : α → R)
(l : Filter α)
:
IsBigOWith ‖c‖ l (fun (x : α) => c * f x) f
theorem
Asymptotics.isBigO_const_mul_self
{α : Type u_1}
{R : Type u_4}
[SeminormedRing R]
(c : R)
(f : α → R)
(l : Filter α)
:
theorem
Asymptotics.IsBigOWith.const_mul_left
{α : Type u_1}
{F : Type u_3}
{R : Type u_4}
[Norm F]
[SeminormedRing R]
{c : ℝ}
{g : α → F}
{l : Filter α}
{f : α → R}
(h : IsBigOWith c l f g)
(c' : R)
:
IsBigOWith (‖c'‖ * c) l (fun (x : α) => c' * f x) g
theorem
Asymptotics.isBigOWith_self_const_mul'
{α : Type u_1}
{R : Type u_4}
[SeminormedRing R]
(u : Rˣ)
(f : α → R)
(l : Filter α)
:
IsBigOWith ‖↑u⁻¹‖ l f fun (x : α) => ↑u * f x
theorem
Asymptotics.isBigOWith_self_const_mul
{α : Type u_1}
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{c : S}
(hc : c ≠ 0)
(f : α → S)
(l : Filter α)
:
IsBigOWith ‖c‖⁻¹ l f fun (x : α) => c * f x
theorem
Asymptotics.isBigO_self_const_mul'
{α : Type u_1}
{R : Type u_4}
[SeminormedRing R]
{c : R}
(hc : IsUnit c)
(f : α → R)
(l : Filter α)
:
theorem
Asymptotics.isBigO_self_const_mul
{α : Type u_1}
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{c : S}
(hc : c ≠ 0)
(f : α → S)
(l : Filter α)
:
theorem
Asymptotics.IsBigOWith.of_const_mul_right
{α : Type u_1}
{E : Type u_2}
{R : Type u_4}
[Norm E]
[SeminormedRing R]
{c' : ℝ}
{f : α → E}
{l : Filter α}
{g : α → R}
{c : R}
(hc' : 0 ≤ c')
(h : IsBigOWith c' l f fun (x : α) => c * g x)
:
IsBigOWith (c' * ‖c‖) l f g
theorem
Asymptotics.IsBigOWith.const_mul_right'
{α : Type u_1}
{E : Type u_2}
{R : Type u_4}
[Norm E]
[SeminormedRing R]
{f : α → E}
{l : Filter α}
{g : α → R}
{u : Rˣ}
{c' : ℝ}
(hc' : 0 ≤ c')
(h : IsBigOWith c' l f g)
:
theorem
Asymptotics.IsBigOWith.const_mul_right
{α : Type u_1}
{E : Type u_2}
[Norm E]
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{f : α → E}
{l : Filter α}
{g : α → S}
{c : S}
(hc : c ≠ 0)
{c' : ℝ}
(hc' : 0 ≤ c')
(h : IsBigOWith c' l f g)
:
theorem
Asymptotics.IsBigO.const_mul_right
{α : Type u_1}
{E : Type u_2}
[Norm E]
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{f : α → E}
{l : Filter α}
{g : α → S}
{c : S}
(hc : c ≠ 0)
(h : f =O[l] g)
:
theorem
Asymptotics.IsLittleO.const_mul_right
{α : Type u_1}
{E : Type u_2}
[Norm E]
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{f : α → E}
{l : Filter α}
{g : α → S}
{c : S}
(hc : c ≠ 0)
(h : f =o[l] g)
:
Multiplication #
theorem
Asymptotics.IsBigOWith.mul
{α : Type u_1}
{R : Type u_4}
[SeminormedRing R]
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{l : Filter α}
{f₁ f₂ : α → R}
{g₁ g₂ : α → S}
{c₁ c₂ : ℝ}
(h₁ : IsBigOWith c₁ l f₁ g₁)
(h₂ : IsBigOWith c₂ l f₂ g₂)
:
IsBigOWith (c₁ * c₂) l (fun (x : α) => f₁ x * f₂ x) fun (x : α) => g₁ x * g₂ x
theorem
Asymptotics.IsBigO.mul
{α : Type u_1}
{R : Type u_4}
[SeminormedRing R]
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{l : Filter α}
{f₁ f₂ : α → R}
{g₁ g₂ : α → S}
(h₁ : f₁ =O[l] g₁)
(h₂ : f₂ =O[l] g₂)
:
theorem
Asymptotics.IsBigO.mul_isLittleO
{α : Type u_1}
{R : Type u_4}
[SeminormedRing R]
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{l : Filter α}
{f₁ f₂ : α → R}
{g₁ g₂ : α → S}
(h₁ : f₁ =O[l] g₁)
(h₂ : f₂ =o[l] g₂)
:
theorem
Asymptotics.IsLittleO.mul_isBigO
{α : Type u_1}
{R : Type u_4}
[SeminormedRing R]
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{l : Filter α}
{f₁ f₂ : α → R}
{g₁ g₂ : α → S}
(h₁ : f₁ =o[l] g₁)
(h₂ : f₂ =O[l] g₂)
:
theorem
Asymptotics.IsLittleO.mul
{α : Type u_1}
{R : Type u_4}
[SeminormedRing R]
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{l : Filter α}
{f₁ f₂ : α → R}
{g₁ g₂ : α → S}
(h₁ : f₁ =o[l] g₁)
(h₂ : f₂ =o[l] g₂)
:
theorem
Asymptotics.IsBigOWith.pow'
{α : Type u_1}
{R : Type u_4}
[SeminormedRing R]
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{c : ℝ}
{l : Filter α}
[NormOneClass S]
{f : α → R}
{g : α → S}
(h : IsBigOWith c l f g)
(n : ℕ)
:
IsBigOWith (Nat.casesOn n ‖1‖ fun (n : ℕ) => c ^ (n + 1)) l (fun (x : α) => f x ^ n) fun (x : α) => g x ^ n
theorem
Asymptotics.IsBigOWith.pow
{α : Type u_1}
{R : Type u_4}
[SeminormedRing R]
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{c : ℝ}
{l : Filter α}
[NormOneClass R]
[NormOneClass S]
{f : α → R}
{g : α → S}
(h : IsBigOWith c l f g)
(n : ℕ)
:
IsBigOWith (c ^ n) l (fun (x : α) => f x ^ n) fun (x : α) => g x ^ n
theorem
Asymptotics.IsBigOWith.of_pow
{α : Type u_1}
{R : Type u_4}
[SeminormedRing R]
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{c c' : ℝ}
{l : Filter α}
[NormOneClass S]
{n : ℕ}
{f : α → S}
{g : α → R}
(h : IsBigOWith c l (f ^ n) (g ^ n))
(hn : n ≠ 0)
(hc : c ≤ c' ^ n)
(hc' : 0 ≤ c')
:
IsBigOWith c' l f g
theorem
Asymptotics.IsBigO.pow
{α : Type u_1}
{R : Type u_4}
[SeminormedRing R]
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{l : Filter α}
[NormOneClass S]
{f : α → R}
{g : α → S}
(h : f =O[l] g)
(n : ℕ)
:
theorem
Asymptotics.IsLittleO.pow
{α : Type u_1}
{R : Type u_4}
[SeminormedRing R]
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{l : Filter α}
{f : α → R}
{g : α → S}
(h : f =o[l] g)
{n : ℕ}
(hn : 0 < n)
:
theorem
Asymptotics.IsLittleO.of_pow
{α : Type u_1}
{R : Type u_4}
[SeminormedRing R]
{S : Type u_7}
[NormedRing S]
[NormMulClass S]
{l : Filter α}
[NormOneClass S]
{f : α → S}
{g : α → R}
{n : ℕ}
(h : (f ^ n) =o[l] (g ^ n))
(hn : n ≠ 0)
:
Inverse #
theorem
Asymptotics.IsBigOWith.inv_rev
{α : Type u_1}
{𝕜 : Type u_5}
{𝕜' : Type u_6}
[NormedDivisionRing 𝕜]
[NormedDivisionRing 𝕜']
{c : ℝ}
{l : Filter α}
{f : α → 𝕜}
{g : α → 𝕜'}
(h : IsBigOWith c l f g)
(h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0)
:
IsBigOWith c l (fun (x : α) => (g x)⁻¹) fun (x : α) => (f x)⁻¹
Eventually (u / v) * v = u #
If u and v are linked by an IsBigOWith relation, then we
eventually have (u / v) * v = u, even if v vanishes.
theorem
Asymptotics.IsBigOWith.eventually_mul_div_cancel
{α : Type u_1}
{𝕜 : Type u_5}
[NormedDivisionRing 𝕜]
{c : ℝ}
{l : Filter α}
{u v : α → 𝕜}
(h : IsBigOWith c l u v)
: