OAI/NumberTheory/CubicMoment/Theta/CubicThetaCircleSeries.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Small-circle coefficient extraction for an absolutely convergent Fourier series. Only the zeroth, selected and next absolute frequency moments are used.

  1. def OAI.CubicFirstMoment.cubicThetaCircleSeries line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaCircleSeries_continuous line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaCircleSeries_coefficient line 27
  4. theorem OAI.CubicFirstMoment.cubicThetaCircleSeries_remainder line 56