OAI/NumberTheory/CubicMoment/Theta/CubicThetaArithmeticSection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The arithmetic Eisenstein-minus-incoming difference is a genuine continuous automorphic section in the initial convergence half-plane.

  1. lemma OAI.CubicFirstMoment.cubicThetaArithmeticRemainder_continuousAt line 13
  2. def OAI.CubicFirstMoment.cubicThetaArithmeticSection line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaArithmeticSection_norm line 29