mathlib documentation

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]

Numerator of the formula for a fractional linear transformation

Equations
@[simp]

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

Fractional linear transformation

Equations
@[instance]

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

Equations
@[simp]