OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveAveragedHeat.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The radial Mellin kernel at an arbitrary positive cutoff. Its endpoint decay follows from the same double heat kernel, with rescaled parameters.

  1. def OAI.CubicFirstMoment.cubicThetaPositiveAveragedHeat line 13
  2. def OAI.CubicFirstMoment.cubicThetaPositiveRadialWeightMass line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaPositiveRadialWeight_integrable line 19
  4. lemma OAI.CubicFirstMoment.cubicThetaPositiveLinearHeat_bound line 32
  5. lemma OAI.CubicFirstMoment.cubicThetaPositiveDoubleHeat_norm_le_one line 46
  6. lemma OAI.CubicFirstMoment.cubicThetaPositiveAveragedHeat_integrable line 56
  7. lemma OAI.CubicFirstMoment.cubicThetaPositiveAveragedHeat_bound line 69
  8. lemma OAI.CubicFirstMoment.cubicThetaPositiveAveragedHeat_continuous line 80
  9. lemma OAI.CubicFirstMoment.cubicThetaPositiveAveragedHeat_top line 101
  10. lemma OAI.CubicFirstMoment.cubicThetaPositiveAveragedHeat_bottom line 112
  11. theorem OAI.CubicFirstMoment.cubicThetaPositiveAveragedHeat_mellin_entire line 120