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 : filter.is_bounded_under has_le.le (nhds_within a {a}แถ) (has_norm.norm โ f)) :
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 : โ} :
theorem
pow_div_pow_eventually_eq_at_bot
{๐ : Type u_1}
[linear_ordered_field ๐]
{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}
[normed_linear_ordered_field ๐]
[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}
[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
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)
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
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.
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.