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 = ↥(Subsemigroup.unitBall ℂ)

Instances For

source

@[instance_reducible]

noncomputable instance Complex.instTopologicalSpaceUnitDisc :

TopologicalSpace UnitDisc

Equations

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

source

def Complex.UnitClosedDisc :

Type

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

Equations

Complex.UnitClosedDisc = ↥(Submonoid.unitClosedBall ℂ)

Instances For

source

@[instance_reducible]

noncomputable instance Complex.instTopologicalSpaceUnitClosedDisc :

TopologicalSpace UnitClosedDisc

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.term𝕔𝔻 :

Lean.ParserDescr

The complex closed 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

@[instance_reducible]

noncomputable instance Complex.UnitDisc.instCommSemigroup :

CommSemigroup UnitDisc

Equations

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

source

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

@[instance_reducible]

noncomputable instance Complex.UnitDisc.instHasDistribNeg :

HasDistribNeg UnitDisc

Equations

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

source

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

@[instance_reducible]

noncomputable instance Complex.UnitDisc.instInhabited :

Inhabited UnitDisc

Equations

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

source

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

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

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

@[simp]

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

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

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

@[instance_reducible]

instance Complex.UnitDisc.instInvolutiveStar :

InvolutiveStar UnitDisc

Equations

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

source

@[simp]

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

star (-z) = -star z

source

@[simp]

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

(star z).re = z.re

source

@[simp]

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

(star z).im = -z.im

source

@[instance_reducible]

instance Complex.UnitDisc.instStarMul :

StarMul UnitDisc

Equations

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

source

def Complex.UnitClosedDisc.coe :

UnitClosedDisc → ℂ

Coercion to ℂ.

Equations

Complex.UnitClosedDisc.coe = Subtype.val

Instances For

source

@[instance_reducible]

noncomputable instance Complex.UnitClosedDisc.instMonoidWithZero :

MonoidWithZero UnitClosedDisc

Equations

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

source

instance Complex.UnitClosedDisc.instIsCancelMulZero :

IsCancelMulZero UnitClosedDisc

source

@[instance_reducible]

noncomputable instance Complex.UnitClosedDisc.instHasDistribNeg :

HasDistribNeg UnitClosedDisc

Equations

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

source

@[instance_reducible]

instance Complex.UnitClosedDisc.instCoe :

Coe UnitClosedDisc ℂ

Equations

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

source

theorem Complex.UnitClosedDisc.coe_injective :

Function.Injective UnitClosedDisc.coe

source

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

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

source

@[simp]

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

↑z = ↑w ↔ z = w

source

theorem Complex.UnitClosedDisc.isEmbedding_coe :

Topology.IsEmbedding UnitClosedDisc.coe

source

theorem Complex.UnitClosedDisc.continuous_coe :

Continuous UnitClosedDisc.coe

source

theorem Complex.UnitClosedDisc.norm_le_one (z : UnitClosedDisc) :

‖↑z‖ ≤ 1

source

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

‖↑z‖ ^ 2 ≤ 1

source

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

normSq ↑z ≤ 1

source

@[simp]

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

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

source

@[simp]

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

↑(-z) = -↑z

source

def Complex.UnitClosedDisc.mk (z : ℂ) (hz : ‖z‖ ≤ 1) :

UnitClosedDisc

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.UnitClosedDisc.mk z hz = ⟨z, ⋯⟩

Instances For

source

instance Complex.UnitClosedDisc.instCanLiftCoeLeRealNormOfNat :

CanLift ℂ UnitClosedDisc UnitClosedDisc.coe fun (x : ℂ) => ‖x‖ ≤ 1

source

def Complex.UnitClosedDisc.casesOn {motive : UnitClosedDisc → Sort u_1} (mk : (z : ℂ) → (hz : ‖z‖ ≤ 1) → motive (mk z hz)) (z : UnitClosedDisc) :

motive z

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

Equations

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

Instances For

source

@[simp]

