OAI/NumberTheory/CubicMoment/Theta/CubicThetaTranslatedCuspStrip.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Every arithmetic cusp strip remains injective after an integral Mobius transformation. Normality of the actual level-three group and invariance of hyperbolic measure give the exact transported integrals.

  1. def OAI.CubicFirstMoment.cubicThetaPrincipalConjugate line 13
  2. def OAI.CubicFirstMoment.cubicThetaTranslatedCuspStrip line 22
  3. lemma OAI.CubicFirstMoment.cubicThetaTranslatedCuspStrip_measurable line 25
  4. lemma OAI.CubicFirstMoment.cubicThetaTranslatedCuspStrip_injective line 29
  5. lemma OAI.CubicFirstMoment.cubicThetaSmul_map_restrict line 41
  6. lemma OAI.CubicFirstMoment.cubicThetaTranslatedCuspStrip_integral line 54
  7. lemma OAI.CubicFirstMoment.cubicThetaTranslatedCuspStrip_integrable line 67