Finite Field Character Sum Weil Bound 3-AP Discrepancy Control (Exact Normalized)

Proved

weil_bound_ap3_character_density_fixed

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

combinatoricserdos-problemsnumber-theory

For any 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 error density satisfies $E / p^2 \le 2\sqrt{p}/p = 2/\sqrt{p}$ .

Formal statement

import Mathlib

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

View graph