Fourier completion for primitive quadratic character sums

This file records the finite Fourier identity underlying the quadratic Pólya--Vinogradov estimate. In particular, the Gauss factor is paid from the proved primitive root-number norm, rather than postulated as an extra bound.

theorem DirichletCharacter.IsPrimitive.norm_gaussSum_stdAddChar {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (hχ : χ.IsPrimitive) (_hq : 1 < q) : ‖gaussSum χ ZMod.stdAddChar‖ = √↑q

The Gauss sum of a primitive character modulo q has norm sqrt q. This is extracted from the already proved unit norm of the root number.

theorem DirichletCharacter.IsPrimitive.sum_range_fourier_completion {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (hχ : χ.IsPrimitive) (M : ℕ) : ∑ n ∈ Finset.range M, χ ↑n = (↑q)⁻¹ * gaussSum χ ZMod.stdAddChar * ∑ j : ZMod q, χ⁻¹ (-j) * ∑ n ∈ Finset.range M, ZMod.stdAddChar (j * ↑n)

Exact finite Fourier completion of a primitive character prefix. The zero frequency vanishes automatically through χ⁻¹ 0 = 0; retaining it makes the identity canonical and avoids a choice of integer representatives.

theorem DirichletCharacter.IsPrimitive.norm_sum_range_le_sqrt_mul_fourierKernelL1 {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (hχ : χ.IsPrimitive) (hq : 1 < q) (M : ℕ) : ‖∑ n ∈ Finset.range M, χ ↑n‖ ≤ √↑q / ↑q * ∑ j : ZMod q, ‖∑ n ∈ Finset.range M, ZMod.stdAddChar (j * ↑n)‖

Norm form of Fourier completion. This isolates the sole remaining Pólya--Vinogradov input as the L¹ norm of the finite geometric kernels; the Gauss sum has already been replaced by sqrt q.