# mathlibdocumentation

analysis.complex.upper_half_plane

# The upper half plane and its automorphisms #

This file defines upper_half_plane to be the upper half plane in ℂ.

We furthermore equip it with the structure of an SL(2,ℝ) action by fractional linear transformations.

We define the notation ℍ for the upper half plane available in the locale upper_half_plane so as not to conflict with the quaternions.

def upper_half_plane  :
Type

The open upper half plane

def upper_half_plane.im (z : ) :

Imaginary part

Equations
def upper_half_plane.re (z : ) :

Real part

Equations
@[simp]
theorem upper_half_plane.coe_im (z : ) :
z.im = z.im
@[simp]
theorem upper_half_plane.coe_re (z : ) :
z.re = z.re
theorem upper_half_plane.im_pos (z : ) :
0 < z.im
theorem upper_half_plane.ne_zero (z : ) :
z 0
@[simp]
def upper_half_plane.num (g : SL(2,)) (z : ) :

Numerator of the formula for a fractional linear transformation

Equations
@[simp]
def upper_half_plane.denom (g : SL(2,)) (z : ) :

Denominator of the formula for a fractional linear transformation

Equations
theorem upper_half_plane.linear_ne_zero (cd : fin 2) (z : ) (h : cd 0) :
((cd 0)) * z + (cd 1) 0
noncomputable def upper_half_plane.smul_aux' (g : SL(2,)) (z : ) :

Fractional linear transformation

Equations
noncomputable def upper_half_plane.smul_aux (g : SL(2,)) (z : ) :

Fractional linear transformation

Equations
theorem upper_half_plane.mul_smul' (x y : SL(2,)) (z : ) :
@[protected, instance]
noncomputable def upper_half_plane.mul_action  :

The action of SL(2, ℝ) on the upper half-plane by fractional linear transformations.

Equations
@[simp]
theorem upper_half_plane.coe_smul (g : SL(2,)) (z : ) :
(g z) =
@[simp]
theorem upper_half_plane.re_smul (g : SL(2,)) (z : ) :
(g z).re = .re
theorem upper_half_plane.im_smul (g : SL(2,)) (z : ) :
(g z).im = .im
@[simp]
theorem upper_half_plane.neg_smul (g : SL(2,)) (z : ) :
-g z = g z