OAI/NumberTheory/CubicMoment/Theta/CubicThetaAngularFunctionalEquation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The functional equation for the actual continued additive angular Dirichlet series. Gamma cancellation is required only on the dual side.

  1. def OAI.CubicFirstMoment.cubicThetaAngularUncompletion line 10
  2. def OAI.CubicFirstMoment.cubicThetaAngularCompletion line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaAngular_completion_cancel line 19
  4. lemma OAI.CubicFirstMoment.cubicThetaAngularDirichletContinuation_factor line 41
  5. lemma OAI.CubicFirstMoment.cubicThetaAngularDirichletContinuation_complete line 47
  6. theorem OAI.CubicFirstMoment.cubicThetaLevelAngularCompleted_paired line 56
  7. theorem OAI.CubicFirstMoment.cubicThetaAngularDirichletContinuation_functional line 70