OAI/NumberTheory/CubicMoment/Theta/CubicThetaQuotientMeasure.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The quotient Borel structure and intrinsic hyperbolic measure. The measure is independent of the measurable fundamental domain.

  1. lemma OAI.CubicFirstMoment.cubicThetaQuotient_measurable_iff line 12
  2. instance OAI.CubicFirstMoment.cubicThetaPrincipalPointMeasure_invariant line 24
  3. instance OAI.CubicFirstMoment.cubicThetaPrincipalGroup_countable line 29
  4. lemma OAI.CubicFirstMoment.cubicThetaQuotientMeasure_apply line 43
  5. lemma OAI.CubicFirstMoment.cubicThetaQuotientMeasure_independent line 49
  6. lemma OAI.CubicFirstMoment.cubicThetaQuotientMeasure_integral line 62