OAI/NumberTheory/CubicMoment/Theta/CubicThetaForcedCusp.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual arithmetic continuation restricted to the high cusp. Both its meromorphic dependence and its initial pointwise representative are retained in the L2 strip space.

  1. def OAI.CubicFirstMoment.cubicThetaArithmeticFiniteEnergy line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaArithmeticFiniteEnergy_embedding line 18
  3. def OAI.CubicFirstMoment.cubicThetaForcedCusp line 22
  4. lemma OAI.CubicFirstMoment.cubicThetaForcedEnergy_meromorphic line 26
  5. theorem OAI.CubicFirstMoment.cubicThetaForcedCusp_meromorphic line 38
  6. lemma OAI.CubicFirstMoment.cubicThetaForcedCusp_right line 42
  7. lemma OAI.CubicFirstMoment.cubicThetaForcedCusp_coe line 47
  8. theorem OAI.CubicFirstMoment.cubicThetaForcedCusp_residue_closed line 53
  9. theorem OAI.CubicFirstMoment.cubicThetaForcedCusp_residue line 60