mathlib3 documentation

analysis.complex.unit_disc.basic

Poincaré disc #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define complex.unit_disc to be the unit disc in the complex plane. We also introduce some basic operations on this disc.

source
@[protected, instance]
noncomputable def complex.unit_disc.topological_space  :
topological_space complex.unit_disc
source
@[protected, instance]
def complex.unit_disc.has_coe  :
has_coe complex.unit_disc ℂ
source
def complex.unit_disc  :
Type

Complex unit disc.

Equations
Instances for complex.unit_disc
source
@[protected, instance]
noncomputable def complex.unit_disc.has_distrib_neg  :
has_distrib_neg complex.unit_disc
source
@[protected, instance]
noncomputable def complex.unit_disc.comm_semigroup  :
comm_semigroup complex.unit_disc
source
theorem complex.unit_disc.coe_injective  :
function.injective coe
source
theorem complex.unit_disc.abs_lt_one (z : complex.unit_disc) :
⇑complex.abs ↑z < 1
source
theorem complex.unit_disc.abs_ne_one (z : complex.unit_disc) :
⇑complex.abs ↑z ≠ 1
source
theorem complex.unit_disc.norm_sq_lt_one (z : complex.unit_disc) :
⇑complex.norm_sq ↑z < 1
source
theorem complex.unit_disc.coe_ne_one (z : complex.unit_disc) :
↑z ≠ 1
source
theorem complex.unit_disc.coe_ne_neg_one (z : complex.unit_disc) :
↑z ≠ -1
source
theorem complex.unit_disc.one_add_coe_ne_zero (z : complex.unit_disc) :
1 + ↑z ≠ 0
source
@[simp, norm_cast]
theorem complex.unit_disc.coe_mul (z w : complex.unit_disc) :
↑(z * w) = ↑z * ↑w
source
def complex.unit_disc.mk (z : ℂ) (hz : ⇑complex.abs z < 1) :
complex.unit_disc

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
source
@[simp]
theorem complex.unit_disc.coe_mk (z : ℂ) (hz : ⇑complex.abs z < 1) :
↑(complex.unit_disc.mk z hz) = z
source
@[simp]
theorem complex.unit_disc.mk_coe (z : complex.unit_disc) (hz : ⇑complex.abs ↑z < 1 := _) :
complex.unit_disc.mk ↑z hz = z
source
@[simp]
theorem complex.unit_disc.mk_neg (z : ℂ) (hz : ⇑complex.abs (-z) < 1) :
complex.unit_disc.mk (-z) hz = -complex.unit_disc.mk z _
source
@[protected, instance]
noncomputable def complex.unit_disc.semigroup_with_zero  :
semigroup_with_zero complex.unit_disc
Equations
source
@[simp]
theorem complex.unit_disc.coe_zero  :
↑0 = 0
source
@[simp]
theorem complex.unit_disc.coe_eq_zero {z : complex.unit_disc} :
↑z = 0 ↔ z = 0
source
@[protected, instance]
noncomputable def complex.unit_disc.inhabited  :
inhabited complex.unit_disc
Equations
source
@[protected, instance]
noncomputable def complex.unit_disc.circle_action  :
mul_action ↥circle complex.unit_disc
Equations
source
@[protected, instance]
def complex.unit_disc.is_scalar_tower_circle_circle  :
is_scalar_tower ↥circle ↥circle complex.unit_disc
source
@[protected, instance]
def complex.unit_disc.is_scalar_tower_circle  :
is_scalar_tower ↥circle complex.unit_disc complex.unit_disc
source
@[protected, instance]
def complex.unit_disc.smul_comm_class_circle  :
smul_comm_class ↥circle complex.unit_disc complex.unit_disc
source
@[protected, instance]
def complex.unit_disc.smul_comm_class_circle'  :
smul_comm_class complex.unit_disc ↥circle complex.unit_disc
source
@[simp, norm_cast]
theorem complex.unit_disc.coe_smul_circle (z : ↥circle) (w : complex.unit_disc) :
↑(z • w) = ↑z * ↑w
source
@[protected, instance]
noncomputable def complex.unit_disc.closed_ball_action  :
mul_action ↥(metric.closed_ball 0 1) complex.unit_disc
Equations
source
@[protected, instance]
def complex.unit_disc.is_scalar_tower_closed_ball_closed_ball  :
is_scalar_tower ↥(metric.closed_ball 0 1) ↥(metric.closed_ball 0 1) complex.unit_disc
source
@[protected, instance]
def complex.unit_disc.is_scalar_tower_closed_ball  :
is_scalar_tower ↥(metric.closed_ball 0 1) complex.unit_disc complex.unit_disc
source
@[protected, instance]
def complex.unit_disc.smul_comm_class_closed_ball  :
smul_comm_class ↥(metric.closed_ball 0 1) complex.unit_disc complex.unit_disc
source
@[protected, instance]
def complex.unit_disc.smul_comm_class_closed_ball'  :
smul_comm_class complex.unit_disc ↥(metric.closed_ball 0 1) complex.unit_disc
source
@[protected, instance]
def complex.unit_disc.smul_comm_class_circle_closed_ball  :
smul_comm_class ↥circle ↥(metric.closed_ball 0 1) complex.unit_disc
source
@[protected, instance]
def complex.unit_disc.smul_comm_class_closed_ball_circle  :
smul_comm_class ↥(metric.closed_ball 0 1) ↥circle complex.unit_disc
source
@[simp, norm_cast]
theorem complex.unit_disc.coe_smul_closed_ball (z : ↥(metric.closed_ball 0 1)) (w : complex.unit_disc) :
↑(z • w) = ↑z * ↑w
source
def complex.unit_disc.re (z : complex.unit_disc) :
ℝ

Real part of a point of the unit disc.

Equations
source
def complex.unit_disc.im (z : complex.unit_disc) :
ℝ

Imaginary part of a point of the unit disc.

Equations
source
@[simp, norm_cast]
theorem complex.unit_disc.re_coe (z : complex.unit_disc) :
↑z.re = z.re
source
@[simp, norm_cast]
theorem complex.unit_disc.im_coe (z : complex.unit_disc) :
↑z.im = z.im
source
@[simp]
theorem complex.unit_disc.re_neg (z : complex.unit_disc) :
(-z).re = -z.re
source
@[simp]
theorem complex.unit_disc.im_neg (z : complex.unit_disc) :
(-z).im = -z.im
source
def complex.unit_disc.conj (z : complex.unit_disc) :
complex.unit_disc

Conjugate point of the unit disc.

Equations
source
@[simp, norm_cast]
theorem complex.unit_disc.coe_conj (z : complex.unit_disc) :
↑(z.conj) = ⇑(star_ring_end ℂ) ↑z
source
@[simp]
theorem complex.unit_disc.conj_zero  :
0.conj = 0
source
@[simp]
theorem complex.unit_disc.conj_conj (z : complex.unit_disc) :
z.conj.conj = z
source
@[simp]
theorem complex.unit_disc.conj_neg (z : complex.unit_disc) :
(-z).conj = -z.conj
source
@[simp]
theorem complex.unit_disc.re_conj (z : complex.unit_disc) :
z.conj.re = z.re
source
@[simp]
theorem complex.unit_disc.im_conj (z : complex.unit_disc) :
z.conj.im = -z.im
source
@[simp]
theorem complex.unit_disc.conj_mul (z w : complex.unit_disc) :
(z * w).conj = z.conj * w.conj