OAI/NumberTheory/CubicMoment/Theta/CubicThetaFullEisensteinFourier.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual initial Eisenstein Fourier coefficient on every positive horosphere, including below the injective cusp.

  1. def OAI.CubicFirstMoment.cubicThetaEisensteinSection line 18
  2. def OAI.CubicFirstMoment.cubicThetaFullTorus line 26
  3. lemma OAI.CubicFirstMoment.cubicThetaFullTorus_real line 29
  4. lemma OAI.CubicFirstMoment.cubicThetaFullTorus_coefficient line 39
  5. lemma OAI.CubicFirstMoment.cubicThetaEisenstein_horizontal_coefficient line 52