OAI/NumberTheory/CubicMoment/Transform/MetaplecticNormDyads.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Canonical finite norm-dyad partition of the retained Voronoi pairs. The integral frequency d³n has norm exactly three times N(d³ν).

  1. def OAI.CubicFirstMoment.metaplecticIntegralFrequency line 13
  2. lemma OAI.CubicFirstMoment.metaplecticIntegralFrequency_ne_zero line 16
  3. lemma OAI.CubicFirstMoment.norm_metaplecticIntegralFrequency line 20
  4. def OAI.CubicFirstMoment.metaplecticNormDyadIndex line 31
  5. def OAI.CubicFirstMoment.metaplecticNormDyad line 34
  6. def OAI.CubicFirstMoment.metaplecticNormDyadLength line 38
  7. lemma OAI.CubicFirstMoment.metaplecticNormDyadLength_pos line 40
  8. lemma OAI.CubicFirstMoment.metaplectic_norm_dyad_bounds line 44
  9. lemma OAI.CubicFirstMoment.metaplectic_norm_dyad_partition line 57
  10. lemma OAI.CubicFirstMoment.metaplectic_norm_dyad_length_le line 68
  11. lemma OAI.CubicFirstMoment.metaplectic_norm_dyad_count line 78