OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialInverse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The literal radial Gauss sum inherits the proved two-sided mean by finite inverse completion. The pole contributes its summable divisor tail.

  1. theorem OAI.CubicFirstMoment.UniformLogWeights.cubicTheta_inverted_radial_mean line 15