# Documentation

Mathlib.Analysis.Complex.UpperHalfPlane.Basic

# The upper half plane and its automorphisms #

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

We furthermore equip it with the structure of a GLPos 2 ℝ action by fractional linear transformations.

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

The open upper half plane

Instances For
Instances For

Canonical embedding of the upper half-plane into ℂ.

Instances For
theorem UpperHalfPlane.ext {a : UpperHalfPlane} {b : UpperHalfPlane} (h : a = b) :
a = b
@[simp]
theorem UpperHalfPlane.ext_iff {a : UpperHalfPlane} {b : UpperHalfPlane} :
a = b a = b

Imaginary part

Instances For

Real part

Instances For
theorem UpperHalfPlane.ext' {a : UpperHalfPlane} {b : UpperHalfPlane} (hre : ) (him : ) :
a = b

Extensionality lemma in terms of UpperHalfPlane.re and UpperHalfPlane.im.

def UpperHalfPlane.mk (z : ) (h : 0 < z.im) :

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

Instances For
@[simp]
theorem UpperHalfPlane.coe_im (z : UpperHalfPlane) :
(z).im =
@[simp]
theorem UpperHalfPlane.coe_re (z : UpperHalfPlane) :
(z).re =
@[simp]
theorem UpperHalfPlane.mk_re (z : ) (h : 0 < z.im) :
= z.re
@[simp]
theorem UpperHalfPlane.mk_im (z : ) (h : 0 < z.im) :
= z.im
@[simp]
theorem UpperHalfPlane.coe_mk (z : ) (h : 0 < z.im) :
↑() = z
@[simp]
theorem UpperHalfPlane.mk_coe (z : UpperHalfPlane) (h : optParam (0 < (z).im) (_ : 0 < (z).im)) :
UpperHalfPlane.mk (z) h = z
def UpperHalfPlane.num (g : { x // x Matrix.GLPos (Fin 2) }) (z : UpperHalfPlane) :

Numerator of the formula for a fractional linear transformation

Instances For

Denominator of the formula for a fractional linear transformation

Instances For
theorem UpperHalfPlane.linear_ne_zero (cd : Fin 2) (z : UpperHalfPlane) (h : cd 0) :
↑(cd 0) * z + ↑(cd 1) 0

Fractional linear transformation, also known as the Moebius transformation

Instances For
theorem UpperHalfPlane.smulAux'_im (g : { x // x Matrix.GLPos (Fin 2) }) (z : UpperHalfPlane) :
().im = /

Fractional linear transformation, also known as the Moebius transformation

Instances For
theorem UpperHalfPlane.denom_cocycle (x : { x // x Matrix.GLPos (Fin 2) }) (y : { x // x Matrix.GLPos (Fin 2) }) (z : UpperHalfPlane) :
theorem UpperHalfPlane.mul_smul' (x : { x // x Matrix.GLPos (Fin 2) }) (y : { x // x Matrix.GLPos (Fin 2) }) (z : UpperHalfPlane) :

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

instance UpperHalfPlane.SLAction {R : Type u_1} [] [] :
def UpperHalfPlane.coe' :
{ x // x Matrix.GLPos (Fin 2) }
Instances For
@[simp]
theorem UpperHalfPlane.coe'_apply_complex {g : } {i : Fin 2} {j : Fin 2} :
↑(g i j) = ↑(g i j)
@[simp]
theorem UpperHalfPlane.det_coe' {g : } :
Matrix.det g = 1
theorem UpperHalfPlane.SLOnGLPos_smul_apply (s : ) (g : { x // x Matrix.GLPos (Fin 2) }) (z : UpperHalfPlane) :
(s g) z = (s * g) z
instance UpperHalfPlane.subgroupGLPos (Γ : ) :
SMul { x // x Γ } { x // x Matrix.GLPos (Fin 2) }
theorem UpperHalfPlane.subgroup_on_glpos_smul_apply (Γ : ) (s : { x // x Γ }) (g : { x // x Matrix.GLPos (Fin 2) }) (z : UpperHalfPlane) :
(s g) z = (s * g) z
instance UpperHalfPlane.subgroupSL (Γ : ) :
SMul { x // x Γ } ()
theorem UpperHalfPlane.subgroup_on_SL_apply (Γ : ) (s : { x // x Γ }) (g : ) (z : UpperHalfPlane) :
(s g) z = (s * g) z
theorem UpperHalfPlane.specialLinearGroup_apply {R : Type u_1} [] [] (g : ) (z : UpperHalfPlane) :
g z = UpperHalfPlane.mk ((↑(↑() (g 0 0)) * z + ↑(↑() (g 0 1))) / (↑(↑() (g 1 0)) * z + ↑(↑() (g 1 1)))) (_ : 0 < (↑(g z)).im)
@[simp]
theorem UpperHalfPlane.coe_smul (g : { x // x Matrix.GLPos (Fin 2) }) (z : UpperHalfPlane) :
↑(g z) =
@[simp]
theorem UpperHalfPlane.re_smul (g : { x // x Matrix.GLPos (Fin 2) }) (z : UpperHalfPlane) :
UpperHalfPlane.re (g z) = ().re
theorem UpperHalfPlane.im_smul (g : { x // x Matrix.GLPos (Fin 2) }) (z : UpperHalfPlane) :
UpperHalfPlane.im (g z) = ().im
@[simp]
theorem UpperHalfPlane.neg_smul (g : { x // x Matrix.GLPos (Fin 2) }) (z : UpperHalfPlane) :
-g z = g z
@[simp]
theorem UpperHalfPlane.sl_moeb (A : ) (z : UpperHalfPlane) :
A z = A z
theorem UpperHalfPlane.subgroup_moeb (Γ : ) (A : { x // x Γ }) (z : UpperHalfPlane) :
A z = A z
@[simp]
theorem UpperHalfPlane.subgroup_to_sl_moeb (Γ : ) (A : { x // x Γ }) (z : UpperHalfPlane) :
A z = A z
@[simp]
theorem UpperHalfPlane.SL_neg_smul (g : ) (z : UpperHalfPlane) :
-g z = g z
theorem UpperHalfPlane.c_mul_im_sq_le_normSq_denom (z : UpperHalfPlane) (g : ) :
(↑(Matrix.SpecialLinearGroup.toGLPos g) 1 0 * ) ^ 2 Complex.normSq (UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGLPos g) z)
theorem UpperHalfPlane.denom_apply (g : ) (z : UpperHalfPlane) :
UpperHalfPlane.denom (g) z = ↑(g 1 0) * z + ↑(g 1 1)
@[simp]
theorem UpperHalfPlane.coe_pos_real_smul (x : { x // 0 < x }) (z : UpperHalfPlane) :
↑(x z) = x z
@[simp]
theorem UpperHalfPlane.pos_real_im (x : { x // 0 < x }) (z : UpperHalfPlane) :
@[simp]
theorem UpperHalfPlane.pos_real_re (x : { x // 0 < x }) (z : UpperHalfPlane) :
@[simp]
theorem UpperHalfPlane.coe_vadd (x : ) (z : UpperHalfPlane) :
↑(x +ᵥ z) = x + z
@[simp]
theorem UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero (g : ) (hc : g 1 0 = 0) :
u v, (fun x x_1 => x x_1) g = (fun z => v +ᵥ z) fun z => u z
theorem UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero (g : ) (hc : g 1 0 0) :
u v w, (fun x x_1 => x x_1) g = (fun x x_1 => x +ᵥ x_1) w (fun x x_1 => x x_1) ModularGroup.S (fun x x_1 => x +ᵥ x_1) v (fun x x_1 => x x_1) u