OAI/NumberTheory/CubicMoment/Theta/CubicThetaFiniteFourierParseval.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact finite Fourier orthogonality and Parseval for the codifferent pairing used by the Kloosterman row kernels.

  1. lemma OAI.CubicFirstMoment.cubicThetaResidueFourier_norm line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaResidueFourier_star line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaResidueFourier_orthogonal line 22
  4. def OAI.CubicFirstMoment.cubicThetaFiniteFourier line 37
  5. lemma OAI.CubicFirstMoment.cubicThetaFiniteFourier_inverse_pairing line 41
  6. theorem OAI.CubicFirstMoment.cubicThetaFiniteFourier_parseval line 62
  7. lemma OAI.CubicFirstMoment.cubicThetaFiniteFourier_norm_sq line 86