Finite scale transfer for exponential sums

This module gives two ways to rewrite an exponential sum at a different length scale. Finite Fourier inversion dilates a sum from scale N to q * N, while decomposition into residue classes produces sums at scales approximately N / q. These identities are used to compare the exponential-sum growth exponent at different values of α.

Finite Fourier orthogonality

Reindexing exponential sums

theorem Expdb.exponentialSumAt_dilate (F : ℝ → ℝ) (T N : ℝ) (a b q : ℕ) [NeZero q] (hq : 0 < q) (hT : T ≠ 0) (hN : N ≠ 0) : exponentialSumAt F T N a b = (↑q)⁻¹ * ∑ h : ZMod q, exponentialSumAt (fun (u : ℝ) => F u + ↑h.val * N / T * u) T (↑q * N) (q * a) (q * b)

Finite Fourier inversion expresses a sum at scale N as an average of sums dilated by q.

theorem Expdb.norm_exponentialSumAt_dilate_le (F : ℝ → ℝ) (T N : ℝ) (a b q : ℕ) [NeZero q] (hq : 0 < q) (hT : T ≠ 0) (hN : N ≠ 0) : ‖exponentialSumAt F T N a b‖ ≤ ∑ h : ZMod q, ‖exponentialSumAt (fun (u : ℝ) => F u + ↑h.val * N / T * u) T (↑q * N) (q * a) (q * b)‖ / ↑q

Triangle-inequality form of exponentialSumAt_dilate.

noncomputable def Expdb.residueScale (N : ℝ) (q r : ℕ) : ℝ

The scale induced by restricting a sum to the residue class r mod q.

Equations

• Expdb.residueScale N q r = (N - ↑r) / ↑q

noncomputable def Expdb.residuePhase (F : ℝ → ℝ) (N : ℝ) (r : ℕ) : ℝ → ℝ

The affine phase induced by restricting a sum to the residue class r mod q.

Equations

• Expdb.residuePhase F N r u = F ((1 - ↑r / N) * u + ↑r / N)

theorem Expdb.residuePhase_identity (F : ℝ → ℝ) (N : ℝ) (q r m : ℕ) (hN : N ≠ 0) (hrN : ↑r < N) : residuePhase F N r (↑m / residueScale N q r) = F (↑(q * m + r) / N)

Evaluation of the residue-class phase at its rescaled integer arguments.

theorem Expdb.exponentialSumAt_residue (F : ℝ → ℝ) (T N : ℝ) (a b q r : ℕ) (hq : 0 < q) (hr : r < q) (hra : r ≤ a) (hab : a ≤ b) (hN : N ≠ 0) (hrN : ↑r < N) : ∑ n ∈ Finset.Icc a b with n % q = r, oscillatory F T N ↑n = exponentialSumAt (residuePhase F N r) T (residueScale N q r) ((a - r) ⌈/⌉ q) ((b - r) / q)

Reindex one residue class as an exponential sum with residuePhase and residueScale.

theorem Expdb.norm_exponentialSumAt_le_sum_residues (F : ℝ → ℝ) (T N : ℝ) (a b q : ℕ) (hq : 0 < q) (hqN : ↑q ≤ N) (hN : N ≠ 0) (ha : N ≤ ↑a) (hb : ↑b ≤ 2 * N) : ‖exponentialSumAt F T N a b‖ ≤ ∑ r ∈ Finset.range q, (‖exponentialSumAt (residuePhase F N r) T (residueScale N q r) ((a - r) ⌈/⌉ q) (min ((b - r) / q) ⌊2 * residueScale N q r⌋₊)‖ + 1)

Split an exponential sum into residue classes, trimming each upper endpoint at a cost of at most one term.