OAI/NumberTheory/CubicMoment/Theta/CubicThetaAveragedVoronoi.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A concrete finite character average of the proved angular additive Voronoi formula. The coefficient is the actual finite cusp average; further local/Moebius simplification is kept separate.

  1. def OAI.CubicFirstMoment.cubicThetaResidueDualCoefficient line 13
  2. def OAI.CubicFirstMoment.cubicThetaResidueDualTerm line 21
  3. theorem OAI.CubicFirstMoment.cubicThetaResidue_voronoi line 28