OAI/NumberTheory/CubicMoment/Theta/CubicThetaEnergyResidue.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The Mellin pole of the actual nonconstant horizontal energy, retaining the squared Whittaker mass that will enter the geometric norm comparison.

  1. theorem OAI.CubicFirstMoment.cubicThetaArithmeticFourierEnergy_residue line 13