OAI/NumberTheory/CubicMoment/Theta/CubicThetaResidueWhittaker.lean
2 declarations, 0 contain sorry, 0 declared as axioms
The actual spectral residue observations have the same fixed Whittaker kernel as the explicit arithmetic theta expansion.
- lemma
OAI.CubicFirstMoment.cubicThetaPoleHeat_whittakerline 13 - lemma
OAI.CubicFirstMoment.cubicThetaPoleRadialTest_whittakerline 56