OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspFourierSurjective.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Single Fourier modes are actual cusp slices. Their finite sums and completeness prove that the Fourier isometry is onto the radial mode space.

  1. def OAI.CubicFirstMoment.cubicThetaTorusBasis line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaTorusCoefficient_basis line 18
  3. def OAI.CubicFirstMoment.cubicThetaTorusTensor line 24
  4. def OAI.CubicFirstMoment.cubicThetaTensorSlice line 27
  5. lemma OAI.CubicFirstMoment.cubicThetaTensorSlice_coefficient line 30
  6. lemma OAI.CubicFirstMoment.cubicThetaCuspFourierTransform_tensor line 43
  7. theorem OAI.CubicFirstMoment.cubicThetaCuspFourierTransform_surjective line 52
  8. def OAI.CubicFirstMoment.cubicThetaCuspFourierEquiv line 64