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

Newton sums for the recurrence

Newton identities connecting polynomial coefficients and power sums. The algebra is standard; its indexing here serves the Carlitz (1969) construction.

noncomputable def KloostermanWeil.Carlitz.primePowerWeight (p n : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (z : PrimePowerDecomp p n) : ℂ

The degree-weighted character contribution of an irreducible prime power.

Equations

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

noncomputable def KloostermanWeil.Carlitz.pointedWeight (p n : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (z : PointedFactorData p n) : ℂ

The factor weight multiplied by the degree of the marked irreducible.

Equations

• KloostermanWeil.Carlitz.pointedWeight p n t z = ↑(↑z.snd.fst).natDegree * KloostermanWeil.Carlitz.factorWeight p t z.fst

theorem KloostermanWeil.Carlitz.pointedWeight_primePowerToPointed (p n : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (z : PrimePowerDecomp p n) : pointedWeight p n t (primePowerToPointed p n z) = primePowerWeight p n t z

theorem KloostermanWeil.Carlitz.sum_count_natDegree {p : ℕ} (s : Multiset (Polynomial (ZMod p))) : ∑ q ∈ s.toFinset, Multiset.count q s * q.natDegree = (Multiset.map Polynomial.natDegree s).sum

theorem KloostermanWeil.Carlitz.pointedFiber_sum (p n : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (s : FactorData p n) : ∑ z : (q : ↥(↑s).toFinset) × Fin (Multiset.count ↑q ↑s), ↑(↑z.fst).natDegree * factorWeight p t s = ↑n * factorWeight p t s

theorem KloostermanWeil.Carlitz.sum_primePowerWeight_eq_sum_pointedWeight (p n : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) : ∑ z : PrimePowerDecomp p n, primePowerWeight p n t z = ∑ z : PointedFactorData p n, pointedWeight p n t z

theorem KloostermanWeil.Carlitz.sum_pointedWeight_eq_n_mul_A (p n : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) : ∑ z : PointedFactorData p n, pointedWeight p n t z = ↑n * Dickson.A p t n

theorem KloostermanWeil.Carlitz.sum_primePowerWeight_eq_ghost_convolution (p n : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) : ∑ z : PrimePowerDecomp p n, primePowerWeight p n t z = ∑ j : Fin n, irredGhost p (↑j + 1) t * Dickson.A p t (n - (↑j + 1))

theorem KloostermanWeil.Carlitz.newton_irredGhost (p n : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) : ↑n * Dickson.A p t n = ∑ j : Fin n, irredGhost p (↑j + 1) t * Dickson.A p t (n - (↑j + 1))

theorem KloostermanWeil.Carlitz.newton_Kext (p n : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) : ↑n * Dickson.A p t n = ∑ j : Fin n, Kext p (↑j + 1) t * Dickson.A p t (n - (↑j + 1))