OAI/NumberTheory/CubicMoment/Transform/MetaplecticRetainedKernel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The complete retained frequency estimate passes through the actual critical-line Mellin kernel with its common, integrable weight.

  1. theorem OAI.CubicFirstMoment.metaplectic_actual_retained_kernel line 14