A product of two character sums integrates to a double Jacobi sum

Proved

Weil.sum_prod_char_eq_jacobiSum

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

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

Let $F$ be a finite field, $\chi$ and $\lambda$ multiplicative characters of $F$ valued in $\mathbb{C}$ , and $m, n \in \mathbb{N}$ . Then

\sum_{u \in F}\Bigl(\sum_{i<m}\chi^i(u)\Bigr)\Bigl(\sum_{j<n}\lambda^j(1-u)\Bigr) = \sum_{i<m}\sum_{j<n} J(\chi^i, \lambda^j).

Expanding the product and exchanging the order of summation turns the convolution into $mn$ Jacobi sums.

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 sum_prod_char_eq_jacobiSum : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] {χ lam : MulChar F ℂ} (m n : ℕ), ∑ u : F, (∑ i ∈ Finset.range m, (χ ^ i) u) * (∑ j ∈ Finset.range n, (lam ^ j) (1 - u)) = ∑ i ∈ Finset.range m, ∑ j ∈ Finset.range n, jacobiSum (χ ^ i) (lam ^ j) := 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