OAI/NumberTheory/CubicMoment/Theta/CubicThetaCircleExtraction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fourier coefficient estimates for the small-circle character expansion.

  1. lemma OAI.CubicFirstMoment.cubicThetaCirclePhase_continuous line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaCirclePhase_norm line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaCirclePhase_integrable line 24
  4. lemma OAI.CubicFirstMoment.cubicThetaCircleTaylor_continuous line 29
  5. theorem OAI.CubicFirstMoment.cubicThetaCirclePhase_coefficient_remainder line 36
  6. lemma OAI.CubicFirstMoment.cubicThetaCirclePhase_coefficient_norm line 47