OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialVoronoi.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual radial primary-selected Voronoi formula. Its pole term contains the residue computed from the actual arithmetic theta section.

  1. theorem OAI.CubicFirstMoment.cubicThetaSelected_radial_voronoi_far line 14
  2. theorem OAI.CubicFirstMoment.cubicThetaSelected_radial_voronoi line 41