The trivial bound for a complete character sum

Proved

Weil.norm_sum_addChar_le_card

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

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

Let $F$ be a finite field, $\psi$ an additive character of $F$ valued in $\mathbb{C}$ and $g : F \to F$ any function. Then

\Big\lVert \sum_{x \in F} \psi(g(x)) \Big\rVert \le \#F.

Every term has modulus one, so the triangle inequality gives the number of terms. This is the benchmark that square-root cancellation improves on.

Preamble

import Mathlib.NumberTheory.GaussSum
import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
import Mathlib.NumberTheory.MulChar.Lemmas
import Mathlib.GroupTheory.SpecificGroups.Cyclic
import Mathlib.GroupTheory.Index
import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Analysis.RCLike.Basic
import Mathlib.Analysis.Complex.Basic
import Mathlib.Algebra.Field.GeomSum
import Mathlib.Algebra.Order.BigOperators.Group.Finset

set_option autoImplicit false
set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

universe u_1 u_2

open AddChar MulChar Finset

Formal statement

namespace Weil
theorem norm_sum_addChar_le_card : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] (ψ : AddChar F ℂ) (g : F → F), ‖∑ x : F, (ψ : F → ℂ) (g x)‖ ≤ (↑(Fintype.card F) : ℝ) := by sorry
end Weil

Source

Iwaniec & Kowalski, Analytic Number Theory, AMS Colloquium Publications 53, 2004, Ch. 11 (Sums over finite fields), §11.1-11.3

View graph