OAI/NumberTheory/CubicMoment/Transform/MetaplecticCodeDyads.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The exact norm dyad of each free variable after fixing the supported parameters in the retained Voronoi sum.

  1. abbrev OAI.CubicFirstMoment.MetaplecticDyadPrefix line 12
  2. def OAI.CubicFirstMoment.metaplecticCodePrefix line 14
  3. def OAI.CubicFirstMoment.metaplecticFreeScale line 17
  4. lemma OAI.CubicFirstMoment.metaplecticFreeScale_pos line 20
  5. lemma OAI.CubicFirstMoment.metaplectic_prefix_frequency line 29
  6. lemma OAI.CubicFirstMoment.metaplectic_code_frequency line 41
  7. lemma OAI.CubicFirstMoment.metaplectic_free_dyad line 48
  8. lemma OAI.CubicFirstMoment.metaplectic_free_length_one line 61
  9. lemma OAI.CubicFirstMoment.metaplecticFreeScale_lower line 71
  10. lemma OAI.CubicFirstMoment.metaplectic_free_length_upper line 89