Documentation

Mathlib.Analysis.Asymptotics.SpecificAsymptotics

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 (x1 x2 : โ„) => x1 โ‰ค x2) (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} [LinearOrderedField ๐•œ] {p : โ„•} {q : โ„•} :
(fun (x : ๐•œ) => x ^ p / x ^ q) =แถ [Filter.atTop] fun (x : ๐•œ) => x ^ (โ†‘p - โ†‘q)
theorem pow_div_pow_eventuallyEq_atBot {๐•œ : Type u_1} [LinearOrderedField ๐•œ] {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} [LinearOrderedField ๐•œ] {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} [LinearOrderedField ๐•œ] [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} [NormedLinearOrderedField ๐•œ] [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} [NormedLinearOrderedField ๐•œ] {ฮฑ : 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} [NormedAddCommGroup ฮฑ] {f : โ„• โ†’ ฮฑ} {g : โ„• โ†’ โ„} (h : f =o[Filter.atTop] g) (hg : 0 โ‰ค g) (h'g : Filter.Tendsto (fun (n : โ„•) => โˆ‘ i โˆˆ Finset.range n, g i) Filter.atTop Filter.atTop) :
(fun (n : โ„•) => โˆ‘ i โˆˆ Finset.range n, f i) =o[Filter.atTop] fun (n : โ„•) => โˆ‘ i โˆˆ Finset.range n, g i
theorem Asymptotics.isLittleO_sum_range_of_tendsto_zero {ฮฑ : Type u_1} [NormedAddCommGroup ฮฑ] {f : โ„• โ†’ ฮฑ} (h : Filter.Tendsto f Filter.atTop (nhds 0)) :
(fun (n : โ„•) => โˆ‘ i โˆˆ Finset.range n, f i) =o[Filter.atTop] fun (n : โ„•) => โ†‘n
theorem Filter.Tendsto.cesaro_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace โ„ E] {u : โ„• โ†’ E} {l : E} (h : Filter.Tendsto u Filter.atTop (nhds l)) :
Filter.Tendsto (fun (n : โ„•) => (โ†‘n)โปยน โ€ข โˆ‘ i โˆˆ Finset.range n, 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 โˆˆ Finset.range n, u i) Filter.atTop (nhds l)

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