OAI/NumberTheory/CubicMoment/Transform/MetaplecticCommonBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The two complementary common-factor bounds in each retained metaplectic block. Both come from actual divisibility.

  1. lemma OAI.CubicFirstMoment.metaplecticCommonNorm_le_level line 12
  2. lemma OAI.CubicFirstMoment.metaplecticCommonNorm_nonneg line 25
  3. lemma OAI.CubicFirstMoment.metaplecticCommonNorm_le_geometric line 30
  4. lemma OAI.CubicFirstMoment.metaplectic_actual_coefficient_common_bound line 42