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

    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
          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.mk_re (z : ) (h : 0 < z.im) :
            @[simp]
            theorem UpperHalfPlane.mk_im (z : ) (h : 0 < z.im) :
            @[simp]
            theorem UpperHalfPlane.coe_mk (z : ) (h : 0 < z.im) :
            ↑(UpperHalfPlane.mk z h) = 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

                  Fractional linear transformation, also known as the Moebius transformation

                  Instances For
                    @[simp]
                    theorem UpperHalfPlane.coe'_apply_complex {g : Matrix.SpecialLinearGroup (Fin 2) } {i : Fin 2} {j : Fin 2} :
                    ↑(g i j) = ↑(g i j)
                    theorem UpperHalfPlane.subgroup_on_glpos_smul_apply (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )) (s : { x // x Γ }) (g : { x // x Matrix.GLPos (Fin 2) }) (z : UpperHalfPlane) :
                    (s g) z = (s * g) z
                    theorem UpperHalfPlane.specialLinearGroup_apply {R : Type u_1} [CommRing R] [Algebra R ] (g : Matrix.SpecialLinearGroup (Fin 2) R) (z : UpperHalfPlane) :
                    g z = UpperHalfPlane.mk ((↑(↑(algebraMap R ) (g 0 0)) * z + ↑(↑(algebraMap R ) (g 0 1))) / (↑(↑(algebraMap R ) (g 1 0)) * z + ↑(↑(algebraMap R ) (g 1 1)))) (_ : 0 < (↑(g z)).im)
                    @[simp]
                    theorem UpperHalfPlane.neg_smul (g : { x // x Matrix.GLPos (Fin 2) }) (z : UpperHalfPlane) :
                    -g z = g z
                    theorem UpperHalfPlane.subgroup_moeb (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )) (A : { x // x Γ }) (z : UpperHalfPlane) :
                    A z = A z
                    @[simp]
                    theorem UpperHalfPlane.subgroup_to_sl_moeb (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )) (A : { x // x Γ }) (z : UpperHalfPlane) :
                    A z = A z
                    theorem UpperHalfPlane.c_mul_im_sq_le_normSq_denom (z : UpperHalfPlane) (g : Matrix.SpecialLinearGroup (Fin 2) ) :
                    (↑(Matrix.SpecialLinearGroup.toGLPos g) 1 0 * UpperHalfPlane.im z) ^ 2 Complex.normSq (UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGLPos g) z)
                    theorem UpperHalfPlane.denom_apply (g : Matrix.SpecialLinearGroup (Fin 2) ) (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
                    theorem UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero (g : Matrix.SpecialLinearGroup (Fin 2) ) (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 : Matrix.SpecialLinearGroup (Fin 2) ) (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