OAI/NumberTheory/CubicMoment/Transform/MetaplecticRadialDyadic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The radial dyadic height estimate in the polynomial range used by the prime decomposition. No metaplectic mean-square input is required.

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