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

From point counts to spectral sums

Connects extension Kloosterman sums and the point-count discrepancy in Harcos (2015), equation (3).

theorem KloostermanWeil.Stepanov.Kseq_eq_Kext_of_ne_zero (p n : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (hn : n ≠ 0) : Carlitz.Kseq p t n = Carlitz.Kext p n t

theorem KloostermanWeil.Stepanov.scalarTraceSum_zero (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] (c : GaloisField p n) : extensionKloostermanScalarSum p n c 0 = ↑(p ^ n - 1)

theorem KloostermanWeil.Stepanov.errorAggregate_eq_Kext_sum (p n : ℕ) [Fact (Nat.Prime p)] (c : ZMod p) (hn : n ≠ 0) : errorAggregate p n c = -1 + ∑ m : { m : ZMod p // m ≠ 0 }, Carlitz.Kext p n (↑m ^ 2 * c)

theorem KloostermanWeil.Stepanov.pointCountError_eq_errorAggregate (p n : ℕ) [Fact (Nat.Prime p)] (hpodd : Odd p) (c : ZMod p) (hc : c ≠ 0) (hn : n ≠ 0) : ↑(hyperellipticAffinePointFinset (kloostermanCurvePolynomial p n c)).card - ↑(p ^ n) = errorAggregate p n c

Exact point-count bridge: the specialized affine curve defect is literally the finite aggregate consumed in the Stepanov argument.