OAI/NumberTheory/CubicMoment/Estimates/IdealHeatTheta.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The normalized theta series whose Mellin transform has the angular Gamma shift. Its defining sum runs over all nonzero ideals.

  1. def OAI.CubicFirstMoment.idealHeatTheta line 11
  2. lemma OAI.CubicFirstMoment.idealHeatTheta_term_bound line 14
  3. lemma OAI.CubicFirstMoment.idealHeatTheta_summable line 30
  4. lemma OAI.CubicFirstMoment.idealHeatTheta_continuousOn_ray line 41
  5. lemma OAI.CubicFirstMoment.idealHeatTheta_continuousOn line 62
  6. lemma OAI.CubicFirstMoment.idealHeatTheta_norm_bound line 70
  7. lemma OAI.CubicFirstMoment.idealHeatTheta_isBigO_rpow line 106