OAI/NumberTheory/CubicMoment/Theta/CubicThetaProjectedSmoothMellin.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Mellin inversion for the literal primary-selected coefficients at every primary rational cusp.

  1. lemma OAI.CubicFirstMoment.cubicTheta_twisted_angular_bound line 13
  2. def OAI.CubicFirstMoment.cubicThetaSelectedAdditiveSum line 24
  3. theorem OAI.CubicFirstMoment.cubicThetaSelected_smooth_continued line 30