OAI/NumberTheory/CubicMoment/Theta/CubicThetaProjectedPlane.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual projected cusp expansion supports the same angular extraction as the original theta series, with its own literal coefficients.

  1. lemma OAI.CubicFirstMoment.cubicThetaProjectedCoefficient_arithmetic_bound line 15
  2. def OAI.CubicFirstMoment.cubicThetaProjectedPlane line 21
  3. def OAI.CubicFirstMoment.cubicThetaPrimaryCuspCenter line 26
  4. def OAI.CubicFirstMoment.cubicThetaPrimaryDualCenter line 28
  5. lemma OAI.CubicFirstMoment.cubicThetaSelected_projected_plane line 31
  6. lemma OAI.CubicFirstMoment.cubicThetaProjectedPlane_circle_coefficient line 44
  7. theorem OAI.CubicFirstMoment.cubicThetaProjectedPlane_circle_limit line 64