OAI/NumberTheory/CubicMoment/Theta/CubicThetaCircleNormalized.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Radius-normalized coefficient extraction, with a linear error in the radius.

  1. theorem OAI.CubicFirstMoment.cubicThetaCircleSeries_normalized_remainder line 14
  2. theorem OAI.CubicFirstMoment.cubicThetaCircleSeries_normalized_limit line 37