OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoefficientMellin.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Initial Mellin identity for the actual selected and projected coefficient families, with their horizontal phases retained.

  1. def OAI.CubicFirstMoment.cubicThetaCoefficientTwist line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaCoefficientTwist_norm line 13
  3. lemma OAI.CubicFirstMoment.cubicThetaCoefficientTwist_angular_series line 17
  4. theorem OAI.CubicFirstMoment.cubicThetaCoefficient_mellin line 30