OAI/NumberTheory/CubicMoment/Theta/CubicThetaTorusModes.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual trace frequencies are the full Fourier basis of the three-Eisenstein period cell. This fixes the lattice index and Parseval normalization for the cusp Hilbert space.

  1. def OAI.CubicFirstMoment.cubicThetaFourierIndex line 17
  2. def OAI.CubicFirstMoment.cubicThetaPeriodCell line 20
  3. lemma OAI.CubicFirstMoment.cubicTheta_trace_period_cell line 22
  4. lemma OAI.CubicFirstMoment.cubicTheta_torus_fourier_real line 34
  5. def OAI.CubicFirstMoment.cubicThetaTorusFourier line 44
  6. lemma OAI.CubicFirstMoment.cubicThetaTorusFourier_actual line 47
  7. abbrev OAI.CubicFirstMoment.CubicThetaTorusL2 line 53
  8. def OAI.CubicFirstMoment.cubicThetaTorusCoefficient line 55
  9. theorem OAI.CubicFirstMoment.cubicThetaTorus_parseval line 58
  10. theorem OAI.CubicFirstMoment.cubicThetaTorus_coefficients_summable line 66