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.