OAI/NumberTheory/CubicMoment/Transform/MetaplecticUniformTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Far-left truncation of the literal angular Voronoi series. The absolute coefficient mass is derived from the published theta support, and the height growth is derived from finite Gamma recurrence.

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