OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimitiveKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A positive full-group kernel majorizing the principal scalar kernel. Its right action allows the estimate to be proved in one Siegel set.

  1. lemma OAI.CubicFirstMoment.CubicThetaPrimitiveRow.norm_le_denominator line 13
  2. lemma OAI.CubicFirstMoment.CubicThetaPrimitiveRow.height_le line 24
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimitiveHeight_summable line 32
  4. def OAI.CubicFirstMoment.cubicThetaPrimitiveKernel line 59
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimitiveKernel_summable line 62
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimitiveKernel_invariant line 75
  7. lemma OAI.CubicFirstMoment.cubicThetaScalarHeightCutoff_le_primitive line 84