OAI/NumberTheory/CubicMoment/Theta/CubicThetaLocalQuotientMeasure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

On an injective quotient chart, hyperbolic measure downstairs equals hyperbolic measure upstairs. This follows by replacing the fundamental domain with the proved measurable extension of that chart.

  1. lemma OAI.CubicFirstMoment.cubicThetaQuotientMeasure_local_image line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaQuotientChart_measurable_image line 23
  3. lemma OAI.CubicFirstMoment.cubicThetaQuotientMeasure_chart line 38