OAI/NumberTheory/CubicMoment/Theta/CubicThetaProjectedAngularMellin.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Entire Mellin continuation for the two actual coefficient families in the primary-projected rational-cusp transformation.

  1. def OAI.CubicFirstMoment.cubicThetaProjectedAngularAxis line 15
  2. def OAI.CubicFirstMoment.cubicThetaSelectedAngularAxis line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaSelectedCoefficient_arithmetic_bound line 24
  4. theorem OAI.CubicFirstMoment.cubicThetaProjectedAngularAxis_functional line 29
  5. def OAI.CubicFirstMoment.cubicThetaProjectedAngularCompleted line 42
  6. theorem OAI.CubicFirstMoment.cubicThetaProjectedAngular_mellin line 48
  7. theorem OAI.CubicFirstMoment.cubicThetaProjectedAngularCompleted_entire line 60
  8. theorem OAI.CubicFirstMoment.cubicThetaProjectedAngularCompleted_functional line 72
  9. theorem OAI.CubicFirstMoment.cubicThetaProjectedAngular_actual_entire line 81