theorem Complex.UnitClosedDisc.casesOn_mk {motive : UnitClosedDisc → Sort u_1} (mk' : (z : ℂ) → (hz : ‖z‖ ≤ 1) → motive (mk z hz)) {z : ℂ} (hz : ‖z‖ ≤ 1) :

UnitClosedDisc.casesOn mk' (mk z hz) = mk' z hz

source

@[simp]

theorem Complex.UnitClosedDisc.coe_mk (z : ℂ) (hz : ‖z‖ ≤ 1) :

↑(mk z hz) = z

source

@[simp]

theorem Complex.UnitClosedDisc.mk_coe (z : UnitClosedDisc) (hz : ‖↑z‖ ≤ 1 := ⋯) :

mk (↑z) hz = z

source

@[simp]

theorem Complex.UnitClosedDisc.mk_inj {z w : ℂ} (hz : ‖z‖ ≤ 1) (hw : ‖w‖ ≤ 1) :

mk z hz = mk w hw ↔ z = w

source

theorem Complex.UnitClosedDisc.forall {p : UnitClosedDisc → Prop} :

(∀ (z : UnitClosedDisc), p z) ↔ ∀ (z : ℂ) (hz : ‖z‖ ≤ 1), p (mk z hz)

source

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

(∃ (z : UnitClosedDisc), p z) ↔ ∃ (z : ℂ) (hz : ‖z‖ ≤ 1), p (mk z hz)

source

@[simp]

theorem Complex.UnitClosedDisc.mk_neg (z : ℂ) (hz : ‖-z‖ ≤ 1) :

mk (-z) hz = -mk z ⋯

source

@[simp]

theorem Complex.UnitClosedDisc.coe_zero :

↑0 = 0

source

@[simp]

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

↑z = 0 ↔ z = 0

source

@[simp]

theorem Complex.UnitClosedDisc.mk_zero :

mk 0 mk_zero._proof_1 = 0

source

@[simp]

theorem Complex.UnitClosedDisc.mk_eq_zero {z : ℂ} (hz : ‖z‖ ≤ 1) :

mk z hz = 0 ↔ z = 0

source

@[simp]

theorem Complex.UnitClosedDisc.coe_one :

↑1 = 1

source

@[simp]

theorem Complex.UnitClosedDisc.coe_eq_one {z : UnitClosedDisc} :

↑z = 1 ↔ z = 1

source

@[simp]

theorem Complex.UnitClosedDisc.mk_one :

mk 1 mk_one._proof_1 = 1

source

@[simp]

theorem Complex.UnitClosedDisc.mk_eq_one {z : ℂ} (hz : ‖z‖ ≤ 1) :

mk z hz = 1 ↔ z = 1

source

@[instance_reducible]

noncomputable instance Complex.UnitClosedDisc.instInhabited :

Inhabited UnitClosedDisc

Equations

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

source

@[instance_reducible]

noncomputable instance Complex.UnitClosedDisc.instMulActionCircle :

MulAction Circle UnitClosedDisc

Equations

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

source

instance Complex.UnitClosedDisc.instIsScalarTowerCircle :

IsScalarTower Circle Circle UnitClosedDisc

source

instance Complex.UnitClosedDisc.instIsScalarTowerCircle_1 :

IsScalarTower Circle UnitClosedDisc UnitClosedDisc

source

instance Complex.UnitClosedDisc.instSMulCommClassCircle :

SMulCommClass Circle UnitClosedDisc UnitClosedDisc

source

instance Complex.UnitClosedDisc.instSMulCommClassCircle_1 :

SMulCommClass UnitClosedDisc Circle UnitClosedDisc

source

@[instance_reducible]

noncomputable instance Complex.UnitClosedDisc.instMulActionClosedBall :

MulAction UnitClosedDisc UnitDisc

Equations

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

source

instance Complex.UnitClosedDisc.instIsScalarTower_closedBall_closedBall :

IsScalarTower UnitClosedDisc UnitClosedDisc UnitDisc

source

instance Complex.UnitClosedDisc.instIsScalarTower_closedBall :

IsScalarTower UnitClosedDisc UnitDisc UnitDisc

source

instance Complex.UnitClosedDisc.instSMulCommClass_closedBall_left :

SMulCommClass UnitClosedDisc UnitDisc UnitDisc

source

instance Complex.UnitClosedDisc.instSMulCommClass_closedBall_right :

SMulCommClass UnitDisc UnitClosedDisc UnitDisc

source

instance Complex.UnitClosedDisc.instSMulCommClass_circle_closedBall :

SMulCommClass Circle UnitClosedDisc UnitDisc

source

instance Complex.UnitClosedDisc.instSMulCommClass_closedBall_circle :

SMulCommClass UnitClosedDisc Circle UnitDisc

source

@[simp]

theorem Complex.UnitClosedDisc.coe_closedBall_smul (z : UnitClosedDisc) (w : UnitDisc) :

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

source

@[simp]

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

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

source

instance Complex.UnitClosedDisc.instSMulCommClassCircle_2 :

SMulCommClass UnitClosedDisc Circle UnitClosedDisc

source

@[instance_reducible]

instance Complex.UnitClosedDisc.instPowNat :

Pow UnitClosedDisc ℕ

Equations

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

source

@[simp]

theorem Complex.UnitClosedDisc.coe_pow (z : UnitClosedDisc) (n : ℕ) :

↑(z ^ n) = ↑z ^ n

source

theorem Complex.UnitClosedDisc.continuous_pow (n : ℕ) :

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

source

instance Complex.UnitClosedDisc.instNatPowAssoc :

NatPowAssoc UnitClosedDisc

source

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

ℝ

Real part of a point of the unit disc.

Equations

z.re = (↑z).re

Instances For

source

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

ℝ

Imaginary part of a point of the unit disc.

Equations

z.im = (↑z).im

Instances For

source

@[simp]

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

(↑z).re = z.re

source

@[simp]

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

(↑z).im = z.im

source

@[simp]

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

(-z).re = -z.re

source

@[simp]

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

(-z).im = -z.im

source

@[simp]

theorem Complex.UnitClosedDisc.re_zero :

re 0 = 0

source

@[simp]

theorem Complex.UnitClosedDisc.im_zero :

im 0 = 0

source

@[instance_reducible]

instance Complex.UnitClosedDisc.instStar :

Star UnitClosedDisc

Conjugate point of the unit disc.

Equations

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

source

@[simp]

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

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

source

@[simp]

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

star z = 0 ↔ z = 0

source

@[simp]

theorem Complex.UnitClosedDisc.star_zero :

star 0 = 0

source

@[instance_reducible]

instance Complex.UnitClosedDisc.instInvolutiveStar :

InvolutiveStar UnitClosedDisc

Equations

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

source

@[simp]

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

star (-z) = -star z

source

@[simp]

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

(star z).re = z.re

source

@[simp]

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

(star z).im = -z.im

source

@[instance_reducible]

instance Complex.UnitClosedDisc.instStarMul :

StarMul UnitClosedDisc

Equations

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

Documentation

Mathlib.Analysis.Complex.UnitDisc.Basic

Poincaré disc #