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

Prime Kloosterman sums and normalization

Additive-character conventions and elementary identities for the classical prime sums. References: Weil (1948); Harcos (2015), equation (1).

noncomputable def KloostermanWeil.kloostermanSumPrime (p : ℕ) [Fact (Nat.Prime p)] (a b : ZMod p) : ℂ

The prime-modulus sum of the additive phase b*x + a/x over nonzero residues.

Equations

• KloostermanWeil.kloostermanSumPrime p a b = ∑ x : ZMod p, if x = 0 then 0 else ZMod.stdAddChar (b * x + a * x⁻¹)

noncomputable def KloostermanWeil.zmodInvEquiv (p : ℕ) [Fact (Nat.Prime p)] : ZMod p ≃ ZMod p

Inversion as an involutive permutation of a prime residue field, including zero.

Equations

• KloostermanWeil.zmodInvEquiv p = { toFun := Inv.inv, invFun := Inv.inv, left_inv := ⋯, right_inv := ⋯ }

theorem KloostermanWeil.kloostermanSumPrime_zero_left (p : ℕ) [Fact (Nat.Prime p)] (b : ZMod p) (hb : b ≠ 0) : kloostermanSumPrime p 0 b = -1

theorem KloostermanWeil.kloostermanSumPrime_comm (p : ℕ) [Fact (Nat.Prime p)] (a b : ZMod p) : kloostermanSumPrime p a b = kloostermanSumPrime p b a

theorem KloostermanWeil.kloostermanSumPrime_zero_right (p : ℕ) [Fact (Nat.Prime p)] (a : ZMod p) (ha : a ≠ 0) : kloostermanSumPrime p a 0 = -1

theorem KloostermanWeil.kloostermanSumPrime_zero_zero (p : ℕ) [Fact (Nat.Prime p)] : kloostermanSumPrime p 0 0 = ↑p - 1

def KloostermanWeil.PrimeNondegenerateWeil : Prop

The prime Kloosterman bound with both coefficients nonzero, proved by prime_bound.

Equations

• KloostermanWeil.PrimeNondegenerateWeil = ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (a b : ZMod p), a ≠ 0 → b ≠ 0 → ‖KloostermanWeil.kloostermanSumPrime p a b‖ ≤ 2 * √↑p

noncomputable def KloostermanWeil.weilKloostermanPrime (p : ℕ) [Fact (Nat.Prime p)] (m n : ZMod p) : ℂ

Classical prime Kloosterman sum in conventional coefficient order: S(m,n;p) = ∑_{x mod p, x ≠ 0} e_p(m x + n x⁻¹). This matches Weil (1948), up to the standard additive-character notation.

Equations

• KloostermanWeil.weilKloostermanPrime p m n = ∑ x : ZMod p, if x = 0 then 0 else ZMod.stdAddChar (m * x + n * x⁻¹)

theorem KloostermanWeil.kloostermanSumPrime_eq_weilKloostermanPrime (p : ℕ) [Fact (Nat.Prime p)] (a b : ZMod p) : kloostermanSumPrime p a b = weilKloostermanPrime p b a

Exact normalization bridge: the prime sum agrees with the classical Kloosterman sum with the two coefficients named in the opposite order.

def KloostermanWeil.Weil1948PrimeKloostermanBound : Prop

Classical prime Kloosterman–Weil bound in conventional coefficient order. This proposition is proved in LeanPool.KloostermanWeil.Weil.PrimeKloosterman using a Carlitz recurrence and a Stepanov point-count estimate.

Source: André Weil, "On Some Exponential Sums", Proc. Natl. Acad. Sci. U.S.A. 34 (1948), 204-207, DOI 10.1073/pnas.34.5.204.

Equations

• KloostermanWeil.Weil1948PrimeKloostermanBound = ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (m n : ZMod p), m ≠ 0 → n ≠ 0 → ‖KloostermanWeil.weilKloostermanPrime p m n‖ ≤ 2 * √↑p

theorem KloostermanWeil.primeNondegenerateWeil_iff_weil1948 : PrimeNondegenerateWeil ↔ Weil1948PrimeKloostermanBound

The nondegenerate formulation and the classical Weil statement are exactly equivalent; there is no remaining normalization or convention gap.

theorem KloostermanWeil.weilKloostermanPrime_scaling (p : ℕ) [Fact (Nat.Prime p)] (m n : ZMod p) (hm : m ≠ 0) : weilKloostermanPrime p m n = weilKloostermanPrime p 1 (m * n)

Elementary nonzero scaling reduction: for nonzero m,n mod p, K_p(n,m) = K_p(mn,1), equivalently in the source-normalized order S(m,n;p) = S(1,mn;p).

theorem KloostermanWeil.kloostermanSumPrime_scaling (p : ℕ) [Fact (Nat.Prime p)] (a b : ZMod p) (hb : b ≠ 0) : kloostermanSumPrime p a b = kloostermanSumPrime p (b * a) 1

def KloostermanWeil.OneParameterPrimeWeil : Prop

The prime Kloosterman bound after normalizing the linear coefficient to one.

Equations

• KloostermanWeil.OneParameterPrimeWeil = ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (a : ZMod p), a ≠ 0 → ‖KloostermanWeil.kloostermanSumPrime p a 1‖ ≤ 2 * √↑p

theorem KloostermanWeil.primeNondegenerateWeil_iff_oneParameter : PrimeNondegenerateWeil ↔ OneParameterPrimeWeil