OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedPrimarySeries.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite ramified factors separated from the remaining primary Fourier series. These are identities for the actual convergent Dirichlet sum, with no residue formula assumed.

  1. def OAI.CubicFirstMoment.cubicThetaPrimaryFourierTerm line 12
  2. def OAI.CubicFirstMoment.cubicThetaPrimaryFourierSeries line 17
  3. def OAI.CubicFirstMoment.cubicThetaRamifiedFactor line 20
  4. theorem OAI.CubicFirstMoment.cubicThetaRamifiedTerm_factor line 24
  5. theorem OAI.CubicFirstMoment.cubicThetaFrequencyDirichlet_primary_finite line 36