OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRows.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The five possible local rows at a cubically multiplied frequency.

  1. lemma OAI.CubicFirstMoment.cubicThetaNormPower_cpow line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeFree_cubeFrequency line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeFree_phaseCube line 27
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerTerm_cube_zero line 36
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerTerm_cube_one line 43
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerTerm_cube_two line 55
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerTerm_cube_three line 67
  8. lemma OAI.CubicFirstMoment.cubicThetaEisensteinGaussCoefficient_fourth_cube line 86
  9. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerTerm_cube_four line 98
  10. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerTerm_cube_high line 109