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

Equations
Instances For

    The open upper half plane

    Equations
    Instances For

      Canonical embedding of the upper half-plane into .

      Equations
      • z = z
      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

        Equations
        • z.im = (z).im
        Instances For

          Real part

          Equations
          • z.re = (z).re
          Instances For
            theorem UpperHalfPlane.ext' {a : UpperHalfPlane} {b : UpperHalfPlane} (hre : a.re = b.re) (him : a.im = b.im) :
            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.

            Equations
            Instances For
              @[simp]
              theorem UpperHalfPlane.coe_im (z : UpperHalfPlane) :
              (z).im = z.im
              @[simp]
              theorem UpperHalfPlane.coe_re (z : UpperHalfPlane) :
              (z).re = z.re
              @[simp]
              theorem UpperHalfPlane.mk_re (z : ) (h : 0 < z.im) :
              (UpperHalfPlane.mk z h).re = z.re
              @[simp]
              theorem UpperHalfPlane.mk_im (z : ) (h : 0 < z.im) :
              (UpperHalfPlane.mk z h).im = 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) ) :
              UpperHalfPlane.mk (z) h = z
              theorem UpperHalfPlane.re_add_im (z : UpperHalfPlane) :
              z.re + z.im * Complex.I = z

              Define I := √-1 as an element on the upper half plane.

              Equations
              Instances For
                theorem UpperHalfPlane.normSq_pos (z : UpperHalfPlane) :
                0 < Complex.normSq z
                theorem UpperHalfPlane.normSq_ne_zero (z : UpperHalfPlane) :
                Complex.normSq z 0

                Numerator of the formula for a fractional linear transformation

                Equations
                Instances For

                  Denominator of the formula for a fractional linear transformation

                  Equations
                  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

                    Equations
                    Instances For
                      theorem UpperHalfPlane.smulAux'_im (g : (Matrix.GLPos (Fin 2) )) (z : UpperHalfPlane) :
                      (UpperHalfPlane.smulAux' g z).im = (g).det * z.im / Complex.normSq (UpperHalfPlane.denom g z)

                      Fractional linear transformation, also known as the Moebius transformation

                      Equations
                      Instances For

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Equations

                        Canonical embedding of SL(2, ℤ) into GL(2, ℝ)⁺.

                        Equations
                        Instances For
                          @[simp]
                          theorem UpperHalfPlane.ModularGroup.coe'_apply_complex {g : Matrix.SpecialLinearGroup (Fin 2) } {i : Fin 2} {j : Fin 2} :
                          (g i j) = (g i j)
                          @[simp]
                          Equations
                          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))))
                          @[simp]
                          theorem UpperHalfPlane.im_smul_eq_div_normSq (g : (Matrix.GLPos (Fin 2) )) (z : UpperHalfPlane) :
                          (g z).im = (g).det * z.im / Complex.normSq (UpperHalfPlane.denom g z)
                          theorem UpperHalfPlane.c_mul_im_sq_le_normSq_denom (z : UpperHalfPlane) (g : Matrix.SpecialLinearGroup (Fin 2) ) :
                          ((Matrix.SpecialLinearGroup.toGLPos g) 1 0 * z.im) ^ 2 Complex.normSq (UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGLPos g) z)
                          @[simp]
                          theorem UpperHalfPlane.neg_smul (g : (Matrix.GLPos (Fin 2) )) (z : UpperHalfPlane) :
                          -g z = g z
                          @[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) :
                          (x z).im = x * z.im
                          @[simp]
                          theorem UpperHalfPlane.pos_real_re (x : { x : // 0 < x }) (z : UpperHalfPlane) :
                          (x z).re = x * z.re
                          @[simp]
                          theorem UpperHalfPlane.coe_vadd (x : ) (z : UpperHalfPlane) :
                          (x +ᵥ z) = x + z
                          @[simp]
                          theorem UpperHalfPlane.vadd_re (x : ) (z : UpperHalfPlane) :
                          (x +ᵥ z).re = x + z.re
                          @[simp]
                          theorem UpperHalfPlane.vadd_im (x : ) (z : UpperHalfPlane) :
                          (x +ᵥ z).im = z.im
                          theorem UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero (g : Matrix.SpecialLinearGroup (Fin 2) ) (hc : g 1 0 = 0) :
                          ∃ (u : { x : // 0 < x }) (v : ), (fun (x : UpperHalfPlane) => g x) = (fun (x : UpperHalfPlane) => v +ᵥ x) fun (x : UpperHalfPlane) => u x
                          theorem UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero (g : Matrix.SpecialLinearGroup (Fin 2) ) (hc : g 1 0 0) :
                          ∃ (u : { x : // 0 < x }) (v : ) (w : ), (fun (x : UpperHalfPlane) => g x) = (fun (x : UpperHalfPlane) => w +ᵥ x) (fun (x : UpperHalfPlane) => ModularGroup.S x) (fun (x : UpperHalfPlane) => v +ᵥ x) fun (x : UpperHalfPlane) => u x