OAI/NumberTheory/CubicMoment/Theta/CubicThetaCircleActual.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Small-circle coefficients of the actual fixed-height theta series. Both orientations retain their precise signed angular coefficients.

  1. def OAI.CubicFirstMoment.cubicThetaCircleOrder line 16
  2. def OAI.CubicFirstMoment.cubicThetaCircleMultiplier line 17
  3. def OAI.CubicFirstMoment.cubicThetaCircleFrequency line 18
  4. def OAI.CubicFirstMoment.cubicThetaSignedCircle line 20
  5. lemma OAI.CubicFirstMoment.cubicThetaCircleActual_series line 23
  6. lemma OAI.CubicFirstMoment.cubicThetaCircleActual_power line 33
  7. lemma OAI.CubicFirstMoment.cubicThetaCircleActual_power_norm line 48
  8. lemma OAI.CubicFirstMoment.cubicThetaCircleActual_summable line 57
  9. theorem OAI.CubicFirstMoment.cubicThetaCircleActual_remainder line 65