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

Finite spectral aggregates

Defines the finite sums linking spectral power sums and curve-point data. Reference: Harcos (2015), equation (3).

noncomputable def KloostermanWeil.Stepanov.errorAggregate (p n : ℕ) [Fact (Nat.Prime p)] (c : ZMod p) : ℂ

Finite aggregate appearing in the Stepanov point-count argument. For the specialized curve, this is identified with #C_n - p^n exactly, with no asymptotic notation.

Equations

• KloostermanWeil.Stepanov.errorAggregate p n c = -1 + ∑ m : { m : ZMod p // m ≠ 0 }, KloostermanWeil.Carlitz.Kseq p (↑m ^ 2 * c) n