Documentation

LeanPool.KasamiCyclicAdditive.MCM.Fourier

The MCM Fourier/Dickson reduction #

For a multiplicative character χ with χ^(2^k+1) ≠ 1, additive Fourier inversion reduces the untwisted and additively twisted MCM character sums

∑_s χ(M_k s) and ∑_s ψ(s) χ(M_k s)

to Gauss-sum ratios against sparse Dickson-polynomial character sums, using the identities

b^(2^k+1) T_k(b⁻¹)² = D_(2^k-1)(b), b^(2^k+1) T_k(1+b⁻¹)² = D_(2^k+1)(b).

For the complementary case of a nonprincipal cubic χ and odd k, the MCM map is invisible to χ: χ(M_k s) = χ(s).

source
noncomputable def KasamiCyclicAdditive.mcmCharSum {K : Type u_1} [Field K] [Fintype K] (k : ℕ) (χ : MulChar K ℂ) :
ℂ

Untwisted MCM character sum. Multiplicative characters vanish at zero.

Equations
Instances For
    source
    noncomputable def KasamiCyclicAdditive.mcmTwistedCharSum {K : Type u_1} [Field K] [Fintype K] (k : ℕ) (ψ : AddChar K ℂ) (χ : MulChar K ℂ) :
    ℂ

    Additively twisted MCM character sum.

    Equations
    Instances For

      Characteristic-two preliminaries #

      Dickson polynomial identities #

      source
      theorem KasamiCyclicAdditive.dickson_add_formula (R : Type u_2) [CommRing R] (n d : ℕ) :
      Polynomial.dickson 1 1 (d + 2 * n) + Polynomial.dickson 1 1 d = Polynomial.dickson 1 1 (d + n) * Polynomial.dickson 1 1 n

      D_(d + 2n) + D_d = D_(d + n) * D_n for Dickson polynomials of parameter 1.

      source
      theorem KasamiCyclicAdditive.dickson_two_pow (R : Type u_2) [CommRing R] [CharP R 2] (k : ℕ) :
      Polynomial.dickson 1 1 (2 ^ k) = Polynomial.X ^ 2 ^ k

      In characteristic two, D_(2 ^ k) = X ^ (2 ^ k).

      Character preliminaries #

      The adjoint of T_k for the trace pairing #

      Factorisation of χ ∘ M_k #

      Fourier/adjoint and Dickson bridges #

      source
      theorem KasamiCyclicAdditive.mcmCharSum_eq_dickson {K : Type u_1} [Field K] [Fintype K] [CharP K 2] {n k : ℕ} (hklt : k < n) (hcard : Fintype.card K = 2 ^ n) (ψ : AddChar K ℂ) (hpsi : ψ.IsPrimitive) (hpsi_sq : ∀ (x : K), ψ (x ^ 2) = ψ x) (χ : MulChar K ℂ) (hchie : χ ^ (2 ^ k + 1) ≠ 1) :
      mcmCharSum k χ = gaussSum (χ⁻¹ ^ 2 ^ k) ψ / gaussSum (χ⁻¹ ^ (2 ^ k + 1)) ψ * ∑ b : K, χ (Polynomial.eval b (Polynomial.dickson 1 1 (2 ^ k - 1)))

      The untwisted MCM character sum as a Gauss-sum ratio against a sparse Dickson character sum.

      source
      theorem KasamiCyclicAdditive.mcmTwistedCharSum_eq_dickson {K : Type u_1} [Field K] [Fintype K] [CharP K 2] {n k : ℕ} (hklt : k < n) (hcard : Fintype.card K = 2 ^ n) (hk : Odd k) (ψ : AddChar K ℂ) (hpsi : ψ.IsPrimitive) (hpsi_sq : ∀ (x : K), ψ (x ^ 2) = ψ x) (χ : MulChar K ℂ) (hchie : χ ^ (2 ^ k + 1) ≠ 1) :
      mcmTwistedCharSum k ψ χ = gaussSum (χ⁻¹ ^ 2 ^ k) ψ / gaussSum (χ⁻¹ ^ (2 ^ k + 1)) ψ * ∑ b : K, χ (Polynomial.eval b (Polynomial.dickson 1 1 (2 ^ k + 1)))

      The additively twisted MCM character sum as a Gauss-sum ratio against a sparse Dickson character sum.

      source
      theorem KasamiCyclicAdditive.cubic_mcm_apply {K : Type u_1} [Field K] [Fintype K] [CharP K 2] {n k : ℕ} (hcard : Fintype.card K = 2 ^ n) (hk : Odd k) (hkn : k.Coprime n) (χ : MulChar K ℂ) (hchi3 : χ ^ 3 = 1) (s : K) :
      χ (mcmMap k s) = χ s

      Cubic exceptional case: if χ^3=1 and χ is nonprincipal, then for odd k the MCM map is invisible to χ: χ(M_k(s))=χ(s).