OAI/NumberTheory/CubicMoment/Theta/CubicThetaEisensteinUnfold.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact absolutely convergent unfolding from primitive rows to the two Eisenstein lattice coordinates.

  1. def OAI.CubicFirstMoment.cubicThetaAdmissiblePair line 11
  2. def OAI.CubicFirstMoment.cubicThetaBottomRowEquiv line 14
  3. def OAI.CubicFirstMoment.cubicThetaEisensteinGridTerm line 20
  4. lemma OAI.CubicFirstMoment.cubicThetaEisensteinGridTerm_admissible line 26
  5. lemma OAI.CubicFirstMoment.cubicThetaEisensteinGrid_summable line 34
  6. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_eq_grid line 53
  7. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_unfold line 71