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

Extension-field sums and trace scaling

Connects Carlitz’s extension sums (1969) to the trace formulation used in Harcos (2015), §3.

noncomputable def KloostermanWeil.Stepanov.extensionKloostermanAB (p n : ℕ) [Fact (Nat.Prime p)] (A B : GaloisField p n) : ℂ

The two-coefficient Kloosterman sum over units of the chosen finite extension.

Equations

• KloostermanWeil.Stepanov.extensionKloostermanAB p n A B = ∑ u : (GaloisField p n)ˣ, (KloostermanWeil.Carlitz.psiExt p n) (A * ↑u + B * (↑u)⁻¹)

theorem KloostermanWeil.Stepanov.scalarTraceSum_eq_extensionKloostermanAB (p n : ℕ) [Fact (Nat.Prime p)] (c : GaloisField p n) (m : ZMod p) : extensionKloostermanScalarSum p n c m = extensionKloostermanAB p n ((algebraMap (ZMod p) (GaloisField p n)) m) ((algebraMap (ZMod p) (GaloisField p n)) m * c)

theorem KloostermanWeil.Stepanov.Kext_eq_extensionKloostermanAB_one (p n : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) : Carlitz.Kext p n t = extensionKloostermanAB p n 1 ((algebraMap (ZMod p) (GaloisField p n)) t)

theorem KloostermanWeil.Stepanov.scale_arg {F : Type u_1} [Field F] (M C U : F) (hM : M ≠ 0) : M * U + M * C * U⁻¹ = M * U + M ^ 2 * C * (M * U)⁻¹

noncomputable def KloostermanWeil.Stepanov.extensionKloostermanAB0 (p n : ℕ) [Fact (Nat.Prime p)] (A B : GaloisField p n) : ℂ

The extension Kloosterman sum written over the whole field with zero omitted.

Equations

• KloostermanWeil.Stepanov.extensionKloostermanAB0 p n A B = ∑ x : GaloisField p n, if x = 0 then 0 else (KloostermanWeil.Carlitz.psiExt p n) (A * x + B * x⁻¹)

theorem KloostermanWeil.Stepanov.extensionKloostermanAB_eq_AB0 (p n : ℕ) [Fact (Nat.Prime p)] (A B : GaloisField p n) : extensionKloostermanAB p n A B = extensionKloostermanAB0 p n A B

theorem KloostermanWeil.Stepanov.Kext_eq_AB0_one (p n : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) : Carlitz.Kext p n t = extensionKloostermanAB0 p n 1 ((algebraMap (ZMod p) (GaloisField p n)) t)

theorem KloostermanWeil.Stepanov.extensionKloostermanAB0_scaling (p n : ℕ) [Fact (Nat.Prime p)] (c m : ZMod p) (hm : m ≠ 0) : extensionKloostermanAB0 p n ((algebraMap (ZMod p) (GaloisField p n)) m) ((algebraMap (ZMod p) (GaloisField p n)) m * (algebraMap (ZMod p) (GaloisField p n)) c) = extensionKloostermanAB0 p n 1 ((algebraMap (ZMod p) (GaloisField p n)) (m ^ 2 * c))

theorem KloostermanWeil.Stepanov.extensionKloostermanAB_scaling (p n : ℕ) [Fact (Nat.Prime p)] (c m : ZMod p) (hm : m ≠ 0) : extensionKloostermanAB p n ((algebraMap (ZMod p) (GaloisField p n)) m) ((algebraMap (ZMod p) (GaloisField p n)) m * (algebraMap (ZMod p) (GaloisField p n)) c) = Carlitz.Kext p n (m ^ 2 * c)

theorem KloostermanWeil.Stepanov.scalarTraceSum_eq_Kext_sq (p n : ℕ) [Fact (Nat.Prime p)] (c m : ZMod p) (hm : m ≠ 0) : extensionKloostermanScalarSum p n ((algebraMap (ZMod p) (GaloisField p n)) c) m = Carlitz.Kext p n (m ^ 2 * c)