OAI/NumberTheory/CubicMoment/Theta/CubicThetaInvertedUnfold.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Absolute convergence and the literal primary-row unfolding at the inverted cusp. The second coordinate is exactly three times a lattice point.

  1. def OAI.CubicFirstMoment.cubicThetaInvertedAdmissible line 12
  2. def OAI.CubicFirstMoment.cubicThetaInvertedPairEquiv line 15
  3. def OAI.CubicFirstMoment.cubicThetaInvertedGridTerm line 22
  4. lemma OAI.CubicFirstMoment.cubicThetaInvertedGridTerm_admissible line 29
  5. lemma OAI.CubicFirstMoment.cubicThetaInvertedTerm_summable line 37
  6. lemma OAI.CubicFirstMoment.cubicThetaInvertedGrid_summable line 50
  7. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_inverted_grid line 67
  8. lemma OAI.CubicFirstMoment.cubicThetaInvertedGridTerm_triple line 85