OAI/NumberTheory/CubicMoment/Theta/CubicThetaScalarHeightSeed.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The sharp scalar height cutoff has an actual half-open strip seed.

  1. def OAI.CubicFirstMoment.cubicThetaScalarHeightWeight line 11
  2. def OAI.CubicFirstMoment.cubicThetaScalarHeightSeed line 13
  3. lemma OAI.CubicFirstMoment.cubicThetaScalarHeightWeight_nonneg line 16
  4. lemma OAI.CubicFirstMoment.cubicThetaScalarHeightSeed_nonneg line 23
  5. lemma OAI.CubicFirstMoment.cubicThetaScalarHeightSeed_translate line 30
  6. lemma OAI.CubicFirstMoment.cubicThetaScalarHeightSeed_translation_hasSum line 38
  7. lemma OAI.CubicFirstMoment.cubicThetaScalarHeightSeed_group_summable line 50
  8. theorem OAI.CubicFirstMoment.cubicThetaScalarHeightSeed_group_sum line 70