OAI/NumberTheory/CubicMoment/Theta/CubicThetaScalarRankinKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The positive truncated scalar kernel on the actual arithmetic quotient. Its residue is known before any integration against the theta norm.

  1. lemma OAI.CubicFirstMoment.cubicThetaScalarHeightCutoff_nonneg line 20
  2. lemma OAI.CubicFirstMoment.cubicThetaScalarHeightCutoff_invariant line 28
  3. lemma OAI.CubicFirstMoment.cubicThetaScalarHeightCutoff_point_measurable line 37
  4. def OAI.CubicFirstMoment.cubicThetaScalarRankinKernel line 50
  5. lemma OAI.CubicFirstMoment.cubicThetaScalarRankinKernel_measurable line 53
  6. lemma OAI.CubicFirstMoment.cubicThetaScalarRankinKernel_nonneg line 57
  7. theorem OAI.CubicFirstMoment.cubicThetaScalarRankinKernel_residue line 61