OAI/NumberTheory/CubicMoment/Transform/MetaplecticTailCounting.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The literal grouped long-completion coefficient has the counting bound used in the low-height Type-I argument, on every norm dyad.

  1. lemma OAI.CubicFirstMoment.metaplectic_tail_counting_scale line 12
  2. theorem OAI.CubicFirstMoment.metaplectic_tail_dyad_counting line 26