OAI/NumberTheory/CubicMoment/Theta/CubicThetaFiniteKloostermanIntertwiner.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite Fourier-conjugated Kloosterman operator. It is Hermitian and squares to the actual primary Fourier projection. Its entries are the normalized signed Kloosterman kernel from the Gram expansion.

  1. lemma OAI.CubicFirstMoment.cubicThetaFiniteFourierAdjoint_neg line 12
  2. def OAI.CubicFirstMoment.cubicThetaFiniteKloostermanIntertwiner line 22
  3. theorem OAI.CubicFirstMoment.cubicThetaFiniteKloostermanIntertwiner_kernel line 29
  4. theorem OAI.CubicFirstMoment.cubicThetaFiniteKloostermanIntertwiner_fourier line 37
  5. theorem OAI.CubicFirstMoment.cubicThetaFiniteKloostermanIntertwiner_square line 49
  6. theorem OAI.CubicFirstMoment.cubicThetaFiniteKloostermanIntertwiner_symmetric line 64