The Weil bound for a diagonal equation, sharp form (no character supplied)

Proved

Weil.abs_card_diagonal_sub_card_le_gcd

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 and $d, e \ge 1$ . Then

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

The characters of the required orders exist over $\mathbb{C}$ , so no character need be supplied. In the sharp form the relevant quantities are the numbers of $d$ -th and $e$ -th power classes, not $d$ and $e$ themselves; in particular the count is exactly $\#F$ whenever $\gcd(\#F-1,d) = 1$ or $\gcd(\#F-1,e) = 1$ .

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_gcd : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {d e : ℕ}, d ≠ 0 → e ≠ 0 → |(↑(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