Power asymptotics

This module collects the project-wide notation and elementary calculus for quantities of the form T ^ (α + o(1)). It is independent of exponential sums and can therefore be reused by all later asymptotic arguments.

Definitions

def Expdb.IsPowerAsymptotic (N T : VariableObject ℝ) (α : ℝ) : Prop

N = T ^ (α + o(1)), expressed using a variable exponent that is equal to α up to an infinitesimal.

Equations

• One or more equations did not get rendered due to their size.

def Expdb.IsPowerBounded {E : Type u_1} [SeminormedAddCommGroup E] (X : VariableObject E) (T : VariableObject ℝ) (β : ℝ) : Prop

X ≪ T ^ (β + o(1)), expressed using a variable exponent that is equal to β up to an infinitesimal.

Equations

• One or more equations did not get rendered due to their size.

Power asymptotics

theorem Expdb.IsPowerAsymptotic.eventually_between {N T : VariableObject ℝ} {α ε : ℝ} (hNT : IsPowerAsymptotic N T α) (hT : ∀ᶠ (i : ℕ) in Filter.atTop, 1 ≤ T i) (hε : 0 < ε) : ∀ᶠ (i : ℕ) in Filter.atTop, T i ^ (α - ε) ≤ N i ∧ N i ≤ T i ^ (α + ε)

If N = T ^ (α + o(1)), then N eventually lies between the powers with exponents α - ε and α + ε.

theorem Expdb.isPowerAsymptotic_of_logb_tendsto {N T : VariableObject ℝ} {α : ℝ} (hT : ∀ᶠ (i : ℕ) in Filter.atTop, 1 < T i) (hN : ∀ᶠ (i : ℕ) in Filter.atTop, 0 < N i) (hexponent : Filter.Tendsto (fun (i : ℕ) => Real.logb (T i) (N i)) Filter.atTop (nhds α)) : IsPowerAsymptotic N T α

Convergence of the logarithmic exponent gives a power asymptotic.

theorem Expdb.isPowerAsymptotic_of_between_of_infinitesimal {N T δ : VariableObject ℝ} {α : ℝ} (hT : ∀ (i : ℕ), 1 < T i) (hN : ∀ (i : ℕ), 0 < N i) (hδ : δ.IsInfinitesimal) (hbetween : ∀ (i : ℕ), T i ^ (α - δ i) ≤ N i ∧ N i ≤ T i ^ (α + δ i)) : IsPowerAsymptotic N T α

A variable power sandwich with an infinitesimal error determines a power asymptotic. No sign condition on the error is needed.

theorem Expdb.isPowerAsymptotic_of_between {N T δ : VariableObject ℝ} {α : ℝ} (hT : ∀ (i : ℕ), 1 < T i) (hN : ∀ (i : ℕ), 0 < N i) (_hδnonneg : ∀ (i : ℕ), 0 ≤ δ i) (hδ : δ.IsInfinitesimal) (hbetween : ∀ (i : ℕ), T i ^ (α - δ i) ≤ N i ∧ N i ≤ T i ^ (α + δ i)) : IsPowerAsymptotic N T α

A variable power sandwich with a nonnegative infinitesimal error determines a power asymptotic. This is the compatibility form of isPowerAsymptotic_of_between_of_infinitesimal.

theorem Expdb.isPowerAsymptotic_of_between_const_rpow {N T : VariableObject ℝ} {α A B : ℝ} (hα : 0 < α) (hA : 0 < A) (hB : 0 < B) (hNtop : Filter.Tendsto N Filter.atTop Filter.atTop) (hT : ∀ᶠ (i : ℕ) in Filter.atTop, A * N i ^ α⁻¹ ≤ T i ∧ T i ≤ B * N i ^ α⁻¹) : IsPowerAsymptotic N T α

Fixed positive multiplicative uncertainty in T = N ^ α⁻¹ does not affect the power asymptotic N = T ^ (α + o(1)).

Algebra and limits

theorem Expdb.isPowerAsymptotic_self (T : VariableObject ℝ) : IsPowerAsymptotic T T 1

A base is power-asymptotic to itself with exponent one.

theorem Expdb.IsPowerAsymptotic.mul {A B T : VariableObject ℝ} {α β : ℝ} (hA : IsPowerAsymptotic A T α) (hB : IsPowerAsymptotic B T β) (hT : ∀ (i : ℕ), 1 ≤ T i) : IsPowerAsymptotic (A * B) T (α + β)

Products of powers add their asymptotic exponents.

theorem Expdb.IsPowerAsymptotic.div {A B T : VariableObject ℝ} {α β : ℝ} (hA : IsPowerAsymptotic A T α) (hB : IsPowerAsymptotic B T β) (hT : ∀ (i : ℕ), 1 ≤ T i) : IsPowerAsymptotic (A / B) T (α - β)

Quotients of powers subtract their asymptotic exponents.

theorem Expdb.IsPowerAsymptotic.tendsto_zero_of_neg {X T : VariableObject ℝ} {α : ℝ} (hX : IsPowerAsymptotic X T α) (hα : α < 0) (hT : ∀ (i : ℕ), 1 ≤ T i) (hTunbounded : T.IsUnbounded) : Filter.Tendsto X Filter.atTop (nhds 0)

A negative power-asymptotic exponent forces convergence to zero.

theorem Expdb.IsPowerAsymptotic.tendsto_atTop_of_pos {X T : VariableObject ℝ} {α : ℝ} (hX : IsPowerAsymptotic X T α) (hα : 0 < α) (hT : ∀ (i : ℕ), 1 ≤ T i) (hTunbounded : T.IsUnbounded) : Filter.Tendsto X Filter.atTop Filter.atTop

A positive power-asymptotic exponent forces convergence to infinity.

theorem Expdb.isPowerAsymptotic_zero_of_tendsto_one {X T : VariableObject ℝ} (hX : Filter.Tendsto X Filter.atTop (nhds 1)) (hT : ∀ (i : ℕ), 1 ≤ T i) (hTunbounded : T.IsUnbounded) : IsPowerAsymptotic X T 0

A quantity tending to one has power-asymptotic exponent zero relative to any unbounded base that is at least one.

Natural-valued power scales

noncomputable def Expdb.floorRpow (T : VariableObject ℝ) (κ : ℝ) : VariableObject ℕ

The positive natural scale obtained by taking the floor of T ^ κ.

Equations

• Expdb.floorRpow T κ i = max 1 ⌊T i ^ κ⌋₊

theorem Expdb.floorRpow_pos (T : VariableObject ℝ) (κ : ℝ) (i : ℕ) : 0 < floorRpow T κ i

theorem Expdb.tendsto_floorRpow_cast_div_rpow_one {T : VariableObject ℝ} {κ : ℝ} (hκ : 0 < κ) (hT : Filter.Tendsto T Filter.atTop Filter.atTop) : Filter.Tendsto (fun (i : ℕ) => ↑(floorRpow T κ i) / T i ^ κ) Filter.atTop (nhds 1)

Flooring a divergent positive power introduces only a multiplicative 1 + o(1) error.

theorem Expdb.isPowerAsymptotic_floorRpow {T : VariableObject ℝ} {κ : ℝ} (hκ : 0 < κ) (hT : ∀ (i : ℕ), 1 ≤ T i) (hTunbounded : T.IsUnbounded) : IsPowerAsymptotic (fun (i : ℕ) => ↑(floorRpow T κ i)) T κ

The cast of floorRpow T κ is power-asymptotic to exponent κ.

Power bounds

theorem Expdb.isLittleO_rpow_comp_tendsto_of_lt {T : VariableObject ℝ} {β γ : ℝ} (hT : Filter.Tendsto T Filter.atTop Filter.atTop) (hβγ : β < γ) : (fun (i : ℕ) => T i ^ β) =o[Filter.atTop] fun (i : ℕ) => T i ^ γ

Strictly increasing a fixed exponent makes a real power little-o along a base tending to infinity.

theorem Expdb.isPowerBounded_iff_forall_pos {E : Type u_1} [SeminormedAddCommGroup E] (X : VariableObject E) (T : VariableObject ℝ) (β : ℝ) (hT : ∀ (i : ℕ), 1 ≤ T i) (hTunbounded : T.IsUnbounded) : IsPowerBounded X T β ↔ ∀ (ε : ℝ), 0 < ε → X =O[Filter.atTop] fun (i : ℕ) => T i ^ (β + ε)

If T is at least one and unbounded, then X ≪ T ^ (β + o(1)) iff X = O(T ^ (β + ε)) for every fixed ε > 0.

theorem Expdb.IsPowerBounded.mono {E : Type u_1} [SeminormedAddCommGroup E] {X : VariableObject E} {T : VariableObject ℝ} {β γ : ℝ} (hX : IsPowerBounded X T β) (hT : ∀ᶠ (i : ℕ) in Filter.atTop, 1 ≤ T i) (hβγ : β ≤ γ) : IsPowerBounded X T γ

Increasing the exponent preserves a power bound when the base is eventually at least one.

theorem Expdb.exponent_le_of_isPowerBounded_of_eventually_norm_ge_rpow {E : Type u_1} [SeminormedAddCommGroup E] {X : VariableObject E} {T : VariableObject ℝ} {β γ c : ℝ} (hT : ∀ (i : ℕ), 1 ≤ T i) (hTunbounded : T.IsUnbounded) (hbound : IsPowerBounded X T β) (hc : 0 < c) (hlower : ∀ᶠ (i : ℕ) in Filter.atTop, c * T i ^ γ ≤ ‖X i‖) : γ ≤ β

A power lower bound for an unbounded object forces its exponent to be no larger than any admissible power-bound exponent.