OAI/NumberTheory/CubicMoment/Theta/CubicThetaRowMellin.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The Gaussian row identity integrated to the actual Eisenstein row on its initial half-plane of absolute convergence.

  1. lemma OAI.CubicFirstMoment.cubicThetaRowRadius_complex_power line 13
  2. def OAI.CubicFirstMoment.cubicThetaEisensteinRow line 25
  3. theorem OAI.CubicFirstMoment.cubicThetaEisensteinRow_mellin line 28