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

Carlitz spectral roots

Connects the two spectral roots of the Carlitz recurrence to the formulation in Harcos (2015), equation (2).

noncomputable def KloostermanWeil.Stepanov.carlitzAlpha (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) : ℂ

A chosen first spectral root for nonzero t, extended by zero at t = 0.

Equations

• KloostermanWeil.Stepanov.carlitzAlpha p t = if ht : t = 0 then 0 else Classical.choose ⋯

noncomputable def KloostermanWeil.Stepanov.carlitzBeta (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) : ℂ

The matching second spectral root, extended by zero at t = 0.

Equations

• KloostermanWeil.Stepanov.carlitzBeta p t = if ht : t = 0 then 0 else Classical.choose ⋯

theorem KloostermanWeil.Stepanov.carlitzAlpha_add_beta (p : ℕ) [Fact (Nat.Prime p)] {t : ZMod p} (ht : t ≠ 0) : carlitzAlpha p t + carlitzBeta p t = -Carlitz.Kext p 1 t

theorem KloostermanWeil.Stepanov.carlitzAlpha_mul_beta (p : ℕ) [Fact (Nat.Prime p)] {t : ZMod p} (ht : t ≠ 0) : carlitzAlpha p t * carlitzBeta p t = ↑p

theorem KloostermanWeil.Stepanov.Kext_eq_neg_root_power_sum (p : ℕ) [Fact (Nat.Prime p)] {t : ZMod p} (ht : t ≠ 0) (r : ℕ) : Carlitz.Kext p (r + 1) t = -(carlitzAlpha p t ^ (r + 1) + carlitzBeta p t ^ (r + 1))

theorem KloostermanWeil.Stepanov.Kext_eq_neg_root_power_sum_pos (p n : ℕ) [Fact (Nat.Prime p)] {t : ZMod p} (ht : t ≠ 0) (hn : n ≠ 0) : Carlitz.Kext p n t = -(carlitzAlpha p t ^ n + carlitzBeta p t ^ n)