OAI/NumberTheory/CubicMoment/Theta/CubicThetaZeroRadialMellin.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The constant-mode radial factor is an entire compact Mellin transform.

  1. lemma OAI.CubicFirstMoment.cubicThetaRadialTestWeight_star line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaRadialTestWeight_zero line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaRadialTestWeight_tsupport line 24
  4. theorem OAI.CubicFirstMoment.cubicThetaZeroRadialTest_mellin line 37
  5. theorem OAI.CubicFirstMoment.cubicThetaZeroRadialTest_entire line 71