Affine maps of the upper half-plane: dilations and moving I to a given point

The dilation Matrix.SpecialLinearGroup.dilation s acts on ℍ as z ↦ exp s * z (TauCeti.UpperHalfPlane.coe_dilation_smul). For P : ℍ, the affine map UpperHalfPlane.toPoint P : z ↦ P.im * z + P.re is the element of PSL(2, ℝ) given by a dilation followed by a real translation; it sends I to P (UpperHalfPlane.toPoint_smul_I). This file records its action, the action of its inverse, and its derivative.

theorem TauCeti.UpperHalfPlane.coe_dilation_smul (s : ℝ) (z : UpperHalfPlane) : ↑(Matrix.SpecialLinearGroup.dilation s • z) = ↑(Real.exp s) * ↑z

dilation s acts on ℍ as z ↦ exp s * z.

noncomputable def UpperHalfPlane.toPoint (P : UpperHalfPlane) : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

The affine map z ↦ P.im * z + P.re, an element of PSL(2, ℝ) sending I to P.

Equations

• P.toPoint = Matrix.ProjectiveSpecialLinearGroup.upperRightHom P.re * ↑(Matrix.SpecialLinearGroup.dilation (Real.log P.im))

theorem UpperHalfPlane.coe_toPoint_smul (P z : UpperHalfPlane) : ↑(P.toPoint • z) = ↑P.im * ↑z + ↑P.re

toPoint P acts on ℍ as z ↦ P.im * z + P.re.

@[simp]

theorem UpperHalfPlane.toPoint_smul_I (P : UpperHalfPlane) : P.toPoint • I = P

toPoint P sends I to P.

theorem UpperHalfPlane.coe_toPoint_inv_smul (P z : UpperHalfPlane) : ↑(P.toPoint⁻¹ • z) = (↑z - ↑P.re) / ↑P.im

The inverse of toPoint P acts on ℍ as z ↦ (z - P.re) / P.im.

theorem UpperHalfPlane.smulDeriv_toPoint (P z : UpperHalfPlane) : P.toPoint.smulDeriv z = ↑P.im

The derivative of the affine map toPoint P is P.im.

theorem UpperHalfPlane.re_toPoint_inv_smul (P z : UpperHalfPlane) : (P.toPoint⁻¹ • z).re = (z.re - P.re) / P.im

The real part of the normalised point (toPoint P)⁻¹ • z.

theorem UpperHalfPlane.normSq_toPoint_inv_smul (P z : UpperHalfPlane) : Complex.normSq ↑(P.toPoint⁻¹ • z) = Complex.normSq (↑z - ↑P.re) / P.im ^ 2

The norm-square of the normalised point (toPoint P)⁻¹ • z.