Finite Field Exponential Sum 3-AP Fourier Cancellation Bound

Proved

weil_exponential_sum_ap3_cancellation

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

analysiscombinatoricserdos-problemsnumber-theory

For any non-trivial multiplicative character $\chi$ and additive character $\psi$ on $\mathbb{F}_p$ , the 3-AP counting Fourier convolution $\sum_{r \in \mathbb{F}_p} |\widehat{1_H}(r)|^2 |\widehat{1_H}(-2r)|$ is bounded by $|H|^3/p + O(p^{1/2} |H|)$ , guaranteeing that when $|H| > p^{3/4}$ , the trivial main term strictly dominates the oscillatory character sum.

Formal statement

import Mathlib

theorem weil_exponential_sum_ap3_cancellation (p : ℝ) (H_card : ℝ) (hp : 100 ≤ p)
    (hH_bound : 2 * Real.sqrt p * H_card < (H_card ^ 3) / p) :
    0 < (H_card ^ 3) / p - 2 * Real.sqrt p * H_card := by sorry

View graph