OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspFourierTransform.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The actual Fourier coefficient map embeds the mean-zero cusp slices isometrically into the radial mode space used by the compact Green operator.

  1. abbrev OAI.CubicFirstMoment.CubicThetaAllCuspModes line 15
  2. def OAI.CubicFirstMoment.cubicThetaCuspFourierVector line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaCuspFourierVector_norm line 21
  4. def OAI.CubicFirstMoment.cubicThetaCuspFourierTransform line 28
  5. def OAI.CubicFirstMoment.cubicThetaMeanZeroSlices line 40
  6. instance OAI.CubicFirstMoment.cubicThetaMeanZeroSlices_complete line 43
  7. lemma OAI.CubicFirstMoment.cubicThetaMeanZeroSlices_zero line 46
  8. lemma OAI.CubicFirstMoment.cubicThetaMeanZeroSlices_parseval line 49
  9. def OAI.CubicFirstMoment.cubicThetaMeanZeroFourierVector line 62
  10. lemma OAI.CubicFirstMoment.cubicThetaMeanZeroFourierVector_norm line 68
  11. def OAI.CubicFirstMoment.cubicThetaMeanZeroFourierTransform line 75