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

From point counts to the spectral circle

Combines the Carlitz recurrence with Stepanov point-count estimates to bound the two spectral roots; compare Harcos (2015), §3, equations (2)–(3).

@[reducible, inline]

abbrev KloostermanWeil.Stepanov.CarlitzRootIndex (p : ℕ) : Type

Index the two spectral roots for each nonzero scalar in the base field.

Equations

• KloostermanWeil.Stepanov.CarlitzRootIndex p = ({ m : ZMod p // m ≠ 0 } × Bool)

noncomputable def KloostermanWeil.Stepanov.normalizedCarlitzSquaredRoot (p : ℕ) [Fact (Nat.Prime p)] (c : ZMod p) (x : CarlitzRootIndex p) : ℂ

The selected spectral root for parameter m²c, squared and divided by p.

Equations

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

theorem KloostermanWeil.Stepanov.natSqrt_even_primePower (p n : ℕ) : (p ^ (2 * n)).sqrt = p ^ n

theorem KloostermanWeil.Stepanov.eventually_kloostermanCurve_large (p : ℕ) [Fact (Nat.Prime p)] : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → 100 * (2 * p + 1) * ((p ^ (2 * n)).sqrt + 1) < p ^ (2 * n)

theorem KloostermanWeil.Stepanov.sum_normalizedCarlitzSquaredRoot_pow (p n : ℕ) [Fact (Nat.Prime p)] (c : ZMod p) : ∑ x : CarlitzRootIndex p, normalizedCarlitzSquaredRoot p c x ^ n = (∑ m : { m : ZMod p // m ≠ 0 }, (carlitzAlpha p (↑m ^ 2 * c) ^ (2 * n) + carlitzBeta p (↑m ^ 2 * c) ^ (2 * n))) / ↑p ^ n

theorem KloostermanWeil.Stepanov.rootPowerSum_eq_neg_errorAggregate_sub_one (p n : ℕ) [Fact (Nat.Prime p)] (c : ZMod p) (hc : c ≠ 0) (hn : n ≠ 0) : ∑ m : { m : ZMod p // m ≠ 0 }, (carlitzAlpha p (↑m ^ 2 * c) ^ n + carlitzBeta p (↑m ^ 2 * c) ^ n) = -errorAggregate p n c - 1

theorem KloostermanWeil.Stepanov.norm_natCast_sub_natCast_eq_intAbs (a b : ℕ) : ‖↑a - ↑b‖ = ↑|↑a - ↑b|

theorem KloostermanWeil.Stepanov.normalizedCarlitzSquaredRoot_powerSum_eventually (p : ℕ) [Fact (Nat.Prime p)] (hpodd : Odd p) (c : ZMod p) (hc : c ≠ 0) : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → ‖∑ x : CarlitzRootIndex p, normalizedCarlitzSquaredRoot p c x ^ n‖ ≤ 160 * (2 * ↑p + 1) + 2

theorem KloostermanWeil.Stepanov.normalizedCarlitzSquaredRoot_norm_le_one (p : ℕ) [Fact (Nat.Prime p)] (hpodd : Odd p) (c : ZMod p) (hc : c ≠ 0) (x : CarlitzRootIndex p) : ‖normalizedCarlitzSquaredRoot p c x‖ ≤ 1

theorem KloostermanWeil.Stepanov.carlitzAlpha_norm_sq_le_prime (p : ℕ) [Fact (Nat.Prime p)] (hpodd : Odd p) (c : ZMod p) (hc : c ≠ 0) (m : { m : ZMod p // m ≠ 0 }) : ‖carlitzAlpha p (↑m ^ 2 * c)‖ ^ 2 ≤ ↑p

theorem KloostermanWeil.Stepanov.carlitzBeta_norm_sq_le_prime (p : ℕ) [Fact (Nat.Prime p)] (hpodd : Odd p) (c : ZMod p) (hc : c ≠ 0) (m : { m : ZMod p // m ≠ 0 }) : ‖carlitzBeta p (↑m ^ 2 * c)‖ ^ 2 ≤ ↑p