Documentation

LeanPool.KloostermanWeil.Carlitz.GeneratingIdentity

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

Extension-field generating identity #

Derives the generating-series identity from the formal algebra and Newton sums, following Carlitz (1969). The exact sign and trace normalization has not yet been compared equation by equation with the original article.

source
noncomputable def KloostermanWeil.Carlitz.Kseq (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) :
ℕ → ℂ

Total sequence wrapper: Carlitz sums live only in positive extension degree.

Equations
Instances For
    source
    @[simp]
    theorem KloostermanWeil.Carlitz.Kseq_zero (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) :
    Kseq p t 0 = 0
    source
    @[simp]
    theorem KloostermanWeil.Carlitz.Kseq_succ (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) (n : ℕ) :
    Kseq p t (n + 1) = Kext p (n + 1) t
    source
    noncomputable def KloostermanWeil.Carlitz.LSeriesA (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) :
    PowerSeries ℂ

    The formal generating series of the weighted monic-polynomial sums A.

    Equations
    Instances For
      source
      @[simp]
      theorem KloostermanWeil.Carlitz.coeff_LSeriesA (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) (n : ℕ) :
      (PowerSeries.coeff n) (LSeriesA p t) = Dickson.A p t n
      source
      @[simp]
      theorem KloostermanWeil.Carlitz.constantCoeff_LSeriesA (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) :
      PowerSeries.constantCoeff (LSeriesA p t) = 1
      source
      theorem KloostermanWeil.Carlitz.Kseq_one_eq_baseKloosterman (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) :
      Kseq p t 1 = Dickson.baseKloosterman p t
      source
      theorem KloostermanWeil.Carlitz.LSeriesA_eq_quadratic (p : ℕ) [Fact (Nat.Prime p)] {t : Fp p} (ht : t ≠ 0) :
      LSeriesA p t = quadraticL (Kseq p t 1) ↑p
      source
      theorem KloostermanWeil.Carlitz.derivative_KSeries_mul_LSeriesA (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) :
      PowerSeries.derivative (KSeries (Kseq p t)) * LSeriesA p t = PowerSeries.derivative (LSeriesA p t)
      source
      theorem KloostermanWeil.Carlitz.generating_identity_with_LSeriesA (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) :
      KSeries (Kseq p t) = (LSeriesA p t).logOf
      source
      theorem KloostermanWeil.Carlitz.carlitz_generating_identity (p : ℕ) [Fact (Nat.Prime p)] {t : Fp p} (ht : t ≠ 0) :
      KSeries (Kseq p t) = (quadraticL (Kseq p t 1) ↑p).logOf

      Carlitz generating-series identity in the exact prime-modulus Kloosterman normalization.