OAI/NumberTheory/CubicMoment/Theta/CubicThetaForcingSeries.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual arithmetic forcing series is locally a finite sum, uniformly in the spectral parameter.

  1. def OAI.CubicFirstMoment.cubicThetaForcingTerm line 11
  2. def OAI.CubicFirstMoment.cubicThetaForcingSeries line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaForcingTerm_translate line 17
  4. theorem OAI.CubicFirstMoment.cubicThetaForcingSeries_automorphy line 33
  5. theorem OAI.CubicFirstMoment.cubicThetaForcingSeries_compact_sum line 43
  6. theorem OAI.CubicFirstMoment.cubicThetaForcingSeries_analytic line 59