OAI/NumberTheory/CubicMoment/Theta/CubicThetaProperAction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual Eisenstein and principal-group actions are properly discontinuous. This supplies the topological quotient needed for global cusp gluing from proved compact-chart transport bounds.

  1. instance OAI.CubicFirstMoment.cubicThetaPoint_topology line 14
  2. instance OAI.CubicFirstMoment.cubicThetaPoint_t2 line 17
  3. instance OAI.CubicFirstMoment.cubicThetaPoint_secondCountable line 20
  4. instance OAI.CubicFirstMoment.cubicThetaFullPointAction line 23
  5. lemma OAI.CubicFirstMoment.cubicThetaFullPointAction_apply line 26
  6. instance OAI.CubicFirstMoment.cubicThetaFullPointAction_continuous line 29
  7. instance OAI.CubicFirstMoment.cubicThetaFullPointAction_properlyDiscontinuous line 40
  8. lemma OAI.CubicFirstMoment.cubicThetaPrincipalPointAction_properlyDiscontinuous line 57