Exponential sum growth exponents

This module formalizes the asymptotic definition of the exponential sum growth exponent from the blueprint's Exponential sum growth exponents chapter (beta-chapter). It defines admissible model-phase bounds at a fixed scale and defines β(α) as the least such exponent.

Overview

For α : ℝ≥0, an exponent β is admissible if every model-phase exponential sum at scale N = T ^ (α + o(1)) is bounded by T ^ (β + o(1)). We show that the admissible exponents form [β(α), ∞) and then specialize the bound to the logarithmic model phase.

Asymptotic definition

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.

noncomputable def Expdb.exponentialSum (F : VariableFunction (VariableObject.fixed ℝ) ℝ) (T N : VariableObject ℝ) (a b : VariableObject ℕ) : VariableObject ℂ

The variable exponential sum ∑ n ∈ [a, b], e(T F(n / N)).

Equations

• Expdb.exponentialSum F T N a b i = ∑ n ∈ Finset.Icc (a i) (b i), ↑(Real.fourierChar (T i * F i (↑n / N i)))

def Expdb.IsExponentSumBound (α : NNReal) (β : ℝ) : Prop

The assertion that β is an admissible exponential-sum growth exponent at scale α.

Equations

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

noncomputable def Expdb.exponentSumGrowthExponent (α : NNReal) : ℝ

The exponential sum growth exponent β(α) from the blueprint definition beta-def.

Equations

• Expdb.exponentSumGrowthExponent α = sInf {β : ℝ | Expdb.IsExponentSumBound α β}

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 {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 an infinitesimal error determines a power asymptotic.

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

Power bounds

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.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.

Admissible exponents

The candidate set is upward closed, nonempty, and bounded below.

Monotonicity

theorem Expdb.IsExponentSumBound.mono {α : NNReal} {β γ : ℝ} (hβ : IsExponentSumBound α β) (hβγ : β ≤ γ) : IsExponentSumBound α γ

Admissible exponential-sum bounds are monotone in the exponent.

Nonemptiness and lower bound

theorem Expdb.isExponentSumBound_self (α : NNReal) : IsExponentSumBound α ↑α

The triangle inequality gives the admissible exponent α.

theorem Expdb.IsExponentSumBound.nonneg {α : NNReal} {β : ℝ} (hβ : IsExponentSumBound α β) : 0 ≤ β

Every admissible exponent at a nonnegative scale is nonnegative.

The least admissible exponent

theorem Expdb.isExponentSumBound_exponentSumGrowthExponent (α : NNReal) : IsExponentSumBound α (exponentSumGrowthExponent α)

By underspill, the infimum of the admissible exponents is itself admissible.

theorem Expdb.exponentSumGrowthExponent_le_iff {α : NNReal} {β : ℝ} : exponentSumGrowthExponent α ≤ β ↔ IsExponentSumBound α β

The defining universal property of the exponential sum growth exponent.

theorem Expdb.isLeast_exponentSumGrowthExponent (α : NNReal) : IsLeast {β : ℝ | IsExponentSumBound α β} (exponentSumGrowthExponent α)

The exponent sum growth exponent is the least admissible exponent.

theorem Expdb.exponentSumBounds_eq_Ici (α : NNReal) : {β : ℝ | IsExponentSumBound α β} = Set.Ici (exponentSumGrowthExponent α)

At scale α, the admissible exponents form the interval [β(α), ∞).

theorem Expdb.isClosed_exponentSumBounds (α : NNReal) : IsClosed {β : ℝ | IsExponentSumBound α β}

The set of admissible exponential-sum exponents at scale α is closed.

Logarithmic model phase

theorem Expdb.isPowerBounded_logPhase (α : NNReal) {N T : VariableObject ℝ} {a b : VariableObject ℕ} (hN : ∀ (i : ℕ), 1 ≤ N i) (hT : ∀ (i : ℕ), 1 ≤ T i) (hTunbounded : T.IsUnbounded) (hNT : IsPowerAsymptotic N T ↑α) (hab : ∀ (i : ℕ), N i ≤ ↑(a i) ∧ ↑(b i) ≤ 2 * N i) : IsPowerBounded (exponentialSum logPhase T N a b) T (exponentSumGrowthExponent α)

Logarithmic-phase sums at scale α are power-bounded by the least admissible exponent. This specializes isExponentSumBound_exponentSumGrowthExponent to logPhase.