OAI/NumberTheory/CubicMoment/Theta/CubicThetaActualProjection.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual primary projector and its finite transformed cusp family.

  1. def OAI.CubicFirstMoment.cubicThetaCuspIndex line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaCuspCoordinates line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaNormalizedSeries_primaryBottom_index line 18
  4. def OAI.CubicFirstMoment.cubicThetaNormalizedPrimaryProjection line 28
  5. lemma OAI.CubicFirstMoment.cubicThetaNormalizedSeries_translation_conjugate line 33
  6. lemma OAI.CubicFirstMoment.cubicThetaNormalizedPrimaryProjection_series line 42
  7. lemma OAI.CubicFirstMoment.cubicThetaFullTranslation_mul_bottom line 59
  8. def OAI.CubicFirstMoment.cubicThetaProjectedCuspMatrix line 66
  9. lemma OAI.CubicFirstMoment.cubicThetaProjectedCuspMatrix_primary line 69
  10. def OAI.CubicFirstMoment.cubicThetaProjectedCuspMultiplier line 74
  11. def OAI.CubicFirstMoment.cubicThetaProjectedCuspType line 79
  12. lemma OAI.CubicFirstMoment.cubicThetaProjectedCusp_identity line 82
  13. theorem OAI.CubicFirstMoment.cubicThetaNormalizedPrimaryProjection_cusps line 96