Lemma 20 — Multiplicative Subgroup Fourier Confinement Positivity

Proved

weil_bound_fourier_positivity_v4

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

combinatoricserdos-problemsnumber-theory

For any character subgroup $H \le \mathbb{F}_p^\times$ satisfying density condition $|H|^2 > 2p^{3/2}$ , the difference between the principal AP3 count $|H|^3/p$ and the Weil dispersion $2\sqrt{p}|H|$ is strictly positive.

Formal statement

import Mathlib

theorem weil_bound_fourier_positivity_v4 (p : ℝ) (H : ℝ) (hp : 0 < p) (hH : 0 < H)
    (h_dense : 2 * Real.sqrt p * p < H ^ 2) :
    0 < (H ^ 3) / p - 2 * Real.sqrt p * H := by sorry

View graph