OAI/NumberTheory/CubicMoment/Transform/MetaplecticCompletedRadialMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Both signed means of the completed zero-mode sum, with its genuine pole retained. The remainder uses the proved short/long Voronoi estimates.

  1. theorem OAI.CubicFirstMoment.UniformLogWeights.metaplectic_completed_signed_radial_mean line 13