OAI/NumberTheory/CubicMoment/Theta/CubicThetaGramKernelScaling.lean
3 declarations, 0 contain sorry, 0 declared as axioms
Exact archimedean scaling of the diagonal prime-power Gram kernels. The denominator transforms by c/a; all frequencies and radial factors are retained.
- lemma
OAI.CubicFirstMoment.cubicThetaRadius_divideline 12 - lemma
OAI.CubicFirstMoment.cubicThetaInversion_double_scaleline 18 - lemma
OAI.CubicFirstMoment.cubicThetaGramInversionKernel_scaleline 41