OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootFourierProducts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal projection algebra for the actual cubic-scale finite action.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootFourierL2_translate line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootFourierL2_commute line 43
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootFourierL2_eigen line 56
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootFourierL2_product line 62
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootFourierL2_idempotent line 83