OAI/NumberTheory/CubicMoment/Theta/CubicThetaAveragedHeat.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Averaging the dilated heat kernel against a fixed radial test preserves exponential decay at both endpoints of its Mellin variable.

  1. def OAI.CubicFirstMoment.cubicThetaAveragedHeat line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaLinearHeat_average_bound line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaDoubleHeat_norm_le_one line 31
  4. lemma OAI.CubicFirstMoment.cubicThetaAveragedHeat_integrable line 38
  5. lemma OAI.CubicFirstMoment.cubicThetaAveragedHeat_bound line 51
  6. lemma OAI.CubicFirstMoment.cubicThetaAveragedHeat_continuous line 62
  7. lemma OAI.CubicFirstMoment.cubicThetaAveragedHeat_top line 83
  8. lemma OAI.CubicFirstMoment.cubicThetaAveragedHeat_bottom line 92
  9. lemma OAI.CubicFirstMoment.cubicThetaAveragedHeat_mellinConvergent line 99
  10. theorem OAI.CubicFirstMoment.cubicThetaAveragedHeat_mellin_entire line 106