OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeEulerStep.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The exact first local Euler step for a frequency prime to p. The two remaining series retain their actual cubic twists on the prime-free rows.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeFreeTerm line 10
  2. def OAI.CubicFirstMoment.cubicThetaPrimeFreeDirichlet line 14
  3. def OAI.CubicFirstMoment.cubicThetaPrimeFirstFactor line 17
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerTerm_zero line 20
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerTerm_one line 26
  6. theorem OAI.CubicFirstMoment.cubicThetaFrequencyDirichlet_primeEulerStep line 39