OAI/NumberTheory/CubicMoment/Theta/CubicThetaQuotientLocalFiniteness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The quotient's actual hyperbolic measure is locally finite. Small compact neighborhoods are lifted through the proved covering charts.

  1. instance OAI.CubicFirstMoment.cubicThetaQuotientMeasure_locallyFinite line 13
  2. instance OAI.CubicFirstMoment.cubicThetaQuotientMeasure_finiteOnCompacts line 26