Documentation

LeanPool.KloostermanWeil.Carlitz.ExtensionDefinitions

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 Kloosterman sums #

Defines additive characters, trace maps and sums over finite extensions. Compare Carlitz (1969), equations (2.8)–(2.13); the exact Lean normalization is specified by the definitions below.

source
@[reducible, inline]
abbrev KloostermanWeil.Carlitz.Fp (p : ℕ) :
Type

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

Equations
Instances For
    source
    @[reducible, inline]
    abbrev KloostermanWeil.Carlitz.Ext (p n : ℕ) [Fact (Nat.Prime p)] :
    Type

    The chosen finite Galois extension of the prime field.

    Equations
    Instances For
      source
      noncomputable def KloostermanWeil.Carlitz.psiExt (p n : ℕ) [Fact (Nat.Prime p)] :
      AddChar (Ext p n) ℂ

      Canonical additive character on the chosen degree-n extension: the base standard additive character composed with algebra trace.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def KloostermanWeil.Carlitz.Kext (p n : ℕ) [Fact (Nat.Prime p)] (t : Fp p) :
        ℂ

        Carlitz extension-field Kloosterman sum in prime-modulus argument/sign convention.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def KloostermanWeil.Carlitz.degreeOneEquiv (p : ℕ) [Fact (Nat.Prime p)] :
          Fp p ≃ₐ[Fp p] Ext p 1

          Canonical degree-one change of variables from the base field.

          Equations
          Instances For
            source
            theorem KloostermanWeil.Carlitz.trace_degreeOneEquiv (p : ℕ) [Fact (Nat.Prime p)] (x : Fp p) :
            (Algebra.trace (Fp p) (Ext p 1)) ((degreeOneEquiv p) x) = x
            source
            theorem KloostermanWeil.Carlitz.psiExt_degreeOneEquiv (p : ℕ) [Fact (Nat.Prime p)] (x : Fp p) :
            (psiExt p 1) ((degreeOneEquiv p) x) = ZMod.stdAddChar x
            source
            theorem KloostermanWeil.Carlitz.Kext_one_eq_kloostermanSumPrime (p : ℕ) [Fact (Nat.Prime p)] (t : Fp p) :
            Kext p 1 t = kloostermanSumPrime p t 1