OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeDirichlet.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact cube-index recurrence of the convergent Eisenstein series. The prime-free term is retained explicitly; no claim about its residue is made by this initial-half-plane identity.

  1. theorem OAI.CubicFirstMoment.cubicThetaFrequencyDirichlet_five_terms line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaFrequencyDirichlet_cube_recurrence line 27