OAI/NumberTheory/CubicMoment/Transform/MetaplecticBilinear.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual bilinear Gauss kernel is controlled by the proved cubic large sieve. This is the finite arithmetic step in the long Type-I tail.

  1. lemma OAI.CubicFirstMoment.metaplectic_bilinear_factor line 12
  2. lemma OAI.CubicFirstMoment.gauss_weight_energy line 25
  3. lemma OAI.CubicFirstMoment.metaplectic_bilinear_operator line 34
  4. theorem OAI.CubicFirstMoment.metaplectic_bilinear_sieve line 57