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 public prime estimate #
Exports Weil’s classical bound and the equivalent coefficient ordering used in Harcos (2015), Theorem 1.
Prime nondegenerate Kloosterman–Weil bound via the Stepanov–Carlitz development.
Conventional Weil (1948) coefficient order and normalization.