# mathlibdocumentation

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.

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 : ) :
f =o[ {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.

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)
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)
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
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
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)
theorem asymptotics.is_o_pow_pow_at_top_of_lt {๐ : Type u_1} [order_topology ๐] {p q : โ} (hpq : p < q) :
(ฮป (x : ๐), x ^ p) =o[filter.at_top] ฮป (x : ๐), x ^ q
theorem asymptotics.is_O.trans_tendsto_norm_at_top {๐ : Type u_1} {ฮฑ : 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
theorem asymptotics.is_o.sum_range {ฮฑ : Type u_1} {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)
theorem asymptotics.is_o_sum_range_of_tendsto_zero {ฮฑ : Type u_1} {f : โ โ ฮฑ} (h : (nhds 0)) :
(ฮป (n : โ), (finset.range n).sum (ฮป (i : โ), f i)) =o[filter.at_top] ฮป (n : โ), โn
theorem filter.tendsto.cesaro_smul {E : Type u_1} [ E] {u : โ โ E} {l : E} (h : (nhds l)) :

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

theorem filter.tendsto.cesaro {u : โ โ โ} {l : โ} (h : (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.