OAI/NumberTheory/CubicMoment/Theta/CubicThetaJacobian.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual Mobius Jacobian has absolute determinant equal to the cube of the height ratio. Thus the hyperbolic volume density is invariant.

  1. abbrev OAI.CubicFirstMoment.TangentL2 line 13
  2. def OAI.CubicFirstMoment.tangentCoordinates line 14
  3. lemma OAI.CubicFirstMoment.tangent_norm_sq line 16
  4. lemma OAI.CubicFirstMoment.tangent_finrank line 22
  5. lemma OAI.CubicFirstMoment.cubicThetaMobius_abs_det line 26
  6. lemma OAI.CubicFirstMoment.cubicThetaMobius_volume_density line 66