Further basic lemmas about asymptotics #
@[simp]
theorem
Asymptotics.isLittleO_principal
{α : Type u_1}
{F' : Type u_7}
{E'' : Type u_9}
[SeminormedAddCommGroup F']
[NormedAddCommGroup E'']
{g' : α → F'}
{f'' : α → E''}
{s : Set α}
:
@[simp]
theorem
Asymptotics.isLittleO_top
{α : Type u_1}
{F' : Type u_7}
{E'' : Type u_9}
[SeminormedAddCommGroup F']
[NormedAddCommGroup E'']
{g' : α → F'}
{f'' : α → E''}
:
theorem
Asymptotics.isBigOWith_const_one
{α : Type u_1}
{E : Type u_3}
(F : Type u_4)
[Norm E]
[Norm F]
[One F]
[NormOneClass F]
(c : E)
(l : Filter α)
:
IsBigOWith ‖c‖ l (fun (_x : α) => c) fun (_x : α) => 1
@[simp]
theorem
Asymptotics.isLittleO_one_iff
{α : Type u_1}
(F : Type u_4)
{E''' : Type u_12}
[Norm F]
[SeminormedAddGroup E''']
{l : Filter α}
[One F]
[NormOneClass F]
{f : α → E'''}
:
theorem
Filter.IsBoundedUnder.isBigO_one
{α : Type u_1}
{E : Type u_3}
(F : Type u_4)
[Norm E]
[Norm F]
{f : α → E}
{l : Filter α}
[One F]
[NormOneClass F]
:
Alias of the reverse direction of Asymptotics.isBigO_one_iff.
@[simp]
theorem
Asymptotics.isLittleO_one_left_iff
{α : Type u_1}
{E : Type u_3}
(F : Type u_4)
[Norm E]
[Norm F]
{f : α → E}
{l : Filter α}
[One F]
[NormOneClass F]
:
theorem
Filter.Tendsto.isBigO_one
{α : Type u_1}
(F : Type u_4)
{E' : Type u_6}
[Norm F]
[SeminormedAddCommGroup E']
{f' : α → E'}
{l : Filter α}
[One F]
[NormOneClass F]
{c : E'}
(h : Tendsto f' l (nhds c))
:
theorem
Asymptotics.IsBigO.trans_tendsto_nhds
{α : Type u_1}
{E : Type u_3}
(F : Type u_4)
{F' : Type u_7}
[Norm E]
[Norm F]
[SeminormedAddCommGroup F']
{f : α → E}
{g' : α → F'}
{l : Filter α}
[One F]
[NormOneClass F]
(hfg : f =O[l] g')
{y : F'}
(hg : Filter.Tendsto g' l (nhds y))
:
theorem
Asymptotics.isBigO_one_nhds_ne_iff
{α : Type u_1}
{E : Type u_3}
(F : Type u_4)
[Norm E]
[Norm F]
{f : α → E}
[One F]
[NormOneClass F]
[TopologicalSpace α]
{a : α}
:
The condition f = O[𝓝[≠] a] 1 is equivalent to f = O[𝓝 a] 1.
theorem
Asymptotics.isLittleO_const_iff
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{f'' : α → E''}
{l : Filter α}
{c : F''}
(hc : c ≠ 0)
:
theorem
Asymptotics.isLittleO_id_const
{E'' : Type u_9}
{F'' : Type u_10}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{c : F''}
(hc : c ≠ 0)
:
theorem
Asymptotics.isBigO_const_of_tendsto
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{f'' : α → E''}
{l : Filter α}
{y : E''}
(h : Filter.Tendsto f'' l (nhds y))
{c : F''}
(hc : c ≠ 0)
:
theorem
Asymptotics.isBigO_const_iff
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{f'' : α → E''}
{l : Filter α}
{c : F''}
:
theorem
Asymptotics.isBigO_const_left_iff_pos_le_norm
{α : Type u_1}
{E' : Type u_6}
{E'' : Type u_9}
[SeminormedAddCommGroup E']
[NormedAddCommGroup E'']
{f' : α → E'}
{l : Filter α}
{c : E''}
(hc : c ≠ 0)
:
(fun x ↦ c) =O[l] f if and only if f is bounded away from zero.
theorem
Asymptotics.IsBigO.trans_tendsto
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{f'' : α → E''}
{g'' : α → F''}
{l : Filter α}
(hfg : f'' =O[l] g'')
(hg : Filter.Tendsto g'' l (nhds 0))
:
Filter.Tendsto f'' l (nhds 0)
theorem
Asymptotics.IsLittleO.trans_tendsto
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{f'' : α → E''}
{g'' : α → F''}
{l : Filter α}
(hfg : f'' =o[l] g'')
(hg : Filter.Tendsto g'' l (nhds 0))
:
Filter.Tendsto f'' l (nhds 0)
theorem
Asymptotics.isLittleO_id_one
{E'' : Type u_9}
{F'' : Type u_10}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
[One F'']
[NeZero 1]
:
theorem
Asymptotics.continuousAt_iff_isLittleO
{α : Type u_17}
{E : Type u_18}
[NormedRing E]
[NormOneClass E]
[TopologicalSpace α]
{f : α → E}
{x : α}
:
Multiplication #
Scalar multiplication #
theorem
Asymptotics.IsBigOWith.const_smul_self
{α : Type u_1}
{E' : Type u_6}
{R : Type u_13}
[SeminormedAddCommGroup E']
[SeminormedRing R]
{f' : α → E'}
{l : Filter α}
[Module R E']
[IsBoundedSMul R E']
(c' : R)
:
IsBigOWith ‖c'‖ l (fun (x : α) => c' • f' x) f'
theorem
Asymptotics.IsBigO.const_smul_self
{α : Type u_1}
{E' : Type u_6}
{R : Type u_13}
[SeminormedAddCommGroup E']
[SeminormedRing R]
{f' : α → E'}
{l : Filter α}
[Module R E']
[IsBoundedSMul R E']
(c' : R)
:
theorem
Asymptotics.IsBigOWith.const_smul_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
{R : Type u_13}
[Norm F]
[SeminormedAddCommGroup E']
[SeminormedRing R]
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : Filter α}
[Module R E']
[IsBoundedSMul R E']
(h : IsBigOWith c l f' g)
(c' : R)
:
IsBigOWith (‖c'‖ * c) l (fun (x : α) => c' • f' x) g
theorem
Asymptotics.IsBigO.const_smul_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
{R : Type u_13}
[Norm F]
[SeminormedAddCommGroup E']
[SeminormedRing R]
{g : α → F}
{f' : α → E'}
{l : Filter α}
[Module R E']
[IsBoundedSMul R E']
(h : f' =O[l] g)
(c : R)
:
theorem
Asymptotics.IsLittleO.const_smul_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
{R : Type u_13}
[Norm F]
[SeminormedAddCommGroup E']
[SeminormedRing R]
{g : α → F}
{f' : α → E'}
{l : Filter α}
[Module R E']
[IsBoundedSMul R E']
(h : f' =o[l] g)
(c : R)
:
theorem
Asymptotics.isBigO_const_smul_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
{𝕜 : Type u_15}
[Norm F]
[SeminormedAddCommGroup E']
[NormedDivisionRing 𝕜]
{g : α → F}
{f' : α → E'}
{l : Filter α}
[Module 𝕜 E']
[NormSMulClass 𝕜 E']
{c : 𝕜}
(hc : c ≠ 0)
:
theorem
Asymptotics.isLittleO_const_smul_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
{𝕜 : Type u_15}
[Norm F]
[SeminormedAddCommGroup E']
[NormedDivisionRing 𝕜]
{g : α → F}
{f' : α → E'}
{l : Filter α}
[Module 𝕜 E']
[NormSMulClass 𝕜 E']
{c : 𝕜}
(hc : c ≠ 0)
:
theorem
Asymptotics.isBigO_const_smul_right
{α : Type u_1}
{E : Type u_3}
{E' : Type u_6}
{𝕜 : Type u_15}
[Norm E]
[SeminormedAddCommGroup E']
[NormedDivisionRing 𝕜]
{f : α → E}
{f' : α → E'}
{l : Filter α}
[Module 𝕜 E']
[NormSMulClass 𝕜 E']
{c : 𝕜}
(hc : c ≠ 0)
:
theorem
Asymptotics.isLittleO_const_smul_right
{α : Type u_1}
{E : Type u_3}
{E' : Type u_6}
{𝕜 : Type u_15}
[Norm E]
[SeminormedAddCommGroup E']
[NormedDivisionRing 𝕜]
{f : α → E}
{f' : α → E'}
{l : Filter α}
[Module 𝕜 E']
[NormSMulClass 𝕜 E']
{c : 𝕜}
(hc : c ≠ 0)
:
theorem
Asymptotics.IsBigOWith.smul
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{R : Type u_13}
{𝕜' : Type u_16}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
[SeminormedRing R]
[NormedDivisionRing 𝕜']
{c c' : ℝ}
{f' : α → E'}
{g' : α → F'}
{l : Filter α}
[Module R E']
[IsBoundedSMul R E']
[Module 𝕜' F']
[NormSMulClass 𝕜' F']
{k₁ : α → R}
{k₂ : α → 𝕜'}
(h₁ : IsBigOWith c l k₁ k₂)
(h₂ : IsBigOWith c' l f' g')
:
IsBigOWith (c * c') l (fun (x : α) => k₁ x • f' x) fun (x : α) => k₂ x • g' x
theorem
Asymptotics.IsBigO.smul
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{R : Type u_13}
{𝕜' : Type u_16}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
[SeminormedRing R]
[NormedDivisionRing 𝕜']
{f' : α → E'}
{g' : α → F'}
{l : Filter α}
[Module R E']
[IsBoundedSMul R E']
[Module 𝕜' F']
[NormSMulClass 𝕜' F']
{k₁ : α → R}
{k₂ : α → 𝕜'}
(h₁ : k₁ =O[l] k₂)
(h₂ : f' =O[l] g')
:
theorem
Asymptotics.IsBigO.smul_isLittleO
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{R : Type u_13}
{𝕜' : Type u_16}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
[SeminormedRing R]
[NormedDivisionRing 𝕜']
{f' : α → E'}
{g' : α → F'}
{l : Filter α}
[Module R E']
[IsBoundedSMul R E']
[Module 𝕜' F']
[NormSMulClass 𝕜' F']
{k₁ : α → R}
{k₂ : α → 𝕜'}
(h₁ : k₁ =O[l] k₂)
(h₂ : f' =o[l] g')
:
theorem
Asymptotics.IsLittleO.smul_isBigO
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{R : Type u_13}
{𝕜' : Type u_16}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
[SeminormedRing R]
[NormedDivisionRing 𝕜']
{f' : α → E'}
{g' : α → F'}
{l : Filter α}
[Module R E']
[IsBoundedSMul R E']
[Module 𝕜' F']
[NormSMulClass 𝕜' F']
{k₁ : α → R}
{k₂ : α → 𝕜'}
(h₁ : k₁ =o[l] k₂)
(h₂ : f' =O[l] g')
:
theorem
Asymptotics.IsLittleO.smul
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{R : Type u_13}
{𝕜' : Type u_16}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
[SeminormedRing R]
[NormedDivisionRing 𝕜']
{f' : α → E'}
{g' : α → F'}
{l : Filter α}
[Module R E']
[IsBoundedSMul R E']
[Module 𝕜' F']
[NormSMulClass 𝕜' F']
{k₁ : α → R}
{k₂ : α → 𝕜'}
(h₁ : k₁ =o[l] k₂)
(h₂ : f' =o[l] g')
:
theorem
Asymptotics.IsBigO.listProd
{α : Type u_1}
{R : Type u_13}
{𝕜 : Type u_15}
[SeminormedRing R]
[NormedDivisionRing 𝕜]
{l : Filter α}
{ι : Type u_17}
{L : List ι}
{f : ι → α → R}
{g : ι → α → 𝕜}
(hf : ∀ i ∈ L, f i =O[l] g i)
:
theorem
Asymptotics.IsBigO.multisetProd
{α : Type u_1}
{l : Filter α}
{ι : Type u_17}
{R : Type u_18}
{𝕜 : Type u_19}
[SeminormedCommRing R]
[NormedField 𝕜]
{s : Multiset ι}
{f : ι → α → R}
{g : ι → α → 𝕜}
(hf : ∀ i ∈ s, f i =O[l] g i)
:
(fun (x : α) => (Multiset.map (fun (x_1 : ι) => f x_1 x) s).prod) =O[l] fun (x : α) =>
(Multiset.map (fun (x_1 : ι) => g x_1 x) s).prod
theorem
Asymptotics.IsBigO.finsetProd
{α : Type u_1}
{l : Filter α}
{ι : Type u_17}
{R : Type u_18}
{𝕜 : Type u_19}
[SeminormedCommRing R]
[NormedField 𝕜]
{s : Finset ι}
{f : ι → α → R}
{g : ι → α → 𝕜}
(hf : ∀ i ∈ s, f i =O[l] g i)
:
theorem
Asymptotics.IsLittleO.listProd
{α : Type u_1}
{R : Type u_13}
{𝕜 : Type u_15}
[SeminormedRing R]
[NormedDivisionRing 𝕜]
{l : Filter α}
{ι : Type u_17}
{L : List ι}
{f : ι → α → R}
{g : ι → α → 𝕜}
(h₁ : ∀ i ∈ L, f i =O[l] g i)
(h₂ : ∃ i ∈ L, f i =o[l] g i)
:
theorem
Asymptotics.IsLittleO.multisetProd
{α : Type u_1}
{l : Filter α}
{ι : Type u_17}
{R : Type u_18}
{𝕜 : Type u_19}
[SeminormedCommRing R]
[NormedField 𝕜]
{s : Multiset ι}
{f : ι → α → R}
{g : ι → α → 𝕜}
(h₁ : ∀ i ∈ s, f i =O[l] g i)
(h₂ : ∃ i ∈ s, f i =o[l] g i)
:
(fun (x : α) => (Multiset.map (fun (x_1 : ι) => f x_1 x) s).prod) =o[l] fun (x : α) =>
(Multiset.map (fun (x_1 : ι) => g x_1 x) s).prod
theorem
Asymptotics.IsLittleO.finsetProd
{α : Type u_1}
{l : Filter α}
{ι : Type u_17}
{R : Type u_18}
{𝕜 : Type u_19}
[SeminormedCommRing R]
[NormedField 𝕜]
{s : Finset ι}
{f : ι → α → R}
{g : ι → α → 𝕜}
(h₁ : ∀ i ∈ s, f i =O[l] g i)
(h₂ : ∃ i ∈ s, f i =o[l] g i)
:
Relation between f = o(g) and f / g → 0 #
theorem
Asymptotics.IsLittleO.tendsto_div_nhds_zero
{α : Type u_1}
{𝕜 : Type u_15}
[NormedDivisionRing 𝕜]
{l : Filter α}
{f g : α → 𝕜}
(h : f =o[l] g)
:
Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0)
theorem
Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero
{α : Type u_1}
{E' : Type u_6}
{𝕜 : Type u_15}
[SeminormedAddCommGroup E']
[NormedDivisionRing 𝕜]
[Module 𝕜 E']
[NormSMulClass 𝕜 E']
{f : α → E'}
{g : α → 𝕜}
{l : Filter α}
(h : f =o[l] g)
:
Filter.Tendsto (fun (x : α) => (g x)⁻¹ • f x) l (nhds 0)
theorem
Asymptotics.isLittleO_iff_tendsto
{α : Type u_1}
{𝕜 : Type u_15}
[NormedDivisionRing 𝕜]
{l : Filter α}
{f g : α → 𝕜}
(hgf : ∀ (x : α), g x = 0 → f x = 0)
:
theorem
Asymptotics.isLittleO_of_tendsto'
{α : Type u_1}
{𝕜 : Type u_15}
[NormedDivisionRing 𝕜]
{l : Filter α}
{f g : α → 𝕜}
(hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0)
:
Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0) → f =o[l] g
Alias of the reverse direction of Asymptotics.isLittleO_iff_tendsto'.
theorem
Asymptotics.isLittleO_of_tendsto
{α : Type u_1}
{𝕜 : Type u_15}
[NormedDivisionRing 𝕜]
{l : Filter α}
{f g : α → 𝕜}
(hgf : ∀ (x : α), g x = 0 → f x = 0)
:
Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0) → f =o[l] g
Alias of the reverse direction of Asymptotics.isLittleO_iff_tendsto.
theorem
Asymptotics.isLittleO_const_left_of_ne
{α : Type u_1}
{F : Type u_4}
{E'' : Type u_9}
[Norm F]
[NormedAddCommGroup E'']
{g : α → F}
{l : Filter α}
{c : E''}
(hc : c ≠ 0)
:
@[simp]
theorem
Asymptotics.isLittleO_const_left
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{g'' : α → F''}
{l : Filter α}
{c : E''}
:
@[simp]
theorem
Asymptotics.isLittleO_const_const_iff
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{l : Filter α}
[l.NeBot]
{d : E''}
{c : F''}
:
@[simp]
theorem
Asymptotics.isLittleO_pure
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{f'' : α → E''}
{g'' : α → F''}
{x : α}
:
theorem
Asymptotics.isLittleO_const_id_cobounded
{E'' : Type u_9}
{F'' : Type u_10}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
(c : F'')
:
Equivalent definitions of the form ∃ φ, u =ᶠ[l] φ * v in a NormedField. #
theorem
Asymptotics.isBigOWith_of_eq_mul
{α : Type u_1}
{R : Type u_13}
[SeminormedRing R]
{c : ℝ}
{l : Filter α}
{u v : α → R}
(φ : α → R)
(hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c)
(h : u =ᶠ[l] φ * v)
:
IsBigOWith c l u v
If ‖φ‖ is eventually bounded by c, and u =ᶠ[l] φ * v, then we have IsBigOWith c u v l.
This does not require any assumptions on c, which is why we keep this version along with
IsBigOWith_iff_exists_eq_mul.
theorem
Asymptotics.IsBigO.exists_eq_mul
{α : Type u_1}
{𝕜 : Type u_15}
[NormedDivisionRing 𝕜]
{l : Filter α}
{u v : α → 𝕜}
:
Alias of the forward direction of Asymptotics.isBigO_iff_exists_eq_mul.
theorem
Asymptotics.isLittleO_iff_exists_eq_mul
{α : Type u_1}
{𝕜 : Type u_15}
[NormedDivisionRing 𝕜]
{l : Filter α}
{u v : α → 𝕜}
:
theorem
Asymptotics.IsLittleO.exists_eq_mul
{α : Type u_1}
{𝕜 : Type u_15}
[NormedDivisionRing 𝕜]
{l : Filter α}
{u v : α → 𝕜}
:
Alias of the forward direction of Asymptotics.isLittleO_iff_exists_eq_mul.
Miscellaneous lemmas #
theorem
Asymptotics.div_isBoundedUnder_of_isBigO
{𝕜 : Type u_15}
[NormedDivisionRing 𝕜]
{α : Type u_17}
{l : Filter α}
{f g : α → 𝕜}
(h : f =O[l] g)
:
theorem
Asymptotics.IsLittleO.tendsto_zero_of_tendsto
{α : Type u_17}
{E : Type u_18}
{𝕜 : Type u_19}
[NormedAddCommGroup E]
[NormedField 𝕜]
{u : α → E}
{v : α → 𝕜}
{l : Filter α}
{y : 𝕜}
(huv : u =o[l] v)
(hv : Filter.Tendsto v l (nhds y))
:
Filter.Tendsto u l (nhds 0)
theorem
Asymptotics.IsBigO.eq_zero_of_norm_pow_within
{E'' : Type u_9}
{F'' : Type u_10}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{f : E'' → F''}
{s : Set E''}
{x₀ : E''}
{n : ℕ}
(h : f =O[nhdsWithin x₀ s] fun (x : E'') => ‖x - x₀‖ ^ n)
(hx₀ : x₀ ∈ s)
(hn : n ≠ 0)
:
theorem
Asymptotics.IsBigOWith.right_le_sub_of_lt_one
{α : Type u_1}
{E' : Type u_6}
[SeminormedAddCommGroup E']
{c : ℝ}
{l : Filter α}
{f₁ f₂ : α → E'}
(h : IsBigOWith c l f₁ f₂)
(hc : c < 1)
:
IsBigOWith (1 / (1 - c)) l f₂ fun (x : α) => f₂ x - f₁ x
theorem
Asymptotics.IsBigOWith.right_le_add_of_lt_one
{α : Type u_1}
{E' : Type u_6}
[SeminormedAddCommGroup E']
{c : ℝ}
{l : Filter α}
{f₁ f₂ : α → E'}
(h : IsBigOWith c l f₁ f₂)
(hc : c < 1)
:
IsBigOWith (1 / (1 - c)) l f₂ fun (x : α) => f₁ x + f₂ x
theorem
Asymptotics.bound_of_isBigO_cofinite
{α : Type u_1}
{E : Type u_3}
{F'' : Type u_10}
[Norm E]
[NormedAddCommGroup F'']
{f : α → E}
{g'' : α → F''}
(h : f =O[Filter.cofinite] g'')
:
If f x = O(g x) along cofinite, then there exists a positive constant C such that
‖f x‖ ≤ C * ‖g x‖ whenever g x ≠ 0.
theorem
Asymptotics.isBigO_cofinite_iff
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[NormedAddCommGroup E'']
[NormedAddCommGroup F'']
{f'' : α → E''}
{g'' : α → F''}
(h : ∀ (x : α), g'' x = 0 → f'' x = 0)
:
theorem
Asymptotics.isBigO_one_nat_atTop_iff
{E'' : Type u_9}
[NormedAddCommGroup E'']
{f : ℕ → E''}
:
theorem
Asymptotics.isBigOWith_pi
{α : Type u_1}
{F' : Type u_7}
[SeminormedAddCommGroup F']
{g' : α → F'}
{l : Filter α}
{ι : Type u_17}
[Fintype ι]
{E' : ι → Type u_18}
[(i : ι) → NormedAddCommGroup (E' i)]
{f : α → (i : ι) → E' i}
{C : ℝ}
(hC : 0 ≤ C)
:
@[simp]
theorem
Asymptotics.isBigO_pi
{α : Type u_1}
{F' : Type u_7}
[SeminormedAddCommGroup F']
{g' : α → F'}
{l : Filter α}
{ι : Type u_17}
[Fintype ι]
{E' : ι → Type u_18}
[(i : ι) → NormedAddCommGroup (E' i)]
{f : α → (i : ι) → E' i}
:
@[simp]
theorem
Asymptotics.isLittleO_pi
{α : Type u_1}
{F' : Type u_7}
[SeminormedAddCommGroup F']
{g' : α → F'}
{l : Filter α}
{ι : Type u_17}
[Fintype ι]
{E' : ι → Type u_18}
[(i : ι) → NormedAddCommGroup (E' i)]
{f : α → (i : ι) → E' i}
:
theorem
Asymptotics.IsBigO.natCast_atTop
{E : Type u_3}
{F : Type u_4}
[Norm E]
[Norm F]
{R : Type u_17}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[Archimedean R]
{f : R → E}
{g : R → F}
(h : f =O[Filter.atTop] g)
:
theorem
Asymptotics.IsLittleO.natCast_atTop
{E : Type u_3}
{F : Type u_4}
[Norm E]
[Norm F]
{R : Type u_17}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[Archimedean R]
{f : R → E}
{g : R → F}
(h : f =o[Filter.atTop] g)
:
theorem
Asymptotics.isBigO_atTop_iff_eventually_exists_pos
{G : Type u_5}
{G' : Type u_8}
[Norm G]
[SeminormedAddCommGroup G']
{α : Type u_17}
[SemilatticeSup α]
[Nonempty α]
{f : α → G}
{g : α → G'}
:
theorem
summable_of_isBigO
{ι : Type u_1}
{E : Type u_2}
[SeminormedAddCommGroup E]
[CompleteSpace E]
{f : ι → E}
{g : ι → ℝ}
(hg : Summable g)
(h : f =O[Filter.cofinite] g)
:
Summable f
theorem
summable_of_isBigO_nat
{E : Type u_1}
[SeminormedAddCommGroup E]
[CompleteSpace E]
{f : ℕ → E}
{g : ℕ → ℝ}
(hg : Summable g)
(h : f =O[Filter.atTop] g)
:
Summable f
theorem
Summable.mul_tendsto_const
{F : Type u_1}
{ι : Type u_2}
[NormedRing F]
[NormMulClass F]
[NormOneClass F]
[CompleteSpace F]
{f g : ι → F}
(hf : Summable fun (n : ι) => ‖f n‖)
{c : F}
(hg : Filter.Tendsto g Filter.cofinite (nhds c))
:
theorem
OpenPartialHomeomorph.isBigOWith_congr
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{E : Type u_3}
[Norm E]
{F : Type u_4}
[Norm F]
(e : OpenPartialHomeomorph α β)
{b : β}
(hb : b ∈ e.target)
{f : β → E}
{g : β → F}
{C : ℝ}
:
Asymptotics.IsBigOWith C (nhds b) f g ↔ Asymptotics.IsBigOWith C (nhds (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)
Transfer IsBigOWith over an OpenPartialHomeomorph.
theorem
OpenPartialHomeomorph.isBigO_congr
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{E : Type u_3}
[Norm E]
{F : Type u_4}
[Norm F]
(e : OpenPartialHomeomorph α β)
{b : β}
(hb : b ∈ e.target)
{f : β → E}
{g : β → F}
:
Transfer IsBigO over an OpenPartialHomeomorph.
theorem
OpenPartialHomeomorph.isLittleO_congr
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{E : Type u_3}
[Norm E]
{F : Type u_4}
[Norm F]
(e : OpenPartialHomeomorph α β)
{b : β}
(hb : b ∈ e.target)
{f : β → E}
{g : β → F}
:
Transfer IsLittleO over an OpenPartialHomeomorph.
theorem
Homeomorph.isBigOWith_congr
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{E : Type u_3}
[Norm E]
{F : Type u_4}
[Norm F]
(e : α ≃ₜ β)
{b : β}
{f : β → E}
{g : β → F}
{C : ℝ}
:
Asymptotics.IsBigOWith C (nhds b) f g ↔ Asymptotics.IsBigOWith C (nhds (e.symm b)) (f ∘ ⇑e) (g ∘ ⇑e)
Transfer IsBigOWith over a Homeomorph.
theorem
ContinuousOn.isBigOWith_principal
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[TopologicalSpace α]
{s : Set α}
{f : α → E}
{c : F}
[SeminormedAddGroup E]
[Norm F]
(hf : ContinuousOn f s)
(hs : IsCompact s)
(hc : ‖c‖ ≠ 0)
:
Asymptotics.IsBigOWith (sSup (Norm.norm '' (f '' s)) / ‖c‖) (Filter.principal s) f fun (x : α) => c
theorem
ContinuousOn.isBigO_principal
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[TopologicalSpace α]
{s : Set α}
{f : α → E}
{c : F}
[SeminormedAddGroup E]
[Norm F]
(hf : ContinuousOn f s)
(hs : IsCompact s)
(hc : ‖c‖ ≠ 0)
:
theorem
ContinuousOn.isBigOWith_rev_principal
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[TopologicalSpace α]
{s : Set α}
{f : α → E}
[NormedAddGroup E]
[SeminormedAddGroup F]
(hf : ContinuousOn f s)
(hs : IsCompact s)
(hC : ∀ i ∈ s, f i ≠ 0)
(c : F)
:
Asymptotics.IsBigOWith (‖c‖ / sInf (Norm.norm '' (f '' s))) (Filter.principal s) (fun (x : α) => c) f
theorem
ContinuousOn.isBigO_rev_principal
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[TopologicalSpace α]
{s : Set α}
{f : α → E}
[NormedAddGroup E]
[SeminormedAddGroup F]
(hf : ContinuousOn f s)
(hs : IsCompact s)
(hC : ∀ i ∈ s, f i ≠ 0)
(c : F)
:
theorem
NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded
{ι : Type u_1}
{𝕜 : Type u_2}
{𝔸 : Type u_3}
[NormedDivisionRing 𝕜]
[NormedAddCommGroup 𝔸]
[Module 𝕜 𝔸]
[IsBoundedSMul 𝕜 𝔸]
{l : Filter ι}
{ε : ι → 𝕜}
{f : ι → 𝔸}
(hε : Filter.Tendsto ε l (nhds 0))
(hf : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ f))
:
Filter.Tendsto (ε • f) l (nhds 0)
The (scalar) product of a sequence that tends to zero with a bounded one also tends to zero.