OAI/NumberTheory/CubicMoment/Theta/CubicThetaLevelReciprocity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Put the genuine primary-level theta transformation on a symmetric height scale, before Mellin integration.

  1. def OAI.CubicFirstMoment.cubicThetaLevelScale line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaLevelScale_pos line 13
  3. lemma OAI.CubicFirstMoment.cubicThetaLevelScale_reciprocal line 17
  4. def OAI.CubicFirstMoment.cubicThetaLevelConstant line 27
  5. theorem OAI.CubicFirstMoment.cubicThetaLevelAxis_reciprocity line 30