Prove2Me

Lemma 20 — Multiplicative Subgroup Fourier Confinement Positivity

Proved
weil_fourier_exact_pos_v5

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

combinatoricserdos-problemsnumber-theory

For any character subgroup H≤Fp×H \le \mathbb{F}_p^\times with density ∣H∣2>2p3/2|H|^2 > 2p^{3/2}, the 3-AP Fourier count strictly dominates Weil dispersion.

Formal statement
import Mathlib

theorem weil_fourier_exact_pos_v5 (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