Gauss sum expansion of $e(b/q)$ over Dirichlet characters

Proved

Vino.sum_charInv_mul_gaussE

by tabbott · Sep 2, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theorycircle-methoddirichlet-charactersnumber-theory

Let $q\ge1$ and let $b$ be coprime to $q$ . Write

\tau(\chi)=\sum_{m<q}\chi(m)\,e\!\left(\frac{m}{q}\right)

for the Gauss sum of a Dirichlet character $\chi$ modulo $q$ . Then

\sum_{\chi \bmod q}\chi^{-1}(b)\,\tau(\chi)\;=\;\varphi(q)\,e\!\left(\frac{b}{q}\right),

the sum running over all $\varphi(q)$ Dirichlet characters modulo $q$ with values in $\mathbb C$ .

This is the exact dual of the definition of a Gauss sum: it expresses the additive character at a reduced fraction as a linear combination of multiplicative characters. It is the identity that converts the major-arc analysis of an exponential sum over primes into a question about $L$ -functions, since after substituting it the inner sum becomes a von Mangoldt sum twisted by a Dirichlet character.

Preamble

import Definitions.Def_Vino_dirichlet
import Mathlib.NumberTheory.DirichletCharacter.Orthogonality
open Finset

Formal statement

namespace Vino

theorem sum_charInv_mul_gaussE (q : ℕ) [NeZero q] {b : ℕ} (hb : IsUnit ((b : ℕ) : ZMod q)) :
    ∑ χ : DirichletCharacter ℂ q, χ⁻¹ ((b : ℕ) : ZMod q) * gaussE q χ
      = (Nat.totient q : ℂ) * CircleMethod.e ((b : ℝ) / (q : ℝ)) := by sorry

end Vino

Source

R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Chapter 3, Section 3.1 (major arcs for the three primes theorem, expansion of the von Mangoldt exponential sum in Dirichlet characters); H. Davenport, Multiplicative Number Theory, 3rd ed., Springer GTM 74, 2000, Chapter 26.

View graph

Gauss sum expansion of e(b/q)e(b/q)e(b/q) over Dirichlet characters

Gauss sum expansion of $e(b/q)$ over Dirichlet characters