OAI/NumberTheory/CubicMoment/Theta/CubicThetaInvertedFiniteFourier.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual finite Fourier coefficient of an inverted row is the middle primary twist already continued from the global Eisenstein series.

  1. def OAI.CubicFirstMoment.cubicThetaInvertedGaussCoefficient line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaInvertedGaussCoefficient_factor line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaInvertedGaussCoefficient_zero line 28
  4. lemma OAI.CubicFirstMoment.cubicThetaSymbol_three line 32
  5. def OAI.CubicFirstMoment.cubicThetaInvertedFrequencyDirichlet line 38
  6. lemma OAI.CubicFirstMoment.cubicThetaInvertedFrequencyDirichlet_eq line 41
  7. theorem OAI.CubicFirstMoment.cubicThetaRegularizedInvertedFrequency_right line 51