OAI/NumberTheory/CubicMoment/Theta/CubicThetaInvertedFourier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The full actual inverted Eisenstein series and its zero-frequency row term. The scalar continuation retains the exact archimedean factor.

  1. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_inverted_fourier_rows line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaInverted_zero_row_factor line 29
  3. def OAI.CubicFirstMoment.cubicThetaInvertedConstantMode line 53
  4. theorem OAI.CubicFirstMoment.cubicThetaInvertedConstantMode_eq line 59
  5. def OAI.CubicFirstMoment.cubicThetaInvertedModeContinuation line 71
  6. theorem OAI.CubicFirstMoment.cubicThetaInvertedModeContinuation_right line 74