OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspStripReduction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Horizontal reduction into the exact half-open cusp strip uses the actual principal translations. It is compatible with every arithmetic cusp through the proved conjugation in the level-three group.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrincipalTranslation_coordinates line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaCuspStrip_reduction line 23
  3. def OAI.CubicFirstMoment.cubicThetaCuspNeighborhood line 42
  4. lemma OAI.CubicFirstMoment.cubicThetaCuspNeighborhood_measurable line 45
  5. lemma OAI.CubicFirstMoment.cubicThetaCuspNeighborhood_mem_of_height line 50