Finite Field Character Weil Dispersion Relative Ratio Decay

Proved

weil_dispersion_ratio_decay_1788790553

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

analysiscombinatoricserdos-problemsnumber-theory

For prime $p$ and character subgroup $|H| > p^{3/4}$ , the relative fluctuation $(2\sqrt{p}|H|) / (|H|^3/p) = 2p^{3/2}/|H|^2$ strictly decays to zero as $|H|$ grows.

Formal statement

import Mathlib

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

View graph