OAI/NumberTheory/CubicMoment/Theta/CubicThetaRegularHeatLow.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The small-time Mellin remainder is integrable and continuous at the critical exponent after subtracting the proved heat coefficient.

  1. def OAI.CubicFirstMoment.cubicThetaRegularHeatLow line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaRegularHeatLow_measurable line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaRegularHeatLow_bound line 22
  4. lemma OAI.CubicFirstMoment.cubicThetaRegularHeatLow_integrable line 34
  5. theorem OAI.CubicFirstMoment.cubicThetaRegularHeatLow_integral_tendsto line 43