OAI/NumberTheory/CubicMoment/Transform/MetaplecticSmoothBilinear.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The cubic-sieve bound applied to the original smooth angular Gauss sums, with the actual compact support and coefficient energies.

  1. lemma OAI.CubicFirstMoment.metaplectic_angular_bilinear_identity line 12
  2. theorem OAI.CubicFirstMoment.UniformLogWeights.metaplectic_smooth_bilinear line 28
  3. lemma OAI.CubicFirstMoment.metaplecticAngularSmoothSum_small line 66
  4. theorem OAI.CubicFirstMoment.UniformLogWeights.metaplectic_smooth_bilinear_all_lengths line 76