OAI/NumberTheory/CubicMoment/Transform/MetaplecticUniformRadialInverse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Direct radial height means from Voronoi, ordinary mean value and finite inverse completion. The pole contributes a summable cube-divisor tail.

  1. theorem OAI.CubicFirstMoment.UniformLogWeights.metaplectic_inverted_radial_mean line 15