Splitting off the degenerate Jacobi sums

Proved

Weil.sum_jacobiSum_split

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

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

Let $F$ be a finite field, $d, e \in \mathbb{N}$ , and let $\chi$ and $\lambda$ have orders exactly $m = \gcd(\#F^\times, d)$ and $n = \gcd(\#F^\times, e)$ . Then

\sum_{i<m}\sum_{j<n} J(\chi^i,\lambda^j) = \#F - m - n + \sum_{i=1}^{m-1}\sum_{j=1}^{n-1} J(\chi^i,\lambda^j).

The terms with $i = 0$ or $j = 0$ are degenerate: $J(1,1) = \#F - 2$ , and $J(1,\lambda^j) = J(\chi^i,1) = -1$ whenever the other character is nontrivial. Summing them contributes $\#F - m - n$ .

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_jacobiSum_split : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {d e : ℕ} {χ lam : MulChar F ℂ}, orderOf χ = Nat.gcd (Fintype.card Fˣ) d → orderOf lam = Nat.gcd (Fintype.card Fˣ) e → ∑ i ∈ Finset.range (Nat.gcd (Fintype.card Fˣ) d), ∑ j ∈ Finset.range (Nat.gcd (Fintype.card Fˣ) e), jacobiSum (χ ^ i) (lam ^ j) = (↑(Fintype.card F) : ℂ) - (↑(Nat.gcd (Fintype.card Fˣ) d) : ℂ) - (↑(Nat.gcd (Fintype.card Fˣ) e) : ℂ) + ∑ i ∈ Finset.Ico 1 (Nat.gcd (Fintype.card Fˣ) d), ∑ j ∈ Finset.Ico 1 (Nat.gcd (Fintype.card Fˣ) e), 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