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

Finite-field and Dickson-polynomial algebra

The finite-field notation, elementary Kloosterman sums and Dickson-polynomial identities used in the Carlitz recurrence. See Carlitz (1969) for the method.

@[reducible, inline]

abbrev KloostermanWeil.Dickson.Fp (p : ℕ) : Type

The prime residue ring used as the base field when p is prime.

Equations

• KloostermanWeil.Dickson.Fp p = ZMod p

@[reducible, inline]

abbrev KloostermanWeil.Dickson.FpPoly (p : ℕ) : Type

Polynomials over the prime residue ring.

Equations

• KloostermanWeil.Dickson.FpPoly p = Polynomial (KloostermanWeil.Dickson.Fp p)

noncomputable def KloostermanWeil.Dickson.baseKloosterman (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) : ℂ

Base-field one-parameter Kloosterman sum in the source-normalized sign convention.

Equations

• KloostermanWeil.Dickson.baseKloosterman p t = ∑ x : KloostermanWeil.Dickson.Fp p, if x = 0 then 0 else ZMod.stdAddChar (x + t * x⁻¹)

noncomputable def KloostermanWeil.Dickson.etaPoly (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) (f : FpPoly p) : ℂ

Carlitz's multiplicative polynomial weight, specialized to K(1,t). It is only used on monic polynomials; the zero-constant case is extended by zero.

Equations

• KloostermanWeil.Dickson.etaPoly p t f = if (Polynomial.coeff f) 0 = 0 then 0 else ZMod.stdAddChar (-Polynomial.nextCoeff f - t * ((Polynomial.coeff f) 1 / (Polynomial.coeff f) 0))

theorem KloostermanWeil.Dickson.etaPoly_one (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) : etaPoly p t 1 = 1

theorem KloostermanWeil.Dickson.etaPoly_mul_of_monic (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) {f g : FpPoly p} (hf : Polynomial.Monic f) (hg : Polynomial.Monic g) : etaPoly p t (f * g) = etaPoly p t f * etaPoly p t g

noncomputable def KloostermanWeil.Dickson.monicFromCoeffs (p n : ℕ) [Fact (Nat.Prime p)] (a : Fin n → Fp p) : FpPoly p

Canonical monic polynomial with prescribed lower coefficients.

Equations

• KloostermanWeil.Dickson.monicFromCoeffs p n a = Polynomial.X ^ n + ∑ i : Fin n, Polynomial.C (a i) * Polynomial.X ^ ↑i

theorem KloostermanWeil.Dickson.monicFromCoeffs_monic (p n : ℕ) [Fact (Nat.Prime p)] (a : Fin n → Fp p) : Polynomial.Monic (monicFromCoeffs p n a)

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

The degree-n coefficient sum in the Carlitz L-polynomial.

Equations

• KloostermanWeil.Dickson.A p t n = ∑ a : Fin n → KloostermanWeil.Dickson.Fp p, KloostermanWeil.Dickson.etaPoly p t (KloostermanWeil.Dickson.monicFromCoeffs p n a)

theorem KloostermanWeil.Dickson.A_one_eq_K (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) : A p t 1 = baseKloosterman p t

Degree one coefficient is the base Kloosterman sum.

theorem KloostermanWeil.Dickson.A_zero_eq_one (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) : A p t 0 = 1

noncomputable def KloostermanWeil.Dickson.monicQuadratic {p : ℕ} [Fact (Nat.Prime p)] (b c : Fp p) : FpPoly p

The monic quadratic with linear coefficient b and constant coefficient c.

Equations

• KloostermanWeil.Dickson.monicQuadratic b c = Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c

theorem KloostermanWeil.Dickson.monicQuadratic_monic {p : ℕ} [Fact (Nat.Prime p)] (b c : Fp p) : Polynomial.Monic (monicQuadratic b c)

theorem KloostermanWeil.Dickson.monicQuadratic_coeff_zero {p : ℕ} [Fact (Nat.Prime p)] (b c : Fp p) : (Polynomial.coeff (monicQuadratic b c)) 0 = c

theorem KloostermanWeil.Dickson.monicQuadratic_coeff_one {p : ℕ} [Fact (Nat.Prime p)] (b c : Fp p) : (Polynomial.coeff (monicQuadratic b c)) 1 = b

theorem KloostermanWeil.Dickson.monicQuadratic_nextCoeff {p : ℕ} [Fact (Nat.Prime p)] (b c : Fp p) : Polynomial.nextCoeff (monicQuadratic b c) = b

theorem KloostermanWeil.Dickson.etaPoly_monicQuadratic (p : ℕ) [Fact (Nat.Prime p)] (t b c : Fp p) : etaPoly p t (monicQuadratic b c) = if c = 0 then 0 else ZMod.stdAddChar (-(1 + t / c) * b)

theorem KloostermanWeil.Dickson.sum_etaPoly_monicQuadratic (p : ℕ) [Fact (Nat.Prime p)] {t c : Fp p} (ht : t ≠ 0) : ∑ b : Fp p, etaPoly p t (monicQuadratic b c) = if c = -t then ↑p else 0

noncomputable def KloostermanWeil.Dickson.finTwoCoeffEquiv (p : ℕ) : (Fin 2 → Fp p) ≃ Fp p × Fp p

Identify a two-entry coefficient vector with an ordered pair.

Equations

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

theorem KloostermanWeil.Dickson.finTwoCoeffEquiv_apply (p : ℕ) (a : Fin 2 → Fp p) : (finTwoCoeffEquiv p) a = (a 0, a 1)

theorem KloostermanWeil.Dickson.monicFromCoeffs_two (p : ℕ) [Fact (Nat.Prime p)] (a : Fin 2 → Fp p) : monicFromCoeffs p 2 a = monicQuadratic (a 1) (a 0)

theorem KloostermanWeil.Dickson.A_two_eq_card (p : ℕ) [Fact (Nat.Prime p)] {t : Fp p} (ht : t ≠ 0) : A p t 2 = ↑p

theorem KloostermanWeil.Dickson.coeff_fintype_sum {R : Type u_1} {ι : Type u_2} [Semiring R] [Fintype ι] (f : ι → Polynomial R) (j : ℕ) : (∑ i : ι, f i).coeff j = ∑ i : ι, (f i).coeff j

theorem KloostermanWeil.Dickson.monicFromCoeffs_degree (p n : ℕ) [Fact (Nat.Prime p)] (a : Fin n → Fp p) : Polynomial.degree (monicFromCoeffs p n a) = ↑n

theorem KloostermanWeil.Dickson.monicFromCoeffs_coeff_lt (p n j : ℕ) [Fact (Nat.Prime p)] (hj : j < n) (a : Fin n → Fp p) : (Polynomial.coeff (monicFromCoeffs p n a)) j = a ⟨j, hj⟩

noncomputable def KloostermanWeil.Dickson.lastIndex (n : ℕ) (hn : 0 < n) : Fin n

The index of the final lower coefficient of a positive-degree monic polynomial.

Equations

• KloostermanWeil.Dickson.lastIndex n hn = ⟨n - 1, ⋯⟩

theorem KloostermanWeil.Dickson.monicFromCoeffs_nextCoeff (p n : ℕ) [Fact (Nat.Prime p)] (hn : 0 < n) (a : Fin n → Fp p) : Polynomial.nextCoeff (monicFromCoeffs p n a) = a (lastIndex n hn)

noncomputable def KloostermanWeil.Dickson.shiftLastEquiv (p n : ℕ) [Fact (Nat.Prime p)] (hn : 0 < n) (u : Fp p) : (Fin n → Fp p) ≃ (Fin n → Fp p)

Translate the final lower coefficient by u, keeping the other coefficients fixed.

Equations

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

theorem KloostermanWeil.Dickson.shiftLastEquiv_at_last (p n : ℕ) [Fact (Nat.Prime p)] (hn : 0 < n) (u : Fp p) (a : Fin n → Fp p) : (shiftLastEquiv p n hn u) a (lastIndex n hn) = a (lastIndex n hn) + u

theorem KloostermanWeil.Dickson.shiftLastEquiv_at_zero (p n : ℕ) [Fact (Nat.Prime p)] (hn2 : 2 ≤ n) (u : Fp p) (a : Fin n → Fp p) : (shiftLastEquiv p n ⋯ u) a ⟨0, ⋯⟩ = a ⟨0, ⋯⟩

theorem KloostermanWeil.Dickson.shiftLastEquiv_at_one (p n : ℕ) [Fact (Nat.Prime p)] (hn3 : 3 ≤ n) (u : Fp p) (a : Fin n → Fp p) : (shiftLastEquiv p n ⋯ u) a ⟨1, ⋯⟩ = a ⟨1, ⋯⟩

theorem KloostermanWeil.Dickson.etaPoly_shiftLast (p n : ℕ) [Fact (Nat.Prime p)] (hn3 : 3 ≤ n) (t u : Fp p) (a : Fin n → Fp p) : etaPoly p t (monicFromCoeffs p n ((shiftLastEquiv p n ⋯ u) a)) = ZMod.stdAddChar (-u) * etaPoly p t (monicFromCoeffs p n a)

theorem KloostermanWeil.Dickson.A_eq_zero_of_three_le (p n : ℕ) [Fact (Nat.Prime p)] (hn3 : 3 ≤ n) (t : Fp p) : A p t n = 0

theorem KloostermanWeil.Dickson.dickson_one_eval_add_of_mul {R : Type u_1} [CommRing R] (x y a : R) (hxy : x * y = a) (n : ℕ) : Polynomial.eval (x + y) (Polynomial.dickson 1 a n) = x ^ n + y ^ n