OAI/NumberTheory/CubicMoment/Theta/CubicThetaForcedResolvent.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The global resolvent applied to the literal incoming arithmetic forcing. Identification with the Eisenstein remainder is a separate step.

  1. def OAI.CubicFirstMoment.cubicThetaForcedResolvent line 13
  2. theorem OAI.CubicFirstMoment.cubicThetaForcedResolvent_meromorphic line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaForcedResolvent_automorphic line 21
  4. theorem OAI.CubicFirstMoment.cubicThetaForcedResolvent_weak line 28