OAI/NumberTheory/CubicMoment/Theta/CubicThetaMobiusAction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Composition and positive-height action for the hyperbolic matrices used in the cubic theta transformation.

  1. lemma OAI.CubicFirstMoment.cubicThetaMobiusDenominator_comp line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaHermitian_comp line 25
  3. theorem OAI.CubicFirstMoment.cubicThetaMobius_comp line 38
  4. lemma OAI.CubicFirstMoment.cubicThetaMobius_one line 52
  5. def OAI.CubicFirstMoment.CubicThetaPoint line 57

    Source documentation

    Hyperbolic three-space in the coordinates of the manuscript.

    def CubicThetaPoint := {p : ℂ × ℝ // 0 < p.2}
  6. instance OAI.CubicFirstMoment.(instance at line 59) line 59