OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootAverageIdentity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Saturation of the actual trace bound identifies the zero-frequency residue with its once-cubic dilation.

  1. theorem OAI.CubicFirstMoment.cubicThetaArithmeticResidue_average_identity line 10