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