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.

Exponential-sum growth definition

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 = Expdb.exponentialSumAt (F i) (T i) (N i) (a i) (b i)

@[simp]

theorem Expdb.exponentialSum_apply (F : VariableFunction (VariableObject.fixed ℝ) ℝ) (T N : VariableObject ℝ) (a b : VariableObject ℕ) (i : ℕ) : exponentialSum F T N a b i = exponentialSumAt (F i) (T i) (N i) (a i) (b 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.

def Expdb.exponentSumBounds (α : NNReal) : Set ℝ

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

Equations

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

@[simp]

theorem Expdb.mem_exponentSumBounds {α : NNReal} {β : ℝ} : β ∈ exponentSumBounds α ↔ IsExponentSumBound α β

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

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

Equations

• Expdb.exponentSumGrowthExponent α = sInf (Expdb.exponentSumBounds α)

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 (exponentSumBounds α) (exponentSumGrowthExponent α)

The exponent sum growth exponent is the least admissible exponent.

theorem Expdb.exponentSumBounds_eq_Ici (α : NNReal) : exponentSumBounds α = Set.Ici (exponentSumGrowthExponent α)

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

theorem Expdb.isClosed_exponentSumBounds (α : NNReal) : IsClosed (exponentSumBounds α)

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.

theorem Expdb.le_exponentSumGrowthExponent_of_logPhase_lower_bound (α : NNReal) {N T : VariableObject ℝ} {a b : VariableObject ℕ} {c γ : ℝ} (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) (hc : 0 < c) (hlower : ∀ᶠ (i : ℕ) in Filter.atTop, c * T i ^ γ ≤ ‖exponentialSum logPhase T N a b i‖) : γ ≤ exponentSumGrowthExponent α

A lower bound of size T ^ γ for logarithmic-phase sums along an admissible family of scales forces γ ≤ β(α).