# A collection of specific asymptotic results #

This file contains specific lemmas about asymptotics which don't have their place in the general theory developed in Mathlib.Analysis.Asymptotics.Asymptotics.

theorem Filter.IsBoundedUnder.isLittleO_sub_self_inv {๐ : Type u_1} {E : Type u_2} [NormedField ๐] [Norm E] {a : ๐} {f : ๐ โ E} (h : Filter.IsBoundedUnder (fun (x x_1 : โ) => x โค x_1) (nhdsWithin a {a}แถ) (norm โ f)) :
f =o[nhdsWithin a {a}แถ] fun (x : ๐) => (x - a)โปยน

If f : ๐ โ E is bounded in a punctured neighborhood of a, then f(x) = o((x - a)โปยน) as x โ a, x โ  a.

theorem pow_div_pow_eventuallyEq_atTop {๐ : Type u_1} [] {p : โ} {q : โ} :
(fun (x : ๐) => x ^ p / x ^ q) =แถ [Filter.atTop] fun (x : ๐) => x ^ (โp - โq)
theorem pow_div_pow_eventuallyEq_atBot {๐ : Type u_1} [] {p : โ} {q : โ} :
(fun (x : ๐) => x ^ p / x ^ q) =แถ [Filter.atBot] fun (x : ๐) => x ^ (โp - โq)
theorem tendsto_pow_div_pow_atTop_atTop {๐ : Type u_1} [] {p : โ} {q : โ} (hpq : q < p) :
Filter.Tendsto (fun (x : ๐) => x ^ p / x ^ q) Filter.atTop Filter.atTop
theorem tendsto_pow_div_pow_atTop_zero {๐ : Type u_1} [] [TopologicalSpace ๐] [OrderTopology ๐] {p : โ} {q : โ} (hpq : p < q) :
Filter.Tendsto (fun (x : ๐) => x ^ p / x ^ q) Filter.atTop (nhds 0)
theorem Asymptotics.isLittleO_pow_pow_atTop_of_lt {๐ : Type u_1} [] [OrderTopology ๐] {p : โ} {q : โ} (hpq : p < q) :
(fun (x : ๐) => x ^ p) =o[Filter.atTop] fun (x : ๐) => x ^ q
theorem Asymptotics.IsBigO.trans_tendsto_norm_atTop {๐ : Type u_1} [] {ฮฑ : Type u_2} {u : ฮฑ โ ๐} {v : ฮฑ โ ๐} {l : Filter ฮฑ} (huv : u =O[l] v) (hu : Filter.Tendsto (fun (x : ฮฑ) => โu xโ) l Filter.atTop) :
Filter.Tendsto (fun (x : ฮฑ) => โv xโ) l Filter.atTop
theorem Asymptotics.IsLittleO.sum_range {ฮฑ : Type u_1} [] {f : โ โ ฮฑ} {g : โ โ โ} (h : f =o[Filter.atTop] g) (hg : 0 โค g) (h'g : Filter.Tendsto (fun (n : โ) => โ i โ , g i) Filter.atTop Filter.atTop) :
(fun (n : โ) => โ i โ , f i) =o[Filter.atTop] fun (n : โ) => โ i โ , g i
theorem Asymptotics.isLittleO_sum_range_of_tendsto_zero {ฮฑ : Type u_1} [] {f : โ โ ฮฑ} (h : Filter.Tendsto f Filter.atTop (nhds 0)) :
(fun (n : โ) => โ i โ , f i) =o[Filter.atTop] fun (n : โ) => โn
theorem Filter.Tendsto.cesaro_smul {E : Type u_1} [] {u : โ โ E} {l : E} (h : Filter.Tendsto u Filter.atTop (nhds l)) :
Filter.Tendsto (fun (n : โ) => (โn)โปยน โข โ i โ , u i) Filter.atTop (nhds l)

The Cesaro average of a converging sequence converges to the same limit.

theorem Filter.Tendsto.cesaro {u : โ โ โ} {l : โ} (h : Filter.Tendsto u Filter.atTop (nhds l)) :
Filter.Tendsto (fun (n : โ) => (โn)โปยน * โ i โ , u i) Filter.atTop (nhds l)

The Cesaro average of a converging sequence converges to the same limit.