OAI/NumberTheory/CubicMoment/Theta/CubicThetaZeroFourier.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The zero Fourier mode of the actual Eisenstein row expansion, including its exact archimedean factor.

  1. lemma OAI.CubicFirstMoment.cubicThetaDualHeat_zero_integral line 13
  2. lemma OAI.CubicFirstMoment.cubicTheta_zero_height_factor line 26
  3. lemma OAI.CubicFirstMoment.cubicTheta_zero_row_factor line 44
  4. def OAI.CubicFirstMoment.cubicThetaEisensteinConstantMode line 64
  5. theorem OAI.CubicFirstMoment.cubicThetaEisensteinConstantMode_eq line 70