mathlibdocumentation

analysis.special_functions.complex.circle

Maps on the unit circle #

In this file we prove some basic lemmas about exp_map_circle and the restriction of complex.arg to the unit circle. These two maps define a local equivalence between circle and ℝ, see circle.arg_local_equiv and circle.arg_equiv, that sends the whole circle to (-π, π].

@[simp]
theorem circle.arg_eq_arg {z w : circle} :
z.arg = w.arg z = w
theorem arg_exp_map_circle {x : } (h₁ : -real.pi < x) (h₂ : x real.pi) :
@[simp]
theorem exp_map_circle_arg (z : circle) :
@[simp]
@[simp]
noncomputable def circle.arg_local_equiv  :

complex.arg ∘ coe and exp_map_circle define a local equivalence between circle andwithsource = set.univandtarget = set.Ioc (-π) π.

Equations
@[simp]
@[simp]
@[simp]
@[simp]
noncomputable def circle.arg_equiv  :

complex.arg and exp_map_circle define an equivalence between circle and(-π, π].

Equations
theorem exp_map_circle_eq_exp_map_circle {x y : } :
∃ (m : ), x = y + (m) *
@[simp]
theorem exp_map_circle_two_pi  :
= 1