OAI/NumberTheory/CubicMoment/Transform/MetaplecticTrivialSum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A literal point-count bound for the original smooth angular Gauss sum, valid also below the first nonzero norm.

  1. theorem OAI.CubicFirstMoment.metaplecticAngularSmoothSum_trivial line 13