OAI/NumberTheory/CubicMoment/Theta/CubicThetaKloostermanFourierGram.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite Fourier realization and exact Gram identity for the actual Kloosterman weights, retaining their zero extension at common factors.

  1. def OAI.CubicFirstMoment.cubicThetaFiniteKloosterman line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaFiniteKloosterman_integer line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaFiniteKloosterman_fourier line 23
  4. theorem OAI.CubicFirstMoment.cubicThetaFiniteKloosterman_gram line 35