OAI/NumberTheory/CubicMoment/Theta/CubicThetaInvertedRows.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact primitive rows at the inverted cusp. This identifies the actual transformed Eisenstein series before taking its constant term.

  1. structure OAI.CubicFirstMoment.CubicThetaInvertedRow line 11
  2. def OAI.CubicFirstMoment.cubicThetaInvertedRowEquiv line 18
  3. def OAI.CubicFirstMoment.CubicThetaInvertedRow.height line 24
  4. def OAI.CubicFirstMoment.cubicThetaInvertedTerm line 27
  5. theorem OAI.CubicFirstMoment.cubicThetaBottomRow_height_full line 30
  6. theorem OAI.CubicFirstMoment.cubicThetaBottomRow_height_inverted line 55
  7. theorem OAI.CubicFirstMoment.cubicThetaEisensteinTerm_inverted line 65
  8. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_inverted line 76