OAI/NumberTheory/CubicMoment/Theta/CubicThetaFourierRemainder.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Separation of the actual Eisenstein series into its constant mode and nonzero Fourier rows on the initial half-plane.

  1. def OAI.CubicFirstMoment.cubicThetaConstantRow line 13
  2. def OAI.CubicFirstMoment.cubicThetaNonzeroFourierRow line 19
  3. lemma OAI.CubicFirstMoment.cubicThetaRowFourier_summable line 27
  4. lemma OAI.CubicFirstMoment.cubicThetaRowFourierCoefficient_zero line 36
  5. lemma OAI.CubicFirstMoment.cubicThetaEisensteinRow_split line 40
  6. lemma OAI.CubicFirstMoment.cubicThetaConstantRow_eq line 58
  7. lemma OAI.CubicFirstMoment.cubicThetaConstantRow_summable line 68
  8. lemma OAI.CubicFirstMoment.cubicThetaNonzeroFourierRow_eq line 74
  9. lemma OAI.CubicFirstMoment.cubicThetaNonzeroFourierRow_summable line 84
  10. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_constant_add_nonzero line 93