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

Irreducible-class ghost sums

Expresses the extension sum using irreducible polynomial classes, in the Carlitz (1969) recurrence framework.

noncomputable def KloostermanWeil.Carlitz.irredGhost (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] (t : Fp p) : ℂ

The extension-sum ghost component indexed by relevant irreducible polynomials.

Equations

• KloostermanWeil.Carlitz.irredGhost p n t = ∑ P : KloostermanWeil.Carlitz.RelevantIrred p n, ↑(↑P).natDegree * KloostermanWeil.Dickson.etaPoly p t ↑P ^ (n / (↑P).natDegree)

theorem KloostermanWeil.Carlitz.minpoly_zero_class_eq_X (p n : ℕ) [Fact (Nat.Prime p)] : ConjRootClass.minpoly 0 = Polynomial.X

theorem KloostermanWeil.Carlitz.classGhost_eq_irredGhost (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] (t : Fp p) : classGhost p n t = irredGhost p n t

theorem KloostermanWeil.Carlitz.Kext_eq_irredGhost (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] (t : Fp p) : Kext p n t = irredGhost p n t