OAI/NumberTheory/CubicMoment/Transform/MetaplecticKernelIntegrability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Absolute convergence of the literal metaplectic Mellin kernel, derived from the proved Gamma strip bound and the smooth weight's rapid decay.

  1. theorem OAI.CubicFirstMoment.metaplecticKernel_integrable line 13