Uniform bound on a Jacobi sum of nontrivial characters

Proved

Weil.norm_jacobiSum_le

by tabbott · Sep 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

Let $F$ be a finite field and let $\chi$ and $\varphi$ be nontrivial multiplicative characters of $F$ valued in $\mathbb{C}$ . Then

\lVert J(\chi,\varphi)\rVert \le \sqrt{\#F},

with no hypothesis on $\chi\varphi$ . When $\chi\varphi$ is nontrivial the modulus is exactly $\sqrt{\#F}$ ; when $\chi\varphi = 1$ the Jacobi sum is $-\chi(-1)$ , of modulus one, which is still at most $\sqrt{\#F}$ .

Preamble

import Mathlib.NumberTheory.GaussSum
import Mathlib.NumberTheory.JacobiSum.Basic
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_jacobiSum_le : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [DecidableEq F] {χ φ : MulChar F ℂ}, χ ≠ 1 → φ ≠ 1 → ‖jacobiSum χ φ‖ ≤ √(↑(Fintype.card F) : ℝ) := by sorry
end Weil

Source

Ireland & Rosen, A Classical Introduction to Modern Number Theory, 2nd ed., Springer GTM 84, Ch. 8 (Gauss and Jacobi Sums), Sections 8.3 and 8.5

View graph