Trivial bounds for exponential sum growth exponents

This module formalizes the trivial bounds on β in the blueprint's Exponential sum growth exponents chapter (beta-chapter).

For α > 1, a uniform Euler–Maclaurin estimate compares the exponential sum of an arbitrary approximate model phase with its oscillatory integral. The derivative bounds for model phases then give the upper bound β(α) ≤ α - 1. For the reverse inequality, it suffices to use the logarithmic model phase, since an admissible exponent must bound every model phase. Its sum is essentially ∑ n ^ (iT) and its integral has size comparable to N / T, while Euler–Maclaurin contributes only a bounded error, giving β(α) ≥ α - 1.

For 0 ≤ α ≤ 1, the triangle inequality gives β(α) ≤ α. The L^2 integral estimate lemma is applied to the separated values log(n/N) to find a parameter for which the logarithmic-phase sum has size comparable to N ^ (1 / 2), yielding the lower bound β(α) ≥ α / 2.

Choosing the Euler–Maclaurin order

The upper bound for α > 1

The matching logarithmic lower bound for α > 1

theorem Expdb.exists_norm_logPhase_sum_sub_mainTerm_le (s : ℕ) : ∃ (K : ℝ) (C : ℝ), 1 ≤ K ∧ 1 ≤ C ∧ ∀ {N T : ℝ} {a b : ℕ}, a < b → 1 ≤ N → 1 ≤ T → ↑a = N → ↑b = 2 * N → HasSmallEulerMaclaurinRemainder s T N K → ‖exponentialSumAt Real.log T N a b - logPhaseMainTerm N T‖ ≤ C

For each Euler–Maclaurin order, the logarithmic exponential sum differs from its explicit main term by a uniformly bounded amount once the scale conditions hold. This is the formal counterpart of the blueprint's estimate for ∑ n ^ (iT), with the factor 2π absorbed into Lean's Fourier character.

The L² lower bound for 0 < α ≤ 1

Trivial bounds

theorem Expdb.exponentSumGrowthExponent_nonneg (α : NNReal) : 0 ≤ exponentSumGrowthExponent α

The exponential-sum growth exponent is nonnegative.

theorem Expdb.exponentSumGrowthExponent_le_self (α : NNReal) : exponentSumGrowthExponent α ≤ ↑α

The triangle inequality bounds the growth exponent by the scale exponent.

theorem Expdb.exponentSumGrowthExponent_eq_sub_one {α : NNReal} (hα : 1 < α) : exponentSumGrowthExponent α = ↑α - 1

For α > 1, the exponential sum growth exponent is α - 1.

theorem Expdb.exponentSumGrowthExponent_mem_Icc {α : NNReal} (hα : α ≤ 1) : exponentSumGrowthExponent α ∈ Set.Icc (↑α / 2) ↑α

For 0 ≤ α ≤ 1, the exponential sum growth exponent lies in the interval [α / 2, α].

@[simp]

theorem Expdb.exponentSumGrowthExponent_zero : exponentSumGrowthExponent 0 = 0

The exponential sum growth exponent vanishes at scale zero.