OAI/NumberTheory/CubicMoment/Transform/MetaplecticCompletedPolynomial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact identification of the completed ideal polynomial with the original completed Gauss sum at every real height.

  1. lemma OAI.CubicFirstMoment.metaplectic_primal_weight_factor line 14
  2. lemma OAI.CubicFirstMoment.metaplectic_completed_ideal_fibers line 27
  3. lemma OAI.CubicFirstMoment.metaplectic_primal_weighted_fibers line 43
  4. theorem OAI.CubicFirstMoment.metaplectic_completed_ideal_polynomial line 68