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

Conjugacy-class ghost sums

Conjugate polynomial classes and ghost sums used in the Carlitz recurrence. The extension-sum method is from Carlitz (1969); the class decomposition is formalized here.

theorem KloostermanWeil.Carlitz.conjCarrier_card_eq_minpoly_natDegree (p n : ℕ) [Fact (Nat.Prime p)] (c : ConjRootClass (Fp p) (Ext p n)) [Fintype ↑c.carrier] : Fintype.card ↑c.carrier = c.minpoly.natDegree

theorem KloostermanWeil.Carlitz.minpoly_eq_class_minpoly (p n : ℕ) [Fact (Nat.Prime p)] {c : ConjRootClass (Fp p) (Ext p n)} (y : ↑c.carrier) : minpoly (Fp p) ↑y = c.minpoly

theorem KloostermanWeil.Carlitz.relative_finrank_eq_total_div_classDegree (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] {c : ConjRootClass (Fp p) (Ext p n)} (y : ↑c.carrier) : Module.finrank (↥(Fp p)⟮↑y⟯) (Ext p n) = n / c.minpoly.natDegree

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

The conjugacy-class expansion of the extension sum, weighted by class cardinality.

Equations

• One or more equations did not get rendered due to their size.

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