OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamanujanProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual finite Ramanujan average is precisely the squarefree local Euler coefficient in the published Voronoi formula.

  1. lemma OAI.CubicFirstMoment.cubicThetaRamanujan_prod line 13
  2. theorem OAI.CubicFirstMoment.cubicThetaRamanujan_squarefree line 30
  3. lemma OAI.CubicFirstMoment.cubicTheta_sum_eq_units line 43
  4. theorem OAI.CubicFirstMoment.cubicThetaRamanujan_units line 57