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

structure Expdb.IsModelPhaseSumSetupAt (α σ δ : ℝ) (P : ℕ) (C T N : ℝ) (F : ℝ → ℝ) (a b : ℕ) : Prop

The fixed data satisfying the hypotheses of the non-asymptotic exponential-sum bound.

• threshold_le_param : C ≤ T

  The phase parameter is above the uniform threshold.

• rpow_sub_le_scale : T ^ (α - δ) ≤ N

  The scale is at least the lower power allowed by δ.

• scale_le_rpow_add : N ≤ T ^ (α + δ)

  The scale is at most the upper power allowed by δ.

• isApproximateModelPhase : IsApproximateModelPhaseFunction F σ P δ

  The phase approximates the model phase through order P.

• scale_le_start : N ≤ ↑a

  The summation interval begins in the dyadic block.

• end_le_two_mul_scale : ↑b ≤ 2 * N

  The summation interval ends in the dyadic block.

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.

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 δ → HasPhaseFirstDerivLowerBound F (2 ^ (-σ) / 2) ∧ HasPhaseDerivBound F (P + 1) 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.