OAI/NumberTheory/CubicMoment/Theta/CubicThetaArithmeticEquation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual arithmetic remainder satisfies the same forced spectral operator as the continued global weak response.

  1. lemma OAI.CubicFirstMoment.second_sub line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaHyperbolicOperator_sub line 25
  3. lemma OAI.CubicFirstMoment.cubicThetaIncomingEisenstein_coordinate_contDiffAt line 42
  4. theorem OAI.CubicFirstMoment.cubicThetaArithmeticRemainder_equation line 61