The quadratic Gauss sum, from the Jacobi theta function

For every natural number N, Gauss's evaluation of the quadratic Gauss sum is

∑_{r = 0}^{N - 1} e^{2πi r² / N} = (1 + i) / 2 · (1 + (-i)^N) · √N,

that is √N, 0, i√N or (1 + i)√N according as N ≡ 1, 2, 3, 0 (mod 4) (for N = 0 both sides vanish). Mathlib's gaussSum_sq determines the square of a quadratic Gauss sum, so only its sign is new here, and the sign is genuinely archimedean: it depends on the choice of e^{2πi/N} among the primitive N-th roots of unity.

The proof compares two asymptotic expansions of the Jacobi theta function θ(τ) = ∑_n e^{πi n² τ} (Mathlib's jacobiTheta) as τ tends to the cusp 2/N, along the curve τ = -1 / (iY - N/2), Y → 0⁺. Splitting n into residue classes modulo N and applying the functional equation jacobiTheta₂_functional_equation to each class expresses θ(τ) through the Gauss sum; splitting n by parity and applying the functional equation to θ(-1/τ) = θ(iY - N/2) expresses it through θ(iY) and θ(4iY). The square roots of the two functional equations combine to the constant (1 + i)√N exactly, so the two expansions give an identity for every Y > 0. As Y → 0⁺ the theta arguments in this identity, i/Y, i/(4Y) and the transformed arguments 1/(2N) + i/(4Y) of the residue-class series, all tend to i∞, so their theta values tend to 1 (θ(τ) → 1 as im τ → ∞), and the identity becomes the evaluation. This is the classical theta-function route of Landsberg and Schaar.

Main results

• TauCeti.sum_range_cexp_two_pi_I_sq_div: Gauss's evaluation of the quadratic Gauss sum.
• TauCeti.sum_range_two_mul_cexp_two_pi_I_sq_div_four_mul: its half for a modulus 4M, the Gauss sum of the discriminant form of the rank-one lattice ⟨2M⟩.

References

• C. F. Gauss, Summatio quarumdam serierum singularium (1811).
• H. Rademacher, Topics in Analytic Number Theory, Chapter 9 (the Landsberg–Schaar relation).
• B. C. Berndt, R. J. Evans and K. S. Williams, Gauss and Jacobi Sums, Chapter 1.

theorem TauCeti.sum_range_cexp_two_pi_I_sq_div (N : ℕ) : ∑ r ∈ Finset.range N, Complex.exp (2 * ↑Real.pi * Complex.I * ↑r ^ 2 / ↑N) = (1 + Complex.I) / 2 * (1 + (-Complex.I) ^ N) * ↑√↑N

Gauss's evaluation of the quadratic Gauss sum: for every natural number N, ∑_{r < N} e^{2πi r²/N} = (1 + i)/2 · (1 + (-i)^N) · √N.

theorem TauCeti.sum_range_two_mul_cexp_two_pi_I_sq_div_four_mul (M : ℕ) : ∑ k ∈ Finset.range (2 * M), Complex.exp (2 * ↑Real.pi * Complex.I * (↑k ^ 2 / (4 * ↑M))) = (1 + Complex.I) * ↑√↑M

Half of Gauss's quadratic sum of modulus 4M: ∑_{k < 2M} e^{2πi k² / (4M)} = (1 + i) √M. The summand has period 2M, so this is half of the sum over the full range r < 4M.