mathlib3 documentation

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.

source
@[protected, instance]
def upper_half_plane.has_coe  :
has_coe upper_half_plane ℂ
source
def upper_half_plane  :
Type

The open upper half plane

Equations
Instances for upper_half_plane
source
@[protected, instance]
def upper_half_plane.inhabited  :
inhabited upper_half_plane
Equations
source
@[protected, instance]
def upper_half_plane.can_lift  :
can_lift ℂ upper_half_plane coe (λ (z : ℂ), 0 < z.im)
Equations
source
def upper_half_plane.im (z : upper_half_plane) :
ℝ

Imaginary part

Equations
source
def upper_half_plane.re (z : upper_half_plane) :
ℝ

Real part

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

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

Equations
source
@[simp]
theorem upper_half_plane.coe_im (z : upper_half_plane) :
↑z.im = z.im
source
@[simp]
theorem upper_half_plane.coe_re (z : upper_half_plane) :
↑z.re = z.re
source
@[simp]
theorem upper_half_plane.mk_re (z : ℂ) (h : 0 < z.im) :
(upper_half_plane.mk z h).re = z.re
source
@[simp]
theorem upper_half_plane.mk_im (z : ℂ) (h : 0 < z.im) :
(upper_half_plane.mk z h).im = z.im
source
@[simp]
theorem upper_half_plane.coe_mk (z : ℂ) (h : 0 < z.im) :
↑(upper_half_plane.mk z h) = z
source
@[simp]
theorem upper_half_plane.mk_coe (z : upper_half_plane) (h : 0 < ↑z.im := _) :
upper_half_plane.mk ↑z h = z
source
theorem upper_half_plane.re_add_im (z : upper_half_plane) :
↑(z.re) + ↑(z.im) * complex.I = ↑z
source
theorem upper_half_plane.im_pos (z : upper_half_plane) :
0 < z.im
source
theorem upper_half_plane.im_ne_zero (z : upper_half_plane) :
z.im ≠ 0
source
theorem upper_half_plane.ne_zero (z : upper_half_plane) :
↑z ≠ 0
source
theorem upper_half_plane.norm_sq_pos (z : upper_half_plane) :
0 < ⇑complex.norm_sq ↑z
source
theorem upper_half_plane.norm_sq_ne_zero (z : upper_half_plane) :
⇑complex.norm_sq ↑z ≠ 0
source
theorem upper_half_plane.im_inv_neg_coe_pos (z : upper_half_plane) :
0 < (-↑z)⁻¹.im
source
@[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
source
@[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
source
theorem upper_half_plane.linear_ne_zero (cd : fin 2 → ℝ) (z : upper_half_plane) (h : cd ≠ 0) :
↑(cd 0) * ↑z + ↑(cd 1) ≠ 0
source
theorem upper_half_plane.denom_ne_zero (g : ↥(matrix.GL_pos (fin 2) ℝ)) (z : upper_half_plane) :
upper_half_plane.denom g z ≠ 0
source
theorem upper_half_plane.norm_sq_denom_pos (g : ↥(matrix.GL_pos (fin 2) ℝ)) (z : upper_half_plane) :
0 < ⇑complex.norm_sq (upper_half_plane.denom g z)
source
theorem upper_half_plane.norm_sq_denom_ne_zero (g : ↥(matrix.GL_pos (fin 2) ℝ)) (z : upper_half_plane) :
⇑complex.norm_sq (upper_half_plane.denom g z) ≠ 0
source
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
source
theorem upper_half_plane.smul_aux'_im (g : ↥(matrix.GL_pos (fin 2) ℝ)) (z : upper_half_plane) :
(upper_half_plane.smul_aux' g z).im = ↑g.det * z.im / ⇑complex.norm_sq (upper_half_plane.denom g z)
source
noncomputable def upper_half_plane.smul_aux (g : ↥(matrix.GL_pos (fin 2) ℝ)) (z : upper_half_plane) :
upper_half_plane

Fractional linear transformation, also known as the Moebius transformation

Equations
source
theorem upper_half_plane.denom_cocycle (x y : ↥(matrix.GL_pos (fin 2) ℝ)) (z : upper_half_plane) :
upper_half_plane.denom (x * y) z = upper_half_plane.denom x (upper_half_plane.smul_aux y z) * upper_half_plane.denom y z
source
theorem upper_half_plane.mul_smul' (x y : ↥(matrix.GL_pos (fin 2) ℝ)) (z : upper_half_plane) :
upper_half_plane.smul_aux (x * y) z = upper_half_plane.smul_aux x (upper_half_plane.smul_aux y z)
source
@[protected, instance]
noncomputable def upper_half_plane.mul_action  :
mul_action ↥(matrix.GL_pos (fin 2) ℝ) upper_half_plane

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

Equations
source
@[protected, instance]
noncomputable def upper_half_plane.SL_action {R : Type u_1} [comm_ring R] [algebra R ℝ] :
mul_action (matrix.special_linear_group (fin 2) R) upper_half_plane
Equations
source
@[protected, instance]
noncomputable def upper_half_plane.matrix.GL_pos.has_coe  :
has_coe (matrix.special_linear_group (fin 2) ℤ) ↥(matrix.GL_pos (fin 2) ℝ)
Equations
source
@[protected, instance]
noncomputable def upper_half_plane.SL_on_GL_pos  :
has_smul (matrix.special_linear_group (fin 2) ℤ) ↥(matrix.GL_pos (fin 2) ℝ)
Equations
source
theorem upper_half_plane.SL_on_GL_pos_smul_apply (s : matrix.special_linear_group (fin 2) ℤ) (g : ↥(matrix.GL_pos (fin 2) ℝ)) (z : upper_half_plane) :
(s • g) • z = (↑s * g) • z
source
@[protected, instance]
def upper_half_plane.SL_to_GL_tower  :
is_scalar_tower (matrix.special_linear_group (fin 2) ℤ) ↥(matrix.GL_pos (fin 2) ℝ) upper_half_plane
source
@[protected, instance]
noncomputable def upper_half_plane.subgroup_GL_pos (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) :
has_smul ↥Γ ↥(matrix.GL_pos (fin 2) ℝ)
Equations
source
theorem upper_half_plane.subgroup_on_GL_pos_smul_apply (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) (s : ↥Γ) (g : ↥(matrix.GL_pos (fin 2) ℝ)) (z : upper_half_plane) :
(s • g) • z = (↑s * g) • z
source
@[protected, instance]
def upper_half_plane.subgroup_on_GL_pos (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) :
is_scalar_tower ↥Γ ↥(matrix.GL_pos (fin 2) ℝ) upper_half_plane
source
@[protected, instance]
def upper_half_plane.subgroup_SL (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) :
has_smul ↥Γ (matrix.special_linear_group (fin 2) ℤ)
Equations
source
theorem upper_half_plane.subgroup_on_SL_apply (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) (s : ↥Γ) (g : matrix.special_linear_group (fin 2) ℤ) (z : upper_half_plane) :
(s • g) • z = (↑s * g) • z
source
@[protected, instance]
def upper_half_plane.subgroup_to_SL_tower (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) :
is_scalar_tower ↥Γ (matrix.special_linear_group (fin 2) ℤ) upper_half_plane
source
theorem upper_half_plane.special_linear_group_apply {R : Type u_1} [comm_ring R] [algebra R ℝ] (g : matrix.special_linear_group (fin 2) 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))) _
source
@[simp]
theorem upper_half_plane.coe_smul (g : ↥(matrix.GL_pos (fin 2) ℝ)) (z : upper_half_plane) :
↑(g • z) = upper_half_plane.num g z / upper_half_plane.denom g z
source
@[simp]
theorem upper_half_plane.re_smul (g : ↥(matrix.GL_pos (fin 2) ℝ)) (z : upper_half_plane) :
(g • z).re = (upper_half_plane.num g z / upper_half_plane.denom g z).re
source
theorem upper_half_plane.im_smul (g : ↥(matrix.GL_pos (fin 2) ℝ)) (z : upper_half_plane) :
(g • z).im = (upper_half_plane.num g z / upper_half_plane.denom g z).im
source
theorem upper_half_plane.im_smul_eq_div_norm_sq (g : ↥(matrix.GL_pos (fin 2) ℝ)) (z : upper_half_plane) :
(g • z).im = ↑g.det * z.im / ⇑complex.norm_sq (upper_half_plane.denom g z)
source
@[simp]
theorem upper_half_plane.neg_smul (g : ↥(matrix.GL_pos (fin 2) ℝ)) (z : upper_half_plane) :
-g • z = g • z
source
@[simp]
theorem upper_half_plane.sl_moeb (A : matrix.special_linear_group (fin 2) ℤ) (z : upper_half_plane) :
A • z = ↑A • z
source
theorem upper_half_plane.subgroup_moeb (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) (A : ↥Γ) (z : upper_half_plane) :
A • z = ↑A • z
source
@[simp]
theorem upper_half_plane.subgroup_to_sl_moeb (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) (A : ↥Γ) (z : upper_half_plane) :
A • z = ↑A • z
source
@[simp]
theorem upper_half_plane.SL_neg_smul (g : matrix.special_linear_group (fin 2) ℤ) (z : upper_half_plane) :
-g • z = g • z
source
theorem upper_half_plane.c_mul_im_sq_le_norm_sq_denom (z : upper_half_plane) (g : matrix.special_linear_group (fin 2) ℝ) :
(↑g 1 0 * z.im) ^ 2 ≤ ⇑complex.norm_sq (upper_half_plane.denom ↑g z)
source
theorem upper_half_plane.special_linear_group.im_smul_eq_div_norm_sq (g : matrix.special_linear_group (fin 2) ℤ) (z : upper_half_plane) :
(g • z).im = z.im / ⇑complex.norm_sq (upper_half_plane.denom ↑g z)
source
theorem upper_half_plane.denom_apply (g : matrix.special_linear_group (fin 2) ℤ) (z : upper_half_plane) :
upper_half_plane.denom ↑g z = ↑(↑g 1 0) * ↑z + ↑(↑g 1 1)
source
@[protected, instance]
def upper_half_plane.pos_real_action  :
mul_action {x // 0 < x} upper_half_plane
Equations
source
@[simp]
theorem upper_half_plane.coe_pos_real_smul (x : {x // 0 < x}) (z : upper_half_plane) :
↑(x • z) = ↑x • ↑z
source
@[simp]
theorem upper_half_plane.pos_real_im (x : {x // 0 < x}) (z : upper_half_plane) :
(x • z).im = ↑x * z.im
source
@[simp]
theorem upper_half_plane.pos_real_re (x : {x // 0 < x}) (z : upper_half_plane) :
(x • z).re = ↑x * z.re
source
@[protected, instance]
def upper_half_plane.add_action  :
add_action ℝ upper_half_plane
Equations
source
@[simp]
theorem upper_half_plane.coe_vadd (x : ℝ) (z : upper_half_plane) :
↑(x +ᵥ z) = ↑x + ↑z
source
@[simp]
theorem upper_half_plane.vadd_re (x : ℝ) (z : upper_half_plane) :
(x +ᵥ z).re = x + z.re
source
@[simp]
theorem upper_half_plane.vadd_im (x : ℝ) (z : upper_half_plane) :
(x +ᵥ z).im = z.im
source
theorem upper_half_plane.modular_S_smul (z : upper_half_plane) :
modular_group.S • z = upper_half_plane.mk (-↑z)⁻¹ _
source
theorem upper_half_plane.modular_T_zpow_smul (z : upper_half_plane) (n : ℤ) :
modular_group.T ^ n • z = ↑n +ᵥ z
source
theorem upper_half_plane.modular_T_smul (z : upper_half_plane) :
modular_group.T • z = 1 +ᵥ z
source
theorem upper_half_plane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero (g : matrix.special_linear_group (fin 2) ℝ) (hc : ↑g 1 0 = 0) :
∃ (u : {x // 0 < x}) (v : ℝ), has_smul.smul g = (λ (z : upper_half_plane), v +ᵥ z) ∘ λ (z : upper_half_plane), u • z
source
theorem upper_half_plane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero (g : matrix.special_linear_group (fin 2) ℝ) (hc : ↑g 1 0 ≠ 0) :
∃ (u : {x // 0 < x}) (v w : ℝ), has_smul.smul g = has_vadd.vadd w ∘ has_smul.smul modular_group.S ∘ has_vadd.vadd v ∘ has_smul.smul u