OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspStrip.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A half-open three-Eisenstein period cell gives a genuinely injective high cusp strip in the arithmetic quotient. Boundary points retain their unique representatives.

  1. def OAI.CubicFirstMoment.cubicThetaPeriodCoordinates line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaPeriodCoordinates_continuous line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaPeriodCoordinates_translate line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaPeriodCoordinates_injective line 32
  5. def OAI.CubicFirstMoment.cubicThetaCuspStrip line 37
  6. lemma OAI.CubicFirstMoment.cubicThetaCuspStrip_measurable line 41
  7. lemma OAI.CubicFirstMoment.halfOpen_integer_unique line 57
  8. theorem OAI.CubicFirstMoment.cubicThetaCuspStrip_injective line 66
  9. instance OAI.CubicFirstMoment.cubicThetaPoint_polish line 94
  10. lemma OAI.CubicFirstMoment.cubicThetaQuotient_injective_image_measurable line 97
  11. lemma OAI.CubicFirstMoment.cubicThetaCuspStrip_image_measurable line 102