Commit 2026-03-06 17:09 6321788b

View on Github →

feat(Analysis/Complex/UpperHalfPlane): invariant measure (#34402) Add the invariant measure on the upper half-plane (& prove that it is indeed invariant). Also includes various minor improvements to upper half-plane & related code:

  • improve documentation of GeneralLinearGroup/FinTwo.lean
  • remove no-longer-needed coercion notation

Estimated changes

added def Complex.conjCAE
added theorem Complex.conjCAE_apply
deleted def Complex.conjCLE
deleted theorem Complex.conjCLE_coe
added theorem Complex.conjLIE_toCLE
added def UpperHalfPlane.J
added theorem UpperHalfPlane.J_sq
added theorem UpperHalfPlane.denom_J
added theorem UpperHalfPlane.det_J
added theorem UpperHalfPlane.sigma_J
added theorem UpperHalfPlane.val_J
added theorem UpperHalfPlane.J_smul
deleted def UpperHalfPlane.J
deleted theorem UpperHalfPlane.J_smul
deleted theorem UpperHalfPlane.J_sq
deleted theorem UpperHalfPlane.coe_J_smul
deleted theorem UpperHalfPlane.denom_J
deleted theorem UpperHalfPlane.det_J
deleted theorem UpperHalfPlane.sigma_J
deleted theorem UpperHalfPlane.val_J