OAI/NumberTheory/CubicMoment/Transform/MetaplecticLongDyads.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual long inverse sum has a finite, canonical norm-dyad partition. Each nonempty block lies above half the inverse cutoff.

  1. def OAI.CubicFirstMoment.metaplecticLongSupport line 13
  2. def OAI.CubicFirstMoment.metaplecticLongDyad line 17
  3. def OAI.CubicFirstMoment.metaplecticLongDyads line 20
  4. lemma OAI.CubicFirstMoment.metaplecticLongSupport_primary line 23
  5. lemma OAI.CubicFirstMoment.metaplecticLongSupport_norm line 29
  6. lemma OAI.CubicFirstMoment.metaplecticLongDyad_norm line 37
  7. lemma OAI.CubicFirstMoment.metaplecticLongDyad_cutoff line 46
  8. lemma OAI.CubicFirstMoment.metaplecticLongDyads_card line 52
  9. theorem OAI.CubicFirstMoment.metaplectic_long_completion_active line 64
  10. lemma OAI.CubicFirstMoment.metaplectic_long_dyad_partition line 83