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

def Complex.UnitDisc :

Type

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

Equations

Complex.UnitDisc = ↑(Metric.ball 0 1)

source

instance Complex.instUnitDiscTopologicalSpace :

TopologicalSpace UnitDisc

Equations

Complex.instUnitDiscTopologicalSpace = instTopologicalSpaceSubtype

source

def UnitDisc.term𝔻 :

Lean.ParserDescr

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

Equations

UnitDisc.term𝔻 = Lean.ParserDescr.node `UnitDisc.term𝔻 1024 (Lean.ParserDescr.symbol "𝔻")

source

def Complex.UnitDisc.coe :

UnitDisc → ℂ

Coercion to ℂ.

Equations

Complex.UnitDisc.coe = Subtype.val

source

instance Complex.UnitDisc.instCommSemigroup :

CommSemigroup UnitDisc

Equations

Complex.UnitDisc.instCommSemigroup = id inferInstance

source

instance Complex.UnitDisc.instSemigroupWithZero :

SemigroupWithZero UnitDisc

Equations

Complex.UnitDisc.instSemigroupWithZero = id inferInstance

source

instance Complex.UnitDisc.instIsCancelMulZero :

IsCancelMulZero UnitDisc

source

instance Complex.UnitDisc.instHasDistribNeg :

HasDistribNeg UnitDisc

Equations

Complex.UnitDisc.instHasDistribNeg = id inferInstance

source

instance Complex.UnitDisc.instCoe :

Coe UnitDisc ℂ

Equations

Complex.UnitDisc.instCoe = { coe := Complex.UnitDisc.coe }

source

theorem Complex.UnitDisc.coe_injective :

Function.Injective UnitDisc.coe

source

@[simp]

theorem Complex.UnitDisc.coe_inj {z w : UnitDisc} :

↑z = ↑w ↔ z = w

source

theorem Complex.UnitDisc.norm_lt_one (z : UnitDisc) :

‖↑z‖ < 1

source

theorem Complex.UnitDisc.norm_ne_one (z : UnitDisc) :

‖↑z‖ ≠ 1

source

@[deprecated Complex.UnitDisc.norm_lt_one (since := "2025-02-16")]

theorem Complex.UnitDisc.abs_lt_one (z : UnitDisc) :

‖↑z‖ < 1

Alias of Complex.UnitDisc.norm_lt_one.

source

@[deprecated Complex.UnitDisc.norm_ne_one (since := "2025-02-16")]

theorem Complex.UnitDisc.abs_ne_one (z : UnitDisc) :

‖↑z‖ ≠ 1

Alias of Complex.UnitDisc.norm_ne_one.

source

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

@[simp]

theorem Complex.UnitDisc.coe_mul (z w : UnitDisc) :

↑(z * w) = ↑z * ↑w

source

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.

Equations

Complex.UnitDisc.mk z hz = ⟨z, ⋯⟩

source

@[simp]

theorem Complex.UnitDisc.coe_mk (z : ℂ) (hz : ‖z‖ < 1) :

↑(mk z hz) = z

source

@[simp]

theorem Complex.UnitDisc.mk_coe (z : UnitDisc) (hz : ‖↑z‖ < 1 := ⋯) :

mk (↑z) hz = z

source

@[simp]

theorem Complex.UnitDisc.mk_neg (z : ℂ) (hz : ‖-z‖ < 1) :

mk (-z) hz = -mk z ⋯

source

@[simp]

theorem Complex.UnitDisc.coe_zero :

↑0 = 0

source

@[simp]

theorem Complex.UnitDisc.coe_eq_zero {z : UnitDisc} :

↑z = 0 ↔ z = 0

source

@[simp]

theorem Complex.UnitDisc.mk_zero :

mk 0 ⋯ = 0

source

@[simp]

theorem Complex.UnitDisc.mk_eq_zero {z : ℂ} (hz : ‖z‖ < 1) :

mk z hz = 0 ↔ z = 0

source

instance Complex.UnitDisc.instInhabited :

Inhabited UnitDisc

Equations

Complex.UnitDisc.instInhabited = { default := 0 }

source

instance Complex.UnitDisc.circleAction :

MulAction Circle UnitDisc

Equations

Complex.UnitDisc.circleAction = mulActionSphereBall

source

instance Complex.UnitDisc.isScalarTower_circle_circle :

IsScalarTower Circle Circle UnitDisc

source

instance Complex.UnitDisc.isScalarTower_circle :

IsScalarTower Circle UnitDisc UnitDisc

source

instance Complex.UnitDisc.instSMulCommClass_circle :

SMulCommClass Circle UnitDisc UnitDisc

source

instance Complex.UnitDisc.instSMulCommClass_circle' :

SMulCommClass UnitDisc Circle UnitDisc

source

@[simp]

theorem Complex.UnitDisc.coe_smul_circle (z : Circle) (w : UnitDisc) :

↑(z • w) = ↑z * ↑w

source

instance Complex.UnitDisc.closedBallAction :

MulAction (↑(Metric.closedBall 0 1)) UnitDisc

Equations

Complex.UnitDisc.closedBallAction = mulActionClosedBallBall

source

instance Complex.UnitDisc.isScalarTower_closedBall_closedBall :

IsScalarTower (↑(Metric.closedBall 0 1)) (↑(Metric.closedBall 0 1)) UnitDisc

source

instance Complex.UnitDisc.isScalarTower_closedBall :

IsScalarTower (↑(Metric.closedBall 0 1)) UnitDisc UnitDisc

source

instance Complex.UnitDisc.instSMulCommClass_closedBall :

SMulCommClass (↑(Metric.closedBall 0 1)) UnitDisc UnitDisc

source

instance Complex.UnitDisc.instSMulCommClass_closedBall' :

SMulCommClass UnitDisc (↑(Metric.closedBall 0 1)) UnitDisc

source

instance Complex.UnitDisc.instSMulCommClass_circle_closedBall :

SMulCommClass Circle (↑(Metric.closedBall 0 1)) UnitDisc

source

instance Complex.UnitDisc.instSMulCommClass_closedBall_circle :

SMulCommClass (↑(Metric.closedBall 0 1)) Circle UnitDisc

source

@[simp]

theorem Complex.UnitDisc.coe_smul_closedBall (z : ↑(Metric.closedBall 0 1)) (w : UnitDisc) :

↑(z • w) = ↑z * ↑w

source

def Complex.UnitDisc.re (z : UnitDisc) :

ℝ

Real part of a point of the unit disc.

Equations

z.re = (↑z).re

source

def Complex.UnitDisc.im (z : UnitDisc) :

ℝ

Imaginary part of a point of the unit disc.

Equations

z.im = (↑z).im

source

@[simp]

theorem Complex.UnitDisc.re_coe (z : UnitDisc) :

(↑z).re = z.re

source

@[simp]

theorem Complex.UnitDisc.im_coe (z : UnitDisc) :

(↑z).im = z.im

source

@[simp]

theorem Complex.UnitDisc.re_neg (z : UnitDisc) :

(-z).re = -z.re

source

@[simp]

theorem Complex.UnitDisc.im_neg (z : UnitDisc) :

(-z).im = -z.im

source

def Complex.UnitDisc.conj (z : UnitDisc) :

UnitDisc

Conjugate point of the unit disc.

Equations

z.conj = Complex.UnitDisc.mk ((starRingEnd ℂ) ↑z) ⋯

source

@[simp]

theorem Complex.UnitDisc.coe_conj (z : UnitDisc) :

↑z.conj = (starRingEnd ℂ) ↑z

source

@[simp]

theorem Complex.UnitDisc.conj_zero :

conj 0 = 0

source

@[simp]

theorem Complex.UnitDisc.conj_conj (z : UnitDisc) :

z.conj.conj = z

source

@[simp]

theorem Complex.UnitDisc.conj_neg (z : UnitDisc) :

(-z).conj = -z.conj

source

@[simp]

theorem Complex.UnitDisc.re_conj (z : UnitDisc) :

z.conj.re = z.re

source

@[simp]

theorem Complex.UnitDisc.im_conj (z : UnitDisc) :

z.conj.im = -z.im

source

@[simp]

theorem Complex.UnitDisc.conj_mul (z w : UnitDisc) :

(z * w).conj = z.conj * w.conj

Documentation

Mathlib.Analysis.Complex.UnitDisc.Basic

Poincaré disc #