Documentation

Mathlib.Analysis.Complex.UnitDisc.Basic

Poincaré disc #

In this file we define Complex.UnitDisc to be the unit disc in the complex plane. We also introduce some basic operations on this disc.

Complex unit disc.

Equations
Instances For

    Complex unit disc.

    Equations
    Instances For
      theorem Complex.UnitDisc.abs_lt_one (z : Complex.UnitDisc) :
      Complex.abs ↑z < 1
      theorem Complex.UnitDisc.abs_ne_one (z : Complex.UnitDisc) :
      Complex.abs ↑z ≠ 1
      theorem Complex.UnitDisc.normSq_lt_one (z : Complex.UnitDisc) :
      Complex.normSq ↑z < 1
      @[simp]
      theorem Complex.UnitDisc.coe_mul (z : Complex.UnitDisc) (w : Complex.UnitDisc) :
      ↑(z * w) = ↑z * ↑w
      def Complex.UnitDisc.mk (z : â„‚) (hz : Complex.abs z < 1) :

      A constructor that assumes abs z < 1 instead of dist z 0 < 1 and returns an element of 𝔻 instead of ↥Metric.ball (0 : ℂ) 1.

      Equations
      Instances For
        @[simp]
        theorem Complex.UnitDisc.coe_mk (z : â„‚) (hz : Complex.abs z < 1) :
        ↑(Complex.UnitDisc.mk z hz) = z
        @[simp]
        theorem Complex.UnitDisc.mk_coe (z : Complex.UnitDisc) (hz : optParam (Complex.abs ↑z < 1) ⋯) :
        Complex.UnitDisc.mk (↑z) hz = z
        @[simp]
        theorem Complex.UnitDisc.mk_neg (z : â„‚) (hz : Complex.abs (-z) < 1) :
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem Complex.UnitDisc.coe_zero :
        ↑0 = 0
        @[simp]
        @[simp]
        theorem Complex.UnitDisc.coe_smul_circle (z : ↥circle) (w : Complex.UnitDisc) :
        ↑(z • w) = ↑z * ↑w
        @[simp]
        theorem Complex.UnitDisc.coe_smul_closedBall (z : ↑(Metric.closedBall 0 1)) (w : Complex.UnitDisc) :
        ↑(z • w) = ↑z * ↑w

        Real part of a point of the unit disc.

        Equations
        • z.re = (↑z).re
        Instances For

          Imaginary part of a point of the unit disc.

          Equations
          • z.im = (↑z).im
          Instances For
            @[simp]
            theorem Complex.UnitDisc.re_coe (z : Complex.UnitDisc) :
            (↑z).re = z.re
            @[simp]
            theorem Complex.UnitDisc.im_coe (z : Complex.UnitDisc) :
            (↑z).im = z.im
            @[simp]
            theorem Complex.UnitDisc.re_neg (z : Complex.UnitDisc) :
            (-z).re = -z.re
            @[simp]
            theorem Complex.UnitDisc.im_neg (z : Complex.UnitDisc) :
            (-z).im = -z.im

            Conjugate point of the unit disc.

            Equations
            Instances For
              @[simp]
              theorem Complex.UnitDisc.coe_conj (z : Complex.UnitDisc) :
              ↑z.conj = (starRingEnd ℂ) ↑z
              @[simp]
              theorem Complex.UnitDisc.conj_conj (z : Complex.UnitDisc) :
              z.conj.conj = z
              @[simp]
              theorem Complex.UnitDisc.conj_neg (z : Complex.UnitDisc) :
              (-z).conj = -z.conj
              @[simp]
              theorem Complex.UnitDisc.re_conj (z : Complex.UnitDisc) :
              z.conj.re = z.re
              @[simp]
              theorem Complex.UnitDisc.im_conj (z : Complex.UnitDisc) :
              z.conj.im = -z.im
              @[simp]
              theorem Complex.UnitDisc.conj_mul (z : Complex.UnitDisc) (w : Complex.UnitDisc) :
              (z * w).conj = z.conj * w.conj