OAI/NumberTheory/CubicMoment/Theta/CubicThetaIncomingRows.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The incoming cutoff series uses the actual primitive bottom rows. Above the arithmetic cusp threshold at most one row contributes.

  1. lemma OAI.CubicFirstMoment.CubicThetaBottomRow.high_height_c_zero line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaIncomingRows_unique line 22
  3. def OAI.CubicFirstMoment.cubicThetaIncomingTerm line 47
  4. lemma OAI.CubicFirstMoment.cubicThetaIncomingTerm_high line 50
  5. lemma OAI.CubicFirstMoment.cubicThetaIncomingTerm_finite line 56
  6. def OAI.CubicFirstMoment.cubicThetaIncomingEisenstein line 63
  7. lemma OAI.CubicFirstMoment.cubicThetaIncomingTerm_translate line 66
  8. theorem OAI.CubicFirstMoment.cubicThetaIncomingEisenstein_automorphy line 74
  9. theorem OAI.CubicFirstMoment.cubicThetaIncomingEisenstein_high line 84