OAI/NumberTheory/CubicMoment/Theta/CubicThetaLevelAngularMellin.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Entire Mellin continuation of the actual nonzero angular series at inverse cusps.

  1. def OAI.CubicFirstMoment.cubicThetaLevelAngularPhase line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaLevelAngularAxis_functional line 15
  3. def OAI.CubicFirstMoment.cubicThetaLevelAngularCompleted line 32
  4. theorem OAI.CubicFirstMoment.cubicThetaLevelAngular_mellin line 39
  5. theorem OAI.CubicFirstMoment.cubicThetaLevelAngularCompleted_entire line 51