# mathlib3documentation

analysis.complex.upper_half_plane.basic

# The upper half plane and its automorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]

The open upper half plane

Equations
Instances for upper_half_plane
@[protected, instance]
Equations
@[protected, instance]
def upper_half_plane.can_lift  :
(λ (z : ), 0 < z.im)
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) :
h).re = z.re
@[simp]
theorem upper_half_plane.mk_im (z : ) (h : 0 < z.im) :
h).im = z.im
@[simp]
theorem upper_half_plane.coe_mk (z : ) (h : 0 < z.im) :
h) = z
@[simp]
theorem upper_half_plane.mk_coe (z : upper_half_plane) (h : 0 < z.im := _) :
@[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]
noncomputable def upper_half_plane.mul_action  :

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

Equations
@[protected, instance]
noncomputable def upper_half_plane.SL_action {R : Type u_1} [comm_ring R] [ ] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
theorem upper_half_plane.subgroup_on_SL_apply (Γ : subgroup ) (s : Γ) (g : ) (z : upper_half_plane) :
(s g) z = (s * g) z
@[protected, instance]
theorem upper_half_plane.special_linear_group_apply {R : Type u_1} [comm_ring R] [ ] (g : R) (z : upper_half_plane) :
g z = upper_half_plane.mk (((g 0 0) * z + (g 0 1)) / ((g 1 0) * z + (g 1 1))) _
@[simp]
@[simp]
@[simp]
@[simp]
theorem upper_half_plane.sl_moeb (A : ) (z : upper_half_plane) :
A z = A z
theorem upper_half_plane.subgroup_moeb (Γ : subgroup ) (A : Γ) (z : upper_half_plane) :
A z = A z
@[simp]
theorem upper_half_plane.subgroup_to_sl_moeb (Γ : subgroup ) (A : Γ) (z : upper_half_plane) :
A z = A z
@[simp]
theorem upper_half_plane.SL_neg_smul (g : ) (z : upper_half_plane) :
-g z = g z
theorem upper_half_plane.denom_apply (g : ) (z : upper_half_plane) :
= (g 1 0) * z + (g 1 1)
@[protected, instance]
Equations
@[simp]
theorem upper_half_plane.coe_pos_real_smul (x : {x // 0 < x}) (z : upper_half_plane) :
(x z) = x z
@[simp]
theorem upper_half_plane.pos_real_im (x : {x // 0 < x}) (z : upper_half_plane) :
(x z).im = x * z.im
@[simp]
theorem upper_half_plane.pos_real_re (x : {x // 0 < x}) (z : upper_half_plane) :
(x z).re = x * z.re
@[protected, instance]
Equations
@[simp]
theorem upper_half_plane.coe_vadd (x : ) (z : upper_half_plane) :
(x +ᵥ z) = x + z
@[simp]
theorem upper_half_plane.vadd_re (x : ) (z : upper_half_plane) :
(x +ᵥ z).re = x + z.re
@[simp]
theorem upper_half_plane.vadd_im (x : ) (z : upper_half_plane) :
(x +ᵥ z).im = z.im
theorem upper_half_plane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero (g : ) (hc : g 1 0 = 0) :
(u : {x // 0 < x}) (v : ), = (λ (z : upper_half_plane), v +ᵥ z) λ (z : upper_half_plane), u z
theorem upper_half_plane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero (g : ) (hc : g 1 0 0) :
(u : {x // 0 < x}) (v w : ),