OAI/NumberTheory/CubicMoment/Theta/CubicThetaArithmeticResolvent.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The continued global resolvent is the literal arithmetic Eisenstein remainder on its initial half-plane of absolute convergence.

  1. lemma OAI.CubicFirstMoment.cubicThetaArithmeticEnergy_eq_continued line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaArithmeticL2_eq_forcedResolvent line 24