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` #

source

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 → K * T / N ≤ 1 → N * (K * T / N) ^ (s + 1) ≤ 1 → ‖∑ n ∈ Finset.Icc a b, ↑(Real.fourierChar (T * Real.log (↑n / N))) - 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.