OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveRadialMellin.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The full positive-height radial Fourier factor is entire. All integral interchanges retain the positive cutoff rather than discarding it.

  1. lemma OAI.CubicFirstMoment.cubicThetaPositiveRadialMellin_integrable line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPositiveRadialTest_dilated line 32
  3. theorem OAI.CubicFirstMoment.cubicThetaPositiveRadialTest_mellin line 50
  4. theorem OAI.CubicFirstMoment.cubicThetaPositiveRadialTest_entire line 80