Non-asymptotic exponential sum growth bounds

This module formalizes the non-asymptotic definition of exponential sum exponent from the blueprint's Exponential sum growth exponents chapter (beta-chapter). 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 the blueprint lemma beta-asymp (Non-asymptotic definition of β).

Equations

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

Uniform approximation by fixed phases

From fixed bounds to asymptotic bounds

Uniform bounds for approximate model phases

theorem Expdb.approximate_model_phase_deriv_bounds {σ : ℝ} (hσ : 0 < σ) (P : ℕ) : ∃ (K : ℝ), 1 ≤ K ∧ ∀ {δ : ℝ} {F : ℝ → ℝ}, δ ≤ min (2 ^ (-σ) / 2) 1 → IsApproximateModelPhaseFunction F σ P δ → (∀ u ∈ phaseInterval, 2 ^ (-σ) / 2 ≤ iteratedDerivWithin 1 F phaseInterval u) ∧ ∀ (k : ℕ), 1 ≤ k → k ≤ P + 1 → ∀ u ∈ phaseInterval, ‖iteratedDerivWithin k F phaseInterval u‖ ≤ K

An approximate model phase with sufficiently small error has a uniform positive first derivative and uniform bounds on all derivatives through order P + 1, with constants depending only on σ and P.

theorem Expdb.isApproximateModelPhaseFunction_log (P : ℕ) : IsApproximateModelPhaseFunction Real.log 1 P 0

The logarithm is an exact approximate model phase at every finite order.

Building asymptotic counterexamples

Equivalence with the asymptotic definition

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

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