A collection of specific asymptotic results

This file contains specific lemmas about asymptotics which don't have their place in the general theory developed in Mathlib.Analysis.Asymptotics.Asymptotics.

theorem Filter.IsBoundedUnder.isLittleO_sub_self_inv {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [Norm E] {a : 𝕜} {f : 𝕜 → E} (h : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin a {a}ᶜ) (norm ∘ f)) : f =o[nhdsWithin a {a}ᶜ] fun (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.

theorem pow_div_pow_eventuallyEq_atTop {𝕜 : Type u_1} [LinearOrderedField 𝕜] {p : ℕ} {q : ℕ} : (fun (x : 𝕜) => x ^ p / x ^ q) =ᶠ[Filter.atTop] fun (x : 𝕜) => x ^ (↑p - ↑q)

theorem pow_div_pow_eventuallyEq_atBot {𝕜 : Type u_1} [LinearOrderedField 𝕜] {p : ℕ} {q : ℕ} : (fun (x : 𝕜) => x ^ p / x ^ q) =ᶠ[Filter.atBot] fun (x : 𝕜) => x ^ (↑p - ↑q)

theorem tendsto_pow_div_pow_atTop_atTop {𝕜 : Type u_1} [LinearOrderedField 𝕜] {p : ℕ} {q : ℕ} (hpq : q < p) : Filter.Tendsto (fun (x : 𝕜) => x ^ p / x ^ q) Filter.atTop Filter.atTop

theorem tendsto_pow_div_pow_atTop_zero {𝕜 : Type u_1} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : ℕ} {q : ℕ} (hpq : p < q) : Filter.Tendsto (fun (x : 𝕜) => x ^ p / x ^ q) Filter.atTop (nhds 0)

theorem Asymptotics.isLittleO_pow_pow_atTop_of_lt {𝕜 : Type u_1} [NormedLinearOrderedField 𝕜] [OrderTopology 𝕜] {p : ℕ} {q : ℕ} (hpq : p < q) : (fun (x : 𝕜) => x ^ p) =o[Filter.atTop] fun (x : 𝕜) => x ^ q

theorem Asymptotics.IsBigO.trans_tendsto_norm_atTop {𝕜 : Type u_1} [NormedLinearOrderedField 𝕜] {α : Type u_2} {u : α → 𝕜} {v : α → 𝕜} {l : Filter α} (huv : u =O[l] v) (hu : Filter.Tendsto (fun (x : α) => ‖u x‖) l Filter.atTop) : Filter.Tendsto (fun (x : α) => ‖v x‖) l Filter.atTop

theorem Asymptotics.IsLittleO.sum_range {α : Type u_1} [NormedAddCommGroup α] {f : ℕ → α} {g : ℕ → ℝ} (h : f =o[Filter.atTop] g) (hg : 0 ≤ g) (h'g : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, g i) Filter.atTop Filter.atTop) : (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) =o[Filter.atTop] fun (n : ℕ) => ∑ i ∈ Finset.range n, g i

theorem Asymptotics.isLittleO_sum_range_of_tendsto_zero {α : Type u_1} [NormedAddCommGroup α] {f : ℕ → α} (h : Filter.Tendsto f Filter.atTop (nhds 0)) : (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) =o[Filter.atTop] fun (n : ℕ) => ↑n

theorem Filter.Tendsto.cesaro_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {u : ℕ → E} {l : E} (h : Filter.Tendsto u Filter.atTop (nhds l)) : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ • ∑ i ∈ Finset.range n, u i) Filter.atTop (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.atTop (nhds l)) : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * ∑ i ∈ Finset.range n, u i) Filter.atTop (nhds l)

The Cesaro average of a converging sequence converges to the same limit.