Non-asymptotic exponential sum growth bounds

This module formalizes Lemma 4.3 of the ANTEDB blueprint. It gives a fixed-parameter, epsilon--delta characterization of the exponential sum growth exponent.

Fixed-parameter formulation

noncomputable def Expdb.exponentialSumAt (F : ℝ → ℝ) (T N : ℝ) (a b : ℕ) : ℂ

The exponential sum at fixed parameters.

Equations

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

def Expdb.IsApproximateModelPhaseFunction (F : ℝ → ℝ) (σ : ℝ) (P : ℕ) (δ : ℝ) : Prop

A fixed phase function whose model-phase errors through order P are at most δ.

Equations

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

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

The fixed-parameter epsilon--delta bound from Lemma 4.3 of the blueprint.

Equations

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

Uniform approximation by fixed phases

From fixed bounds to asymptotic bounds

Building asymptotic counterexamples

Lemma 4.3

theorem Expdb.exponentSumGrowthExponent_le_iff_nonAsymptotic {α : NNReal} {β : ℝ} : exponentSumGrowthExponent α ≤ β ↔ IsExponentSumBoundNonAsymptotic α β

The non-asymptotic characterization of the exponential sum growth exponent.