OAI/NumberTheory/CubicMoment/Theta/CubicThetaRowContinuation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Continuation of each individual Eisenstein row. Its nonzero modes are entire; the constant mode can have a pole only at s=1. This does not interchange continuation with the infinite sum over rows.

  1. theorem OAI.CubicFirstMoment.cubicThetaNonzeroFourierRow_entire line 14
  2. def OAI.CubicFirstMoment.cubicThetaRowContinuation line 30
  3. theorem OAI.CubicFirstMoment.cubicThetaRowContinuation_right line 35
  4. lemma OAI.CubicFirstMoment.cubicThetaFrequencyTerm_entire line 47
  5. theorem OAI.CubicFirstMoment.cubicThetaRowContinuation_differentiableAt line 56