OAI/NumberTheory/CubicMoment/Theta/CubicThetaFiniteFourierInverse.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The inverse of the actual finite codifferent Fourier transform, including the cardinality normalization.

  1. def OAI.CubicFirstMoment.cubicThetaFiniteFourierAdjoint line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaFiniteFourierAdjoint_conjugate line 15
  3. theorem OAI.CubicFirstMoment.cubicThetaFiniteFourierAdjoint_inverse line 26
  4. theorem OAI.CubicFirstMoment.cubicThetaFiniteFourier_inverse_adjoint line 34
  5. lemma OAI.CubicFirstMoment.cubicThetaFiniteFourier_const_mul line 47
  6. lemma OAI.CubicFirstMoment.cubicThetaFiniteFourierAdjoint_const_mul line 52
  7. theorem OAI.CubicFirstMoment.cubicThetaFiniteFourier_injective line 58