OAI/NumberTheory/CubicMoment/Transform/MetaplecticUniformInverse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The signed-height estimate for the original angular Gauss sum. Both its completion and its inverse have been derived. The harmonic cube-divisor loss is absorbed by choosing its exponent first.

  1. theorem OAI.CubicFirstMoment.UniformLogWeights.metaplectic_inverted_angular_mean line 16