The Weil bound for a diagonal equation, sharp form

Proved

Weil.abs_card_diagonal_sub_card_le

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

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

Weil bound for $x^d + y^e = 1$ . Let $F$ be a finite field, $d, e \ge 1$ , and let $\chi$ and $\lambda$ be multiplicative characters of $F$ of orders exactly $m = \gcd(\#F^\times, d)$ and $n = \gcd(\#F^\times, e)$ . Then

\bigl|\#\{(x,y) \in F^2 : x^d + y^e = 1\} - \#F\bigr| \le (m-1)(n-1)\sqrt{\#F}.

This is the Riemann hypothesis for the diagonal curve $x^d + y^e = 1$ , in the one case where it is reachable without any theory of curves: the deviation from the main term $\#F$ is a sum of $(m-1)(n-1)$ Jacobi sums, each of modulus 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 abs_card_diagonal_sub_card_le : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {d e : ℕ} {χ lam : MulChar F ℂ}, d ≠ 0 → e ≠ 0 → orderOf χ = Nat.gcd (Fintype.card Fˣ) d → orderOf lam = Nat.gcd (Fintype.card Fˣ) e → |(↑(Finset.card {z : F × F | Prod.fst z ^ d + Prod.snd z ^ e = 1}) : ℝ) - (↑(Fintype.card F) : ℝ)| ≤ ((↑(Nat.gcd (Fintype.card Fˣ) d) : ℝ) - 1) * ((↑(Nat.gcd (Fintype.card Fˣ) e) : ℝ) - 1) * √(↑(Fintype.card F) : ℝ) := by sorry
end Weil

Source

A. Weil, Numbers of solutions of equations in finite fields, Bull. Amer. Math. Soc. 55 (1949), 497-508 (diagonal equations are the worked example of the Weil conjectures)

View graph