Trivial bound for the Gauss sum

Proved

Vino.norm_gaussE_le

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

analytic-number-theorycircle-methoddirichlet-charactersnumber-theory

For every Dirichlet character $\chi$ modulo $q$ ,

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

This is the trivial bound. For a primitive character the truth is $|\tau(\chi)|=\sqrt q$ , a square-root saving; the trivial bound is nevertheless what one uses for the imprimitive and principal characters, where no such saving is available.

Preamble

import Definitions.Def_Vino_dirichlet
import Definitions.Def_Vino_primes
import Mathlib.NumberTheory.DirichletCharacter.Bounds
open Finset

Formal statement

namespace Vino

theorem norm_gaussE_le (q : ℕ) (χ : DirichletCharacter ℂ q) : ‖gaussE q χ‖ ≤ (q : ℝ) := by sorry

end Vino

Source

H. Davenport, Multiplicative Number Theory, 3rd ed., Springer GTM 74, 2000, Chapters 9 and 26; R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Chapter 3, Section 3.1.

View graph