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.

source
πŸ”Έ coverage
def Complex.UnitDisc :
Type

The complex unit disc, denoted as 𝔻 within the Complex namespace

Instances For
    source
    πŸ”Έ coverage
    @[implicit_reducible]
    noncomputable instance Complex.instTopologicalSpaceUnitDisc :
    TopologicalSpace UnitDisc
    source
    πŸ”Έ coverage
    def Complex.UnitDisc.term𝔻 :
    Lean.ParserDescr

    The complex unit disc, denoted as 𝔻 within the Complex namespace

    Instances For
      source
      πŸ”Έ coverage
      def Complex.UnitDisc.coe :
      UnitDisc β†’ β„‚

      Coercion to β„‚.

      Instances For
        source
        πŸ”Έ coverage
        @[implicit_reducible]
        noncomputable instance Complex.UnitDisc.instCommSemigroup :
        CommSemigroup UnitDisc
        source
        πŸ”Έ coverage
        @[implicit_reducible]
        noncomputable instance Complex.UnitDisc.instSemigroupWithZero :
        SemigroupWithZero UnitDisc
        source
        πŸ“ coverage
        instance Complex.UnitDisc.instIsCancelMulZero :
        IsCancelMulZero UnitDisc
        source
        πŸ”Έ coverage
        @[implicit_reducible]
        noncomputable instance Complex.UnitDisc.instHasDistribNeg :
        HasDistribNeg UnitDisc
        source
        πŸ”Έ coverage
        @[implicit_reducible]
        instance Complex.UnitDisc.instCoe :
        Coe UnitDisc β„‚
        source
        πŸ“ coverage
        theorem Complex.UnitDisc.coe_injective :
        Function.Injective UnitDisc.coe
        source
        πŸ“ coverage
        theorem Complex.UnitDisc.coe_injective_iff {a₁ aβ‚‚ : UnitDisc} :
        a₁ = aβ‚‚ ↔ ↑a₁ = ↑aβ‚‚
        source
        πŸ“ coverage
        @[simp]
        theorem Complex.UnitDisc.coe_inj {z w : UnitDisc} :
        ↑z = ↑w ↔ z = w
        source
        πŸ“ coverage
        theorem Complex.UnitDisc.isEmbedding_coe :
        Topology.IsEmbedding UnitDisc.coe
        source
        πŸ“ coverage
        theorem Complex.UnitDisc.continuous_coe :
        Continuous UnitDisc.coe
        source
        πŸ“ coverage
        theorem Complex.UnitDisc.norm_lt_one (z : UnitDisc) :
        ‖↑zβ€– < 1
        source
        theorem Complex.UnitDisc.norm_ne_one (z : UnitDisc) :
        ‖↑zβ€– β‰  1
        source
        πŸ“ coverage
        theorem Complex.UnitDisc.sq_norm_lt_one (z : UnitDisc) :
        ‖↑zβ€– ^ 2 < 1
        source
        πŸ“ coverage
        theorem Complex.UnitDisc.normSq_lt_one (z : UnitDisc) :
        normSq ↑z < 1
        source
        theorem Complex.UnitDisc.coe_ne_one (z : UnitDisc) :
        ↑z β‰  1
        source
        theorem Complex.UnitDisc.coe_ne_neg_one (z : UnitDisc) :
        ↑z β‰  -1
        source
        theorem Complex.UnitDisc.one_add_coe_ne_zero (z : UnitDisc) :
        1 + ↑z β‰  0
        source
        πŸ“ coverage
        @[simp]
        theorem Complex.UnitDisc.coe_mul (z w : UnitDisc) :
        ↑(z * w) = ↑z * ↑w
        source
        πŸ“ coverage
        @[simp]
        theorem Complex.UnitDisc.coe_neg (z : UnitDisc) :
        ↑(-z) = -↑z
        source
        πŸ”Έ coverage
        def Complex.UnitDisc.mk (z : β„‚) (hz : β€–zβ€– < 1) :
        UnitDisc

        A constructor that assumes β€–zβ€– < 1 instead of dist z 0 < 1 and returns an element of 𝔻 instead of β†₯Metric.ball (0 : β„‚) 1.

        Instances For
          source
          πŸ“ coverage
          instance Complex.UnitDisc.instCanLiftCoeLtRealNormOfNat :
          CanLift β„‚ UnitDisc UnitDisc.coe fun (x : β„‚) => β€–xβ€– < 1
          source
          πŸ”Έ coverage
          def Complex.UnitDisc.casesOn {motive : UnitDisc β†’ Sort u_1} (mk : (z : β„‚) β†’ (hz : β€–zβ€– < 1) β†’ motive (mk z hz)) (z : UnitDisc) :
          motive z

          A cases eliminator that makes cases z use UnitDisc.mk instead of Subtype.mk.

          Instances For
            source
            @[simp]
            theorem Complex.UnitDisc.casesOn_mk {motive : UnitDisc β†’ Sort u_1} (mk' : (z : β„‚) β†’ (hz : β€–zβ€– < 1) β†’ motive (mk z hz)) {z : β„‚} (hz : β€–zβ€– < 1) :
            UnitDisc.casesOn mk' (mk z hz) = mk' z hz
            source
            πŸ“ coverage
            @[simp]
            theorem Complex.UnitDisc.coe_mk (z : β„‚) (hz : β€–zβ€– < 1) :
            ↑(mk z hz) = z
            source
            πŸ“ coverage
            @[simp]
            theorem Complex.UnitDisc.mk_coe (z : UnitDisc) (hz : ‖↑zβ€– < 1 := β‹―) :
            mk (↑z) hz = z
            source
            @[simp]
            theorem Complex.UnitDisc.mk_inj {z w : β„‚} (hz : β€–zβ€– < 1) (hw : β€–wβ€– < 1) :
            mk z hz = mk w hw ↔ z = w
            source
            theorem Complex.UnitDisc.forall {p : UnitDisc β†’ Prop} :
            (βˆ€ (z : UnitDisc), p z) ↔ βˆ€ (z : β„‚) (hz : β€–zβ€– < 1), p (mk z hz)
            source
            πŸ“ coverage
            theorem Complex.UnitDisc.exists {p : UnitDisc β†’ Prop} :
            (βˆƒ (z : UnitDisc), p z) ↔ βˆƒ (z : β„‚) (hz : β€–zβ€– < 1), p (mk z hz)
            source
            πŸ“ coverage
            @[simp]
            theorem Complex.UnitDisc.mk_neg (z : β„‚) (hz : β€–-zβ€– < 1) :
            mk (-z) hz = -mk z β‹―
            source
            πŸ“ coverage
            @[simp]
            theorem Complex.UnitDisc.coe_zero :
            ↑0 = 0
            source
            πŸ“ coverage
            @[simp]
            theorem Complex.UnitDisc.coe_eq_zero {z : UnitDisc} :
            ↑z = 0 ↔ z = 0
            source
            πŸ“ coverage
            @[simp]
            theorem Complex.UnitDisc.mk_zero :
            mk 0 mk_zero._proof_1 = 0
            source
            πŸ“ coverage
            @[simp]
            theorem Complex.UnitDisc.mk_eq_zero {z : β„‚} (hz : β€–zβ€– < 1) :
            mk z hz = 0 ↔ z = 0
            source
            πŸ”Έ coverage
            @[implicit_reducible]
            noncomputable instance Complex.UnitDisc.instInhabited :
            Inhabited UnitDisc
            source
            πŸ”Έ coverage
            @[implicit_reducible]
            noncomputable instance Complex.UnitDisc.instMulActionCircle :
            MulAction Circle UnitDisc
            source
            πŸ“ coverage
            instance Complex.UnitDisc.instIsScalarTower_circle_circle :
            IsScalarTower Circle Circle UnitDisc
            source
            πŸ“ coverage
            instance Complex.UnitDisc.instIsScalarTower_circle :
            IsScalarTower Circle UnitDisc UnitDisc
            source
            πŸ“ coverage
            instance Complex.UnitDisc.instSMulCommClass_circle_left :
            SMulCommClass Circle UnitDisc UnitDisc
            source
            πŸ“ coverage
            instance Complex.UnitDisc.instSMulCommClass_circle_right :
            SMulCommClass UnitDisc Circle UnitDisc
            source
            πŸ“ coverage
            @[simp]
            theorem Complex.UnitDisc.coe_circle_smul (z : Circle) (w : UnitDisc) :
            ↑(z β€’ w) = ↑z * ↑w
            source
            πŸ“ coverage
            @[deprecated Complex.UnitDisc.coe_circle_smul (since := "2026-01-06")]
            theorem Complex.UnitDisc.coe_smul_circle (z : Circle) (w : UnitDisc) :
            ↑(z β€’ w) = ↑z * ↑w

            Alias of Complex.UnitDisc.coe_circle_smul.

            source
            πŸ”Έ coverage
            @[implicit_reducible]
            noncomputable instance Complex.UnitDisc.instMulActionClosedBall :
            MulAction (↑(Metric.closedBall 0 1)) UnitDisc
            source
            πŸ“ coverage
            instance Complex.UnitDisc.instIsScalarTower_closedBall_closedBall :
            IsScalarTower (↑(Metric.closedBall 0 1)) (↑(Metric.closedBall 0 1)) UnitDisc
            source
            πŸ“ coverage
            instance Complex.UnitDisc.instIsScalarTower_closedBall :
            IsScalarTower (↑(Metric.closedBall 0 1)) UnitDisc UnitDisc
            source
            πŸ“ coverage
            instance Complex.UnitDisc.instSMulCommClass_closedBall_left :
            SMulCommClass (↑(Metric.closedBall 0 1)) UnitDisc UnitDisc
            source
            πŸ“ coverage
            instance Complex.UnitDisc.instSMulCommClass_closedBall_right :
            SMulCommClass UnitDisc (↑(Metric.closedBall 0 1)) UnitDisc
            source
            πŸ“ coverage
            instance Complex.UnitDisc.instSMulCommClass_circle_closedBall :
            SMulCommClass Circle (↑(Metric.closedBall 0 1)) UnitDisc
            source
            πŸ“ coverage
            instance Complex.UnitDisc.instSMulCommClass_closedBall_circle :
            SMulCommClass (↑(Metric.closedBall 0 1)) Circle UnitDisc
            source
            πŸ“ coverage
            @[simp]
            theorem Complex.UnitDisc.coe_closedBall_smul (z : ↑(Metric.closedBall 0 1)) (w : UnitDisc) :
            ↑(z β€’ w) = ↑z * ↑w
            source
            πŸ“ coverage
            @[deprecated Complex.UnitDisc.coe_closedBall_smul (since := "2026-01-06")]
            theorem Complex.UnitDisc.coe_smul_closedBall (z : ↑(Metric.closedBall 0 1)) (w : UnitDisc) :
            ↑(z β€’ w) = ↑z * ↑w

            Alias of Complex.UnitDisc.coe_closedBall_smul.

            source
            πŸ”Έ coverage
            @[implicit_reducible]
            instance Complex.UnitDisc.instPowPNat :
            Pow UnitDisc β„•+
            source
            πŸ“ coverage
            @[simp]
            theorem Complex.UnitDisc.coe_pow (z : UnitDisc) (n : β„•+) :
            ↑(z ^ n) = ↑z ^ ↑n
            source
            πŸ“ coverage
            theorem Complex.UnitDisc.continuous_pow (n : β„•+) :
            Continuous fun (x : UnitDisc) => x ^ n
            source
            πŸ“ coverage
            @[simp]
            theorem Complex.UnitDisc.pow_eq_zero {z : UnitDisc} {n : β„•+} :
            z ^ n = 0 ↔ z = 0
            source
            πŸ“ coverage
            instance Complex.UnitDisc.instPNatPowAssoc :
            PNatPowAssoc UnitDisc
            source
            πŸ“ coverage
            theorem Complex.UnitDisc.tendsto_pow_atTop_nhds_zero (z : UnitDisc) :
            Filter.Tendsto (fun (n : β„•+) => z ^ n) Filter.atTop (nhds 0)
            source
            πŸ”Έ coverage
            def Complex.UnitDisc.re (z : UnitDisc) :
            ℝ

            Real part of a point of the unit disc.

            Instances For
              source
              πŸ”Έ coverage
              def Complex.UnitDisc.im (z : UnitDisc) :
              ℝ

              Imaginary part of a point of the unit disc.

              Instances For
                source
                πŸ“ coverage
                @[simp]
                theorem Complex.UnitDisc.re_coe (z : UnitDisc) :
                (↑z).re = z.re
                source
                πŸ“ coverage
                @[simp]
                theorem Complex.UnitDisc.im_coe (z : UnitDisc) :
                (↑z).im = z.im
                source
                πŸ“ coverage
                @[simp]
                theorem Complex.UnitDisc.re_neg (z : UnitDisc) :
                (-z).re = -z.re
                source
                πŸ“ coverage
                @[simp]
                theorem Complex.UnitDisc.im_neg (z : UnitDisc) :
                (-z).im = -z.im
                source
                πŸ“ coverage
                @[simp]
                theorem Complex.UnitDisc.re_zero :
                re 0 = 0
                source
                πŸ“ coverage
                @[simp]
                theorem Complex.UnitDisc.im_zero :
                im 0 = 0
                source
                πŸ”Έ coverage
                @[implicit_reducible]
                instance Complex.UnitDisc.instStar :
                Star UnitDisc

                Conjugate point of the unit disc.

                source
                πŸ”Έ coverage
                @[deprecated Star.star (since := "2026-01-06")]
                def Complex.UnitDisc.conj (z : UnitDisc) :
                UnitDisc

                Conjugate point of the unit disc. Deprecated, use star instead.

                Instances For
                  source
                  πŸ“ coverage
                  @[simp]
                  theorem Complex.UnitDisc.coe_star (z : UnitDisc) :
                  ↑(star z) = (starRingEnd β„‚) ↑z
                  source
                  πŸ“ coverage
                  @[deprecated Complex.UnitDisc.coe_star (since := "2026-01-06")]
                  theorem Complex.UnitDisc.coe_conj (z : UnitDisc) :
                  ↑(star z) = (starRingEnd β„‚) ↑z

                  Alias of Complex.UnitDisc.coe_star.

                  source
                  πŸ“ coverage
                  @[simp]
                  theorem Complex.UnitDisc.star_eq_zero {z : UnitDisc} :
                  star z = 0 ↔ z = 0
                  source
                  πŸ“ coverage
                  @[simp]
                  theorem Complex.UnitDisc.star_zero :
                  star 0 = 0
                  source
                  πŸ”Έ coverage
                  @[implicit_reducible]
                  instance Complex.UnitDisc.instInvolutiveStar :
                  InvolutiveStar UnitDisc
                  source
                  πŸ“ coverage
                  @[deprecated star_star (since := "2026-01-06")]
                  theorem Complex.UnitDisc.conj_conj (z : UnitDisc) :
                  star (star z) = z
                  source
                  πŸ“ coverage
                  @[simp]
                  theorem Complex.UnitDisc.star_neg (z : UnitDisc) :
                  star (-z) = -star z
                  source
                  πŸ“ coverage
                  @[deprecated Complex.UnitDisc.star_neg (since := "2026-01-06")]
                  theorem Complex.UnitDisc.conj_neg (z : UnitDisc) :
                  star (-z) = -star z

                  Alias of Complex.UnitDisc.star_neg.

                  source
                  πŸ“ coverage
                  @[simp]
                  theorem Complex.UnitDisc.re_star (z : UnitDisc) :
                  (star z).re = z.re
                  source
                  πŸ“ coverage
                  @[deprecated Complex.UnitDisc.re_star (since := "2026-01-06")]
                  theorem Complex.UnitDisc.re_conj (z : UnitDisc) :
                  (star z).re = z.re

                  Alias of Complex.UnitDisc.re_star.

                  source
                  πŸ“ coverage
                  @[simp]
                  theorem Complex.UnitDisc.im_star (z : UnitDisc) :
                  (star z).im = -z.im
                  source
                  πŸ“ coverage
                  @[deprecated Complex.UnitDisc.im_star (since := "2026-01-06")]
                  theorem Complex.UnitDisc.im_conj (z : UnitDisc) :
                  (star z).im = -z.im

                  Alias of Complex.UnitDisc.im_star.

                  source
                  πŸ”Έ coverage
                  @[implicit_reducible]
                  instance Complex.UnitDisc.instStarMul :
                  StarMul UnitDisc
                  source
                  πŸ“ coverage
                  @[deprecated star_mul' (since := "2026-01-06")]
                  theorem Complex.UnitDisc.conj_mul (z w : UnitDisc) :
                  star (z * w) = star z * star w