OAI/NumberTheory/CubicMoment/Theta/CubicThetaEisensteinHolomorphic.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Holomorphy of the actual cubic Eisenstein series on its initial half-plane, obtained from a uniform summable row bound.

  1. lemma OAI.CubicFirstMoment.cubicThetaHeightConstant_ge_one line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaEisensteinTerm_differentiable line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaEisensteinTerm_strip_bound line 26
  4. lemma OAI.CubicFirstMoment.cubicThetaEisenstein_differentiableOn_strip line 42
  5. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_differentiableAt line 62