OAI/NumberTheory/CubicMoment/Theta/CubicThetaLevelAngularCompleted.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Entire completed additive angular Dirichlet series and their paired Mellin identity.

  1. theorem OAI.CubicFirstMoment.cubicThetaLevelAngularCompleted_functional line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaLevelAngular_actual_entire line 21
  3. theorem OAI.CubicFirstMoment.cubicThetaLevelAngularCompleted_dirichlet line 33