OAI/NumberTheory/CubicMoment/Theta/CubicThetaAllGridEquation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every literal Eisenstein grid summand satisfies the same spectral equation, including the distinguished cusp row and the zero extension.

  1. lemma OAI.CubicFirstMoment.cubicThetaEisensteinGridTerm_zero line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaEisensteinGrid_eigenvalue line 23