Documentation

Mathlib.Analysis.Complex.UpperHalfPlane.Basic

The upper half plane #

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

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, denoted as within the UpperHalfPlane namespace

Equations
Instances For

    The open upper half plane, denoted as within the UpperHalfPlane namespace

    Equations
    Instances For

      Canonical embedding of the upper half-plane into .

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

        Imaginary part

        Equations
        Instances For

          Real part

          Equations
          Instances For
            theorem UpperHalfPlane.ext' {a 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) :
              (mk z h).re = z.re
              @[simp]
              theorem UpperHalfPlane.mk_im (z : ) (h : 0 < z.im) :
              (mk z h).im = z.im
              @[simp]
              theorem UpperHalfPlane.coe_mk (z : ) (h : 0 < z.im) :
              (mk z h) = z
              @[simp]
              theorem UpperHalfPlane.coe_mk_subtype {z : } (hz : 0 < z.im) :
              z, hz = z
              @[simp]
              theorem UpperHalfPlane.mk_coe (z : UpperHalfPlane) (h : 0 < (↑z).im := ) :
              mk (↑z) h = z

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

              Equations
              Instances For
                @[simp]
                @[simp]
                theorem UpperHalfPlane.ne_nat (z : UpperHalfPlane) (n : ) :
                z n
                theorem UpperHalfPlane.ne_int (z : UpperHalfPlane) (n : ) :
                z n
                Equations
                • One or more equations did not get rendered due to their size.
                @[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
                Equations
                • One or more equations did not get rendered due to their size.
                @[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