A collection of specific asymptotic results #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains specific lemmas about asymptotics which don't have their place in the general theory developped in analysis.asymptotics.asymptotics.

source

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)) :

f =o[nhds_within a {a}ᶜ] λ (x : 𝕜), (x - a)⁻¹

If f : 𝕜 → E is bounded in a punctured neighborhood of a, then f(x) = o((x - a)⁻¹) as x → a, x ≠ a.

source

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)

source

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)

source

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

source

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

source

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)

source

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

source

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

source

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)

source

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

source

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.

source

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.