OAI/NumberTheory/CubicMoment/Theta/CubicThetaFiniteSpectral.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The spectral equation for actual finite Eisenstein partial sums. Coordinate analyticity justifies every differentiation of the finite sum.

  1. lemma OAI.CubicFirstMoment.deriv_sum_apply line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaHyperbolicOperator_sum line 21
  3. def OAI.CubicFirstMoment.cubicThetaFiniteEisenstein line 58
  4. theorem OAI.CubicFirstMoment.cubicThetaFiniteEisenstein_eigenvalue line 62