OAI/NumberTheory/CubicMoment/Theta/CubicThetaHorizontalDomain.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The literal half-open level-three cell is a fundamental domain for horizontal translations. This is the measure bridge for Hecke constant modes.

  1. def OAI.CubicFirstMoment.CubicThetaPeriodGroup line 11
  2. instance OAI.CubicFirstMoment.(instance at line 13) line 13
  3. instance OAI.CubicFirstMoment.(instance at line 14) line 14
  4. instance OAI.CubicFirstMoment.cubicThetaPeriodGroup_action line 18
  5. instance OAI.CubicFirstMoment.cubicThetaPeriodGroup_continuous line 27
  6. instance OAI.CubicFirstMoment.cubicThetaPeriodGroup_measure line 32
  7. theorem OAI.CubicFirstMoment.cubicThetaHorizontalCell_unique line 37
  8. theorem OAI.CubicFirstMoment.cubicThetaHorizontalCell_fundamental line 68