Adapted from Charlie Dorsey’s Apache-2.0 Weil Bounds Toolkit for Lean Pool’s module system, Mathlib version, quality requirements and compilation performance.

The prime Kloosterman bound

Combines the spectral and point-count arguments to prove Weil’s bound (1948), following Harcos (2015), Theorem 1, for odd primes. The case p=2 is proved separately.

theorem KloostermanWeil.Stepanov.carlitzAlpha_norm_eq_sqrt_prime (p : ℕ) [Fact (Nat.Prime p)] (hpodd : Odd p) (c : ZMod p) (hc : c ≠ 0) (m : { m : ZMod p // m ≠ 0 }) : ‖carlitzAlpha p (↑m ^ 2 * c)‖ = √↑p

theorem KloostermanWeil.Stepanov.carlitzBeta_norm_eq_sqrt_prime (p : ℕ) [Fact (Nat.Prime p)] (hpodd : Odd p) (c : ZMod p) (hc : c ≠ 0) (m : { m : ZMod p // m ≠ 0 }) : ‖carlitzBeta p (↑m ^ 2 * c)‖ = √↑p

theorem KloostermanWeil.Stepanov.oneParameterPrimeWeil_odd (p : ℕ) [Fact (Nat.Prime p)] (hpodd : Odd p) (a : ZMod p) (ha : a ≠ 0) : ‖kloostermanSumPrime p a 1‖ ≤ 2 * √↑p

theorem KloostermanWeil.Stepanov.oneParameterPrimeWeil_two (a : ZMod 2) : ‖kloostermanSumPrime 2 a 1‖ ≤ 2 * √2

theorem KloostermanWeil.Stepanov.oneParameterPrimeWeil_proved : OneParameterPrimeWeil

One-parameter prime Kloosterman–Weil bound, including characteristic two.