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
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_fpow_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 (๐ 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) :
asymptotics.is_o (ฮป (x : ๐), x ^ p) (ฮป (x : ๐), x ^ q) filter.at_top
theorem
asymptotics.is_O.trans_tendsto_norm_at_top
{๐ : Type u_1}
[normed_linear_ordered_field ๐]
{ฮฑ : Type u_2}
{u v : ฮฑ โ ๐}
{l : filter ฮฑ}
(huv : asymptotics.is_O u v l)
(hu : filter.tendsto (ฮป (x : ฮฑ), โฅu xโฅ) l filter.at_top) :
filter.tendsto (ฮป (x : ฮฑ), โฅv xโฅ) l filter.at_top