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

Complex unit disc.

Equations

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

Instances For

source

def UnitDisc.term𝔻 :

Lean.ParserDescr

Complex unit disc.

Equations

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

Instances For

source

instance Complex.UnitDisc.instCommSemigroup :

CommSemigroup Complex.UnitDisc

Equations

Complex.UnitDisc.instCommSemigroup = id inferInstance

source

instance Complex.UnitDisc.instHasDistribNeg :

HasDistribNeg Complex.UnitDisc

Equations

Complex.UnitDisc.instHasDistribNeg = id inferInstance

source

instance Complex.UnitDisc.instCoe :

Coe Complex.UnitDisc ℂ

Equations

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

source

theorem Complex.UnitDisc.coe_injective :

Function.Injective Subtype.val

source

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

Complex.abs ↑z < 1

source

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

Complex.abs ↑z ≠ 1

source

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

Complex.normSq ↑z < 1

source

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

↑z ≠ 1

source

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

↑z ≠ -1

source

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

1 + ↑z ≠ 0

source

@[simp]

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

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

source

def Complex.UnitDisc.mk (z : ℂ) (hz : Complex.abs z < 1) :

Complex.UnitDisc

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

Complex.UnitDisc.mk z hz = { val := z, property := ⋯ }

Instances For

source

@[simp]

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

↑(Complex.UnitDisc.mk z hz) = z

source

@[simp]

theorem Complex.UnitDisc.mk_coe (z : Complex.UnitDisc) (hz : optParam (Complex.abs ↑z < 1) ⋯) :

Complex.UnitDisc.mk (↑z) hz = z

source

@[simp]

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

Complex.UnitDisc.mk (-z) hz = -Complex.UnitDisc.mk z ⋯

source

instance Complex.UnitDisc.instSemigroupWithZeroUnitDisc :

SemigroupWithZero Complex.UnitDisc

Equations

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

source

@[simp]

theorem Complex.UnitDisc.coe_zero :

↑0 = 0

source

@[simp]

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

↑z = 0 ↔ z = 0

source

instance Complex.UnitDisc.instInhabitedUnitDisc :

Inhabited Complex.UnitDisc

Equations

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

source

instance Complex.UnitDisc.circleAction :

MulAction (↥circle) Complex.UnitDisc

Equations

Complex.UnitDisc.circleAction = mulActionSphereBall

source

instance Complex.UnitDisc.isScalarTower_circle_circle :

IsScalarTower (↥circle) (↥circle) Complex.UnitDisc

Equations

Complex.UnitDisc.isScalarTower_circle_circle = ⋯

source

instance Complex.UnitDisc.isScalarTower_circle :

IsScalarTower (↥circle) Complex.UnitDisc Complex.UnitDisc

Equations

Complex.UnitDisc.isScalarTower_circle = ⋯

source

instance Complex.UnitDisc.instSMulCommClass_circle :

SMulCommClass (↥circle) Complex.UnitDisc Complex.UnitDisc

Equations

Complex.UnitDisc.instSMulCommClass_circle = ⋯

source

instance Complex.UnitDisc.instSMulCommClass_circle' :

SMulCommClass Complex.UnitDisc (↥circle) Complex.UnitDisc

Equations

Complex.UnitDisc.instSMulCommClass_circle' = ⋯

source

@[simp]

theorem Complex.UnitDisc.coe_smul_circle (z : ↥circle) (w : Complex.UnitDisc) :

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

source

instance Complex.UnitDisc.closedBallAction :

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

Equations

Complex.UnitDisc.closedBallAction = mulActionClosedBallBall

source

instance Complex.UnitDisc.isScalarTower_closedBall_closedBall :

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

Equations

Complex.UnitDisc.isScalarTower_closedBall_closedBall = ⋯

source

instance Complex.UnitDisc.isScalarTower_closedBall :

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

Equations

Complex.UnitDisc.isScalarTower_closedBall = ⋯

source

instance Complex.UnitDisc.instSMulCommClass_closedBall :

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

Equations

Complex.UnitDisc.instSMulCommClass_closedBall = ⋯

source

instance Complex.UnitDisc.instSMulCommClass_closedBall' :

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

Equations

Complex.UnitDisc.instSMulCommClass_closedBall' = ⋯

source

instance Complex.UnitDisc.instSMulCommClass_circle_closedBall :

SMulCommClass (↥circle) (↑(Metric.closedBall 0 1)) Complex.UnitDisc

Equations

Complex.UnitDisc.instSMulCommClass_circle_closedBall = ⋯

source

instance Complex.UnitDisc.instSMulCommClass_closedBall_circle :

SMulCommClass (↑(Metric.closedBall 0 1)) (↥circle) Complex.UnitDisc

Equations

Complex.UnitDisc.instSMulCommClass_closedBall_circle = ⋯

source

@[simp]

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

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

source

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

ℝ

Real part of a point of the unit disc.

Equations

Complex.UnitDisc.re z = (↑z).re

Instances For

source

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

ℝ

Imaginary part of a point of the unit disc.

Equations

Complex.UnitDisc.im z = (↑z).im

Instances For

source

@[simp]

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

(↑z).re = Complex.UnitDisc.re z

source

@[simp]

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

(↑z).im = Complex.UnitDisc.im z

source

@[simp]

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

Complex.UnitDisc.re (-z) = -Complex.UnitDisc.re z

source

@[simp]

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

Complex.UnitDisc.im (-z) = -Complex.UnitDisc.im z

source

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

Complex.UnitDisc

Conjugate point of the unit disc.

Equations

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

Instances For

source

@[simp]

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

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

source

@[simp]

theorem Complex.UnitDisc.conj_zero :

Complex.UnitDisc.conj 0 = 0

source

@[simp]

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

Complex.UnitDisc.conj (Complex.UnitDisc.conj z) = z

source

@[simp]

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

Complex.UnitDisc.conj (-z) = -Complex.UnitDisc.conj z

source

@[simp]

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

Complex.UnitDisc.re (Complex.UnitDisc.conj z) = Complex.UnitDisc.re z

source

@[simp]

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

Complex.UnitDisc.im (Complex.UnitDisc.conj z) = -Complex.UnitDisc.im z

source

@[simp]

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

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

Documentation

Mathlib.Analysis.Complex.UnitDisc.Basic

Poincaré disc #