OAI/NumberTheory/CubicMoment/Theta/CubicThetaScalarHeightCutoff.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Removing the finitely many rows above height one preserves the scalar Eisenstein pole. The remaining positive kernel is the one used in the Rankin integral of the square-integrable theta section.

  1. def OAI.CubicFirstMoment.cubicThetaScalarHeightCutoff line 15
  2. def OAI.CubicFirstMoment.cubicThetaScalarHeightHigh line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaScalarHeightCutoff_summable line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaScalarHeightHigh_continuous line 34
  5. lemma OAI.CubicFirstMoment.cubicThetaScalarHeightHigh_summable line 56
  6. lemma OAI.CubicFirstMoment.cubicThetaScalarHeightCutoff_split line 66
  7. theorem OAI.CubicFirstMoment.cubicThetaScalarHeightCutoff_residue line 79