OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Both signed means of the literal radial completed sum, using the actual pole and the proved radial remainder. No Voronoi premise remains.

  1. theorem OAI.CubicFirstMoment.UniformLogWeights.cubicTheta_completed_signed_radial_mean line 14