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/Defs.lean and Mathlib/Analysis/Asymptotics/Lemmas.lean.

theorem Filter.IsBoundedUnder.isLittleO_sub_self_inv {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [Norm E] {a : 𝕜} {f : 𝕜 → E} (h : 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 Asymptotics.isLittleO_pow_pow_cobounded_of_lt {R : Type u_1} [NormedRing R] [NormMulClass R] {p q : ℕ} (hpq : p < q) : (fun (x : R) => x ^ p) =o[Bornology.cobounded R] fun (x : R) => x ^ q

theorem Asymptotics.isBigO_pow_pow_cobounded_of_le {R : Type u_1} [NormedRing R] [NormMulClass R] {p q : ℕ} (hpq : p ≤ q) : (fun (x : R) => x ^ p) =O[Bornology.cobounded R] fun (x : R) => x ^ q

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

theorem pow_div_pow_eventuallyEq_atBot {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [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} [NormedField 𝕜] {α : 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.IsEquivalent.rpow {α : Type u_1} {u v : α → ℝ} {l : Filter α} (hv : 0 ≤ v) (h : IsEquivalent l u v) {r : ℝ} : IsEquivalent l (u ^ r) (v ^ r)

theorem Asymptotics.IsEquivalent.log {α : Type u_1} {l : Filter α} {f g : α → ℝ} (hfg : IsEquivalent l f g) (g_tendsto : Filter.Tendsto g l Filter.atTop) : IsEquivalent l (fun (n : α) => Real.log (f n)) fun (n : α) => Real.log (g n)

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 : Tendsto u atTop (nhds l)) : Tendsto (fun (n : ℕ) => (↑n)⁻¹ • ∑ i ∈ Finset.range n, u i) atTop (nhds l)

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

theorem Filter.Tendsto.cesaro {u : ℕ → ℝ} {l : ℝ} (h : Tendsto u atTop (nhds l)) : Tendsto (fun (n : ℕ) => (↑n)⁻¹ * ∑ i ∈ Finset.range n, u i) atTop (nhds l)

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

theorem Asymptotics.isEquivalent_nat_floor {R : Type u_1} [NormedField R] [LinearOrder R] [IsStrictOrderedRing R] [OrderTopology R] [FloorRing R] : IsEquivalent Filter.atTop (fun (x : R) => ↑⌊x⌋₊) fun (x : R) => x

theorem Asymptotics.isEquivalent_nat_ceil {R : Type u_1} [NormedField R] [LinearOrder R] [IsStrictOrderedRing R] [OrderTopology R] [FloorRing R] : IsEquivalent Filter.atTop (fun (x : R) => ↑⌈x⌉₊) fun (x : R) => x

Bounded Range versus IsBigO Asymptotics

For a continuous function f into a seminormed space, having bounded range is equivalent to being O(1) along the cocompact filter (Continuous.isBounded_range_iff_isBigO). On an unbounded linear order whose order topology has compact intervals, this means being O(1) along both atTop and atBot (Continuous.isBounded_range_iff_isBigO_atTop_atBot). For an even function a single O(1) bound along atTop already suffices (Continuous.isBounded_range_iff_isBigO_atTop_of_even).

theorem Continuous.isBounded_range_iff_isBigO {E : Type u_1} [SeminormedAddCommGroup E] {D : Type u_2} [TopologicalSpace D] {f : D → E} (hf : Continuous f) : Bornology.IsBounded (Set.range f) ↔ f =O[Filter.cocompact D] 1

A continuous function f has bounded range if and only if it is O(1) with respect to the cocompact filter.

theorem Continuous.isBounded_range_iff_isBigO_atTop_atBot {E : Type u_1} [SeminormedAddCommGroup E] {β : Type u_3} [TopologicalSpace β] [LinearOrder β] [OrderClosedTopology β] [CompactIccSpace β] [NoMaxOrder β] [NoMinOrder β] {f : β → E} (hf : Continuous f) : Bornology.IsBounded (Set.range f) ↔ f =O[Filter.atTop] 1 ∧ f =O[Filter.atBot] 1

A continuous function f on an unbounded linear order with compact intervals has bounded range if and only if it is O(1) at both atTop and atBot.

theorem Continuous.isBounded_range_iff_isBigO_atTop_of_even {E : Type u_1} [SeminormedAddCommGroup E] {β : Type u_3} [TopologicalSpace β] [LinearOrder β] [OrderClosedTopology β] [CompactIccSpace β] [NoMaxOrder β] [NoMinOrder β] [AddCommGroup β] [IsOrderedAddMonoid β] {f : β → E} (hf : Continuous f) (heven : Function.Even f) : Bornology.IsBounded (Set.range f) ↔ f =O[Filter.atTop] 1

A continuous even function has bounded range if and only if f =O[atTop] 1.