mathlib documentation

analysis.complex.upper_half_plane.basic

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 GL_pos 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.

@[protected, instance]
Equations

Imaginary part

Equations

Real part

Equations
def upper_half_plane.mk (z : ) (h : 0 < z.im) :

Constructor for upper_half_plane. It is useful if ⟨z, h⟩ makes Lean use a wrong typeclass instance.

Equations
@[simp]
@[simp]
@[simp]
theorem upper_half_plane.mk_re (z : ) (h : 0 < z.im) :
@[simp]
theorem upper_half_plane.mk_im (z : ) (h : 0 < z.im) :
@[simp]
theorem upper_half_plane.coe_mk (z : ) (h : 0 < z.im) :
@[simp]
@[simp]
noncomputable def upper_half_plane.num (g : (matrix.GL_pos (fin 2) )) (z : upper_half_plane) :

Numerator of the formula for a fractional linear transformation

Equations
@[simp]
noncomputable def upper_half_plane.denom (g : (matrix.GL_pos (fin 2) )) (z : upper_half_plane) :

Denominator of the formula for a fractional linear transformation

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

Fractional linear transformation, also known as the Moebius transformation

Equations

Fractional linear transformation, also known as the Moebius transformation

Equations
@[protected, instance]

The action of GL_pos 2 ℝ on the upper half-plane by fractional linear transformations.

Equations
@[protected, instance]
Equations
@[simp]