OAI/NumberTheory/CubicMoment/Theta/CubicThetaScalarEisenstein.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The scalar Eisenstein series for the same principal arithmetic group. It supplies the positive height kernel for the energy unfolding.

  1. def OAI.CubicFirstMoment.cubicThetaScalarEisenstein line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaScalarEisenstein_summable line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaScalarEisenstein_real_summable line 22
  4. theorem OAI.CubicFirstMoment.cubicThetaScalarEisenstein_invariant line 30