OAI/NumberTheory/CubicMoment/Theta/CubicThetaAngularDirichletContinuation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Entire continuation of the actual additive Dirichlet series in nonzero angular type. Reciprocal Gamma factors remove the Mellin completion without adding an analytic input.

  1. def OAI.CubicFirstMoment.cubicThetaAngularDirichletContinuation line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaAngularDirichletContinuation_entire line 16
  3. theorem OAI.CubicFirstMoment.cubicThetaAngularDirichletContinuation_eq line 31