The Weil bound for a diagonal equation, classical form

Proved

Weil.abs_card_diagonal_sub_card_le_deg

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$ , $(d-1)(e-1)\sqrt q$ form. 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 (d-1)(e-1)\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_deg : ∀ {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) : ℝ)| ≤ ((↑d : ℝ) - 1) * ((↑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