OAI/NumberTheory/CubicMoment/Theta/CubicThetaEisensteinTorus.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual nonconstant Eisenstein Fourier series is a continuous function on its period torus. Its coefficients retain the arithmetic Dirichlet series and heat integral, including the zero-mode exclusion.

  1. def OAI.CubicFirstMoment.cubicThetaTorusRemainder line 19
  2. lemma OAI.CubicFirstMoment.cubicThetaTorusRemainder_summable line 22
  3. lemma OAI.CubicFirstMoment.cubicThetaNonzeroFrequencyTerm_phase line 28
  4. lemma OAI.CubicFirstMoment.cubicThetaTorusRemainder_real line 37
  5. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_torus line 51
  6. lemma OAI.CubicFirstMoment.cubicThetaTorusFourier_toLp line 60
  7. theorem OAI.CubicFirstMoment.cubicThetaTorusRemainder_coefficient line 66
  8. theorem OAI.CubicFirstMoment.cubicThetaTorusRemainder_mean_zero line 82