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.

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_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