mathlib documentation

analysis.asymptotics.specific_asymptotics

A collection of specific asymptotic results #

This file contains specific lemmas about asymptotics which don't have their place in the general theory developped in analysis.asymptotics.asymptotics.

source
theorem filter.is_bounded_under.is_o_sub_self_inv {π•œ : Type u_1} {E : Type u_2} [normed_field π•œ] [has_norm E] {a : π•œ} {f : π•œ β†’ E} (h : filter.is_bounded_under has_le.le (nhds_within a {a}ᢜ) (has_norm.norm ∘ f)) :
f =o[nhds_within a {a}ᢜ] Ξ» (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.

source
theorem pow_div_pow_eventually_eq_at_top {π•œ : Type u_1} [linear_ordered_field π•œ] {p q : β„•} :
(Ξ» (x : π•œ), x ^ p / x ^ q) =αΆ [filter.at_top] Ξ» (x : π•œ), x ^ (↑p - ↑q)
source
theorem pow_div_pow_eventually_eq_at_bot {π•œ : Type u_1} [linear_ordered_field π•œ] {p q : β„•} :
(Ξ» (x : π•œ), x ^ p / x ^ q) =αΆ [filter.at_bot] Ξ» (x : π•œ), x ^ (↑p - ↑q)
source
theorem tendsto_zpow_at_top_at_top {π•œ : Type u_1} [linear_ordered_field π•œ] {n : β„€} (hn : 0 < n) :
filter.tendsto (Ξ» (x : π•œ), x ^ n) filter.at_top filter.at_top
source
theorem tendsto_pow_div_pow_at_top_at_top {π•œ : Type u_1} [linear_ordered_field π•œ] {p q : β„•} (hpq : q < p) :
filter.tendsto (Ξ» (x : π•œ), x ^ p / x ^ q) filter.at_top filter.at_top
source
theorem tendsto_pow_div_pow_at_top_zero {π•œ : Type u_1} [linear_ordered_field π•œ] [topological_space π•œ] [order_topology π•œ] {p q : β„•} (hpq : p < q) :
filter.tendsto (Ξ» (x : π•œ), x ^ p / x ^ q) filter.at_top (nhds 0)
source
theorem asymptotics.is_o_pow_pow_at_top_of_lt {π•œ : Type u_1} [normed_linear_ordered_field π•œ] [order_topology π•œ] {p q : β„•} (hpq : p < q) :
(Ξ» (x : π•œ), x ^ p) =o[filter.at_top] Ξ» (x : π•œ), x ^ q
source
theorem asymptotics.is_O.trans_tendsto_norm_at_top {π•œ : Type u_1} [normed_linear_ordered_field π•œ] {Ξ± : Type u_2} {u v : Ξ± β†’ π•œ} {l : filter Ξ±} (huv : u =O[l] v) (hu : filter.tendsto (Ξ» (x : Ξ±), β€–u xβ€–) l filter.at_top) :
filter.tendsto (Ξ» (x : Ξ±), β€–v xβ€–) l filter.at_top
source
theorem asymptotics.is_o.sum_range {Ξ± : Type u_1} [normed_add_comm_group Ξ±] {f : β„• β†’ Ξ±} {g : β„• β†’ ℝ} (h : f =o[filter.at_top] g) (hg : 0 ≀ g) (h'g : filter.tendsto (Ξ» (n : β„•), (finset.range n).sum (Ξ» (i : β„•), g i)) filter.at_top filter.at_top) :
(Ξ» (n : β„•), (finset.range n).sum (Ξ» (i : β„•), f i)) =o[filter.at_top] Ξ» (n : β„•), (finset.range n).sum (Ξ» (i : β„•), g i)
source
theorem asymptotics.is_o_sum_range_of_tendsto_zero {Ξ± : Type u_1} [normed_add_comm_group Ξ±] {f : β„• β†’ Ξ±} (h : filter.tendsto f filter.at_top (nhds 0)) :
(Ξ» (n : β„•), (finset.range n).sum (Ξ» (i : β„•), f i)) =o[filter.at_top] Ξ» (n : β„•), ↑n
source
theorem filter.tendsto.cesaro_smul {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] {u : β„• β†’ E} {l : E} (h : filter.tendsto u filter.at_top (nhds l)) :
filter.tendsto (Ξ» (n : β„•), (↑n)⁻¹ β€’ (finset.range n).sum (Ξ» (i : β„•), u i)) filter.at_top (nhds l)

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

source
theorem filter.tendsto.cesaro {u : β„• β†’ ℝ} {l : ℝ} (h : filter.tendsto u filter.at_top (nhds l)) :
filter.tendsto (Ξ» (n : β„•), (↑n)⁻¹ * (finset.range n).sum (Ξ» (i : β„•), u i)) filter.at_top (nhds l)

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