OAI/NumberTheory/CubicMoment/Transform/MetaplecticTailLevel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The long completion coefficient separates exactly into one fixed factor and a coprimality restriction on the original outer coefficients.

  1. def OAI.CubicFirstMoment.metaplecticTailScalar line 13
  2. def OAI.CubicFirstMoment.metaplecticTailOuter line 16
  3. lemma OAI.CubicFirstMoment.metaplectic_tail_level_factor line 19
  4. lemma OAI.CubicFirstMoment.metaplecticTailOuter_energy_le line 33
  5. theorem OAI.CubicFirstMoment.metaplecticTailScalar_bound line 44