OAI/NumberTheory/CubicMoment/Theta/CubicThetaProjectedDirichlet.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Entire continued Dirichlet series for the actual primary-projected cusp pair, with the initial series fixed by the literal coefficients.

  1. lemma OAI.CubicFirstMoment.cubicThetaBoundedScaledAxis_mellin line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaProjectedAngularCompleted_initial line 26
  3. lemma OAI.CubicFirstMoment.cubicThetaSelectedAngularCompleted_initial line 45
  4. def OAI.CubicFirstMoment.cubicThetaProjectedDirichlet line 64
  5. def OAI.CubicFirstMoment.cubicThetaSelectedDirichlet line 69
  6. lemma OAI.CubicFirstMoment.cubicThetaAngularUncompletion_entire line 74
  7. theorem OAI.CubicFirstMoment.cubicThetaProjectedDirichlet_entire line 87
  8. theorem OAI.CubicFirstMoment.cubicThetaSelectedDirichlet_entire line 93
  9. lemma OAI.CubicFirstMoment.cubicThetaAngular_initial_gamma line 99
  10. theorem OAI.CubicFirstMoment.cubicThetaProjectedDirichlet_initial line 106
  11. theorem OAI.CubicFirstMoment.cubicThetaSelectedDirichlet_initial line 118