Finite Field Character Sum Weil Bound 3-AP Discrepancy Control

Proved

weil_bound_ap3_character_density

by Xinyu Xu · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problemsnumber-theory

For a multiplicative character $\chi$ on $\mathbb{F}_p^\times$ with Weil bound $|\sum_{x \in \mathbb{F}_p} \chi(x(x+1))| \le 2\sqrt{p}$ , the 3-AP discrepancy term $E$ satisfies $E / p^2 \le 2 / p^{3/2}$ , decaying strictly faster than the principal density term.

Formal statement

import Mathlib

theorem weil_bound_ap3_character_density (p : ℕ) (hp : 100 ≤ p) (E : ℝ) (hE_nonneg : 0 ≤ E)
    (hE_weil : E ≤ 2 * Real.sqrt (p : ℝ) * (p : ℝ)) :
    E / ((p : ℝ) ^ 2) ≤ 2 / Real.sqrt (p : ℝ) := by sorry

View graph