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

Multiplicative polynomial weights

Relates multiplicative polynomial weights to factorization data in the Carlitz (1969) extension-sum construction.

theorem KloostermanWeil.Carlitz.etaPoly_multiset_prod_of_monic (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (s : Multiset (Polynomial (ZMod p))) (hs : ∀ f ∈ s, f.Monic) : Dickson.etaPoly p t s.prod = (Multiset.map (Dickson.etaPoly p t) s).prod

noncomputable def KloostermanWeil.Carlitz.factorWeight (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) {n : ℕ} (s : FactorData p n) : ℂ

The product of the additive-character weights of the irreducible factors.

Equations

• KloostermanWeil.Carlitz.factorWeight p t s = (Multiset.map (KloostermanWeil.Dickson.etaPoly p t) ↑s).prod

theorem KloostermanWeil.Carlitz.etaPoly_eq_factorWeight (p n : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (f : MonicDeg p n) : Dickson.etaPoly p t ↑f = factorWeight p t (factorDataOf p n f)

noncomputable def KloostermanWeil.Carlitz.coeffFactorEquiv (p n : ℕ) [Fact (Nat.Prime p)] : (Fin n → ZMod p) ≃ FactorData p n

Parametrize irreducible factor data by the lower coefficients of its product.

Equations

• KloostermanWeil.Carlitz.coeffFactorEquiv p n = (KloostermanWeil.Carlitz.coeffVectorEquivMonicDeg p n).trans (KloostermanWeil.Carlitz.monicFactorEquiv p n)

theorem KloostermanWeil.Carlitz.A_eq_factorData_sum (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (n : ℕ) : Dickson.A p t n = ∑ s : FactorData p n, factorWeight p t s