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 𝔻 within the Complex namespace

Equations

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

Instances For

source

@[implicit_reducible]

noncomputable instance Complex.instTopologicalSpaceUnitDisc :

TopologicalSpace UnitDisc

Equations

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

source

def Complex.UnitDisc.term𝔻 :

Lean.ParserDescr

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

Equations

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

Instances For

source

def Complex.UnitDisc.coe :

UnitDisc → ℂ

Coercion to ℂ.

Equations

Complex.UnitDisc.coe = Subtype.val

Instances For

source

@[implicit_reducible]

noncomputable instance Complex.UnitDisc.instCommSemigroup :

CommSemigroup UnitDisc

Equations

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

source

@[implicit_reducible]

noncomputable instance Complex.UnitDisc.instSemigroupWithZero :

SemigroupWithZero UnitDisc

Equations

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

source

instance Complex.UnitDisc.instIsCancelMulZero :

IsCancelMulZero UnitDisc

source

@[implicit_reducible]

noncomputable instance Complex.UnitDisc.instHasDistribNeg :

HasDistribNeg UnitDisc

Equations

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

source

@[implicit_reducible]

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

theorem Complex.UnitDisc.coe_injective_iff {a₁ a₂ : UnitDisc} :

a₁ = a₂ ↔ ↑a₁ = ↑a₂

source

@[simp]

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

↑z = ↑w ↔ z = w

source

theorem Complex.UnitDisc.isEmbedding_coe :

Topology.IsEmbedding UnitDisc.coe

source

theorem Complex.UnitDisc.continuous_coe :

Continuous UnitDisc.coe

source

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

‖↑z‖ < 1

source

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

‖↑z‖ ≠ 1

source

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

‖↑z‖ ^ 2 < 1

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

@[simp]

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

↑(-z) = -↑z

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, ⋯⟩

Instances For

source

instance Complex.UnitDisc.instCanLiftCoeLtRealNormOfNat :

CanLift ℂ UnitDisc UnitDisc.coe fun (x : ℂ) => ‖x‖ < 1

source

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.

Equations

Complex.UnitDisc.casesOn mk z = mk ↑z ⋯

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

@[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_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

theorem Complex.UnitDisc.exists {p : UnitDisc → Prop} :

(∃ (z : UnitDisc), p z) ↔ ∃ (z : ℂ) (hz : ‖z‖ < 1), p (mk z hz)

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 mk_zero._proof_1 = 0

source

@[simp]

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

mk z hz = 0 ↔ z = 0

source

@[implicit_reducible]

noncomputable instance Complex.UnitDisc.instInhabited :

Inhabited UnitDisc

Equations

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

source

@[implicit_reducible]

noncomputable instance Complex.UnitDisc.instMulActionCircle :

MulAction Circle UnitDisc

Equations

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

source

instance Complex.UnitDisc.instIsScalarTower_circle_circle :

IsScalarTower Circle Circle UnitDisc

source

instance Complex.UnitDisc.instIsScalarTower_circle :

IsScalarTower Circle UnitDisc UnitDisc

source

instance Complex.UnitDisc.instSMulCommClass_circle_left :

SMulCommClass Circle UnitDisc UnitDisc

source

instance Complex.UnitDisc.instSMulCommClass_circle_right :

SMulCommClass UnitDisc Circle UnitDisc

source

@[simp]

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

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

source

@[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

@[implicit_reducible]

noncomputable instance Complex.UnitDisc.instMulActionClosedBall :

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

Equations

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

source

instance Complex.UnitDisc.instIsScalarTower_closedBall_closedBall :

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

source

instance Complex.UnitDisc.instIsScalarTower_closedBall :

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

source

instance Complex.UnitDisc.instSMulCommClass_closedBall_left :

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

source

instance Complex.UnitDisc.instSMulCommClass_closedBall_right :

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_closedBall_smul (z : ↑(Metric.closedBall 0 1)) (w : UnitDisc) :

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

source

@[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

@[implicit_reducible]

instance Complex.UnitDisc.instPowPNat :

Pow UnitDisc ℕ+

Equations

Complex.UnitDisc.instPowPNat = { pow := fun (z : Complex.UnitDisc) (n : ℕ+) => ⟨↑z ^ ↑n, ⋯⟩ }

source

@[simp]

theorem Complex.UnitDisc.coe_pow (z : UnitDisc) (n : ℕ+) :

↑(z ^ n) = ↑z ^ ↑n

source

theorem Complex.UnitDisc.continuous_pow (n : ℕ+) :

Continuous fun (x : UnitDisc) => x ^ n

source

@[simp]

theorem Complex.UnitDisc.pow_eq_zero {z : UnitDisc} {n : ℕ+} :

z ^ n = 0 ↔ z = 0

source

instance Complex.UnitDisc.instPNatPowAssoc :

PNatPowAssoc UnitDisc

source

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

Filter.Tendsto (fun (n : ℕ+) => z ^ n) Filter.atTop (nhds 0)

source

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

ℝ

Real part of a point of the unit disc.

Equations

z.re = (↑z).re

Instances For

source

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

ℝ

Imaginary part of a point of the unit disc.

Equations

z.im = (↑z).im

Instances For

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

@[simp]

theorem Complex.UnitDisc.re_zero :

re 0 = 0

source

@[simp]

theorem Complex.UnitDisc.im_zero :

im 0 = 0

source

@[implicit_reducible]

instance Complex.UnitDisc.instStar :

Star UnitDisc

Conjugate point of the unit disc.

Equations

Complex.UnitDisc.instStar = { star := fun (z : Complex.UnitDisc) => Complex.UnitDisc.mk ((starRingEnd ℂ) ↑z) ⋯ }

source

@[deprecated Star.star (since := "2026-01-06")]

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

UnitDisc

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

Equations

z.conj = star z

Instances For

source

@[simp]

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

↑(star z) = (starRingEnd ℂ) ↑z

source

@[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

@[simp]

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

star z = 0 ↔ z = 0

source

@[simp]

theorem Complex.UnitDisc.star_zero :

star 0 = 0

source

@[implicit_reducible]

instance Complex.UnitDisc.instInvolutiveStar :

InvolutiveStar UnitDisc

Equations

Complex.UnitDisc.instInvolutiveStar = { toStar := Complex.UnitDisc.instStar, star_involutive := ⋯ }

source

@[deprecated star_star (since := "2026-01-06")]

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

star (star z) = z

source

@[simp]

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

star (-z) = -star z

source

@[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

@[simp]

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

(star z).re = z.re

source

@[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

@[simp]

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

(star z).im = -z.im

source

@[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

@[implicit_reducible]

instance Complex.UnitDisc.instStarMul :

StarMul UnitDisc

Equations

Complex.UnitDisc.instStarMul = { toInvolutiveStar := Complex.UnitDisc.instInvolutiveStar, star_mul := Complex.UnitDisc.instStarMul._proof_2 }

source

@[deprecated star_mul' (since := "2026-01-06")]

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

star (z * w) = star z * star w

Documentation

Mathlib.Analysis.Complex.UnitDisc.Basic

Poincaré disc #