# Maps on the unit circle #

In this file we prove some basic lemmas about expMapCircle and the restriction of Complex.arg to the unit circle. These two maps define a partial equivalence between circle and ℝ, see circle.argPartialEquiv and circle.argEquiv, that sends the whole circle to (-π, π].

theorem Circle.injective_arg :
Function.Injective fun (z : Circle) => (↑z).arg
@[simp]
theorem Circle.arg_eq_arg {z : Circle} {w : Circle} :
(↑z).arg = (↑w).arg z = w
theorem Circle.arg_exp {x : } (h₁ : ) (h₂ : ) :
(↑(Circle.exp x)).arg = x
@[simp]
theorem Circle.exp_arg (z : Circle) :
Circle.exp (↑z).arg = z
@[deprecated Circle.arg_exp]
theorem arg_expMapCircle {x : } (h₁ : ) (h₂ : ) :
(↑(Circle.exp x)).arg = x

Alias of Circle.arg_exp.

@[deprecated Circle.exp_arg]
theorem expMapCircle_arg (z : Circle) :
Circle.exp (↑z).arg = z

Alias of Circle.exp_arg.

@[simp]
noncomputable def Circle.argPartialEquiv :

Complex.arg ∘ (↑) and expMapCircle define a partial equivalence between circle and ℝ with source = Set.univ and target = Set.Ioc (-π) π.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Circle.argEquiv_apply_coe (z : Circle) :
(Circle.argEquiv z) = (↑z).arg
@[simp]
theorem Circle.argEquiv_symm_apply :
Circle.argEquiv.symm = Subtype.val
noncomputable def Circle.argEquiv :

Complex.arg and expMapCircle define an equivalence between circle and (-π, π].

Equations
Instances For
theorem Circle.invOn_arg_exp :
Set.InvOn (Complex.arg Subtype.val) (⇑Circle.exp) Set.univ
theorem Circle.exp_eq_exp {x : } {y : } :
Circle.exp x = Circle.exp y ∃ (m : ), x = y + m * (2 * Real.pi)
@[simp]
theorem Circle.exp_two_pi :
Circle.exp (2 * Real.pi) = 1
theorem Circle.exp_int_mul_two_pi (n : ) :
Circle.exp (n * (2 * Real.pi)) = 1
theorem Circle.exp_two_pi_mul_int (n : ) :
Circle.exp ( * n) = 1
theorem Circle.exp_eq_one {r : } :
Circle.exp r = 1 ∃ (n : ), r = n * (2 * Real.pi)
theorem Circle.exp_sub_two_pi (x : ) :
Circle.exp (x - ) = Circle.exp x
theorem Circle.exp_add_two_pi (x : ) :
Circle.exp (x + ) = Circle.exp x
@[deprecated Circle.leftInverse_exp_arg]

Alias of Circle.leftInverse_exp_arg.

@[deprecated Circle.surjOn_exp_neg_pi_pi]

Alias of Circle.surjOn_exp_neg_pi_pi.

@[deprecated Circle.invOn_arg_exp]
theorem invOn_arg_expMapCircle :
Set.InvOn (Complex.arg Subtype.val) (⇑Circle.exp) Set.univ

Alias of Circle.invOn_arg_exp.

@[deprecated Circle.exp_eq_exp]
theorem expMapCircle_eq_expMapCircle {x : } {y : } :
Circle.exp x = Circle.exp y ∃ (m : ), x = y + m * (2 * Real.pi)

Alias of Circle.exp_eq_exp.

@[deprecated Circle.periodic_exp]

Alias of Circle.periodic_exp.

@[deprecated Circle.exp_two_pi]
theorem expMapCircle_two_pi :
Circle.exp (2 * Real.pi) = 1

Alias of Circle.exp_two_pi.

@[deprecated Circle.exp_sub_two_pi]
theorem expMapCircle_sub_two_pi (x : ) :
Circle.exp (x - ) = Circle.exp x

Alias of Circle.exp_sub_two_pi.

theorem expMapCircle_add_two_pi (x : ) :
Circle.exp (x + ) = Circle.exp x

Alias of Circle.exp_add_two_pi.

noncomputable def Real.Angle.toCircle (θ : Real.Angle) :

Circle.exp, applied to a Real.Angle.

Equations
Instances For
@[simp]
theorem Real.Angle.toCircle_coe (x : ) :
(↑x).toCircle = Circle.exp x
theorem Real.Angle.coe_toCircle (θ : Real.Angle) :
θ.toCircle = θ.cos + θ.sin * Complex.I
@[simp]
theorem Real.Angle.toCircle_neg (θ : Real.Angle) :
(-θ).toCircle = θ.toCircle⁻¹
@[simp]
theorem Real.Angle.toCircle_add (θ₁ : Real.Angle) (θ₂ : Real.Angle) :
(θ₁ + θ₂).toCircle = θ₁.toCircle * θ₂.toCircle
@[simp]
theorem Real.Angle.arg_toCircle (θ : Real.Angle) :
(↑θ.toCircle).arg = θ
@[deprecated Real.Angle.toCircle]

Alias of Real.Angle.toCircle.

Circle.exp, applied to a Real.Angle.

Equations
Instances For
@[deprecated Real.Angle.toCircle_coe]
theorem Real.Angle.expMapCircle_coe (x : ) :
(↑x).toCircle = Circle.exp x

Alias of Real.Angle.toCircle_coe.

@[deprecated Real.Angle.coe_toCircle]
theorem Real.Angle.coe_expMapCircle (θ : Real.Angle) :
θ.toCircle = θ.cos + θ.sin * Complex.I

Alias of Real.Angle.coe_toCircle.

@[deprecated Real.Angle.toCircle_zero]

Alias of Real.Angle.toCircle_zero.

@[deprecated Real.Angle.toCircle_neg]
theorem Real.Angle.expMapCircle_neg (θ : Real.Angle) :
(-θ).toCircle = θ.toCircle⁻¹

Alias of Real.Angle.toCircle_neg.

theorem Real.Angle.expMapCircle_add (θ₁ : Real.Angle) (θ₂ : Real.Angle) :
(θ₁ + θ₂).toCircle = θ₁.toCircle * θ₂.toCircle

Alias of Real.Angle.toCircle_add.

@[deprecated Real.Angle.arg_toCircle]
theorem Real.Angle.arg_expMapCircle (θ : Real.Angle) :
(↑θ.toCircle).arg = θ

Alias of Real.Angle.arg_toCircle.

### Map from AddCircle to Circle#

theorem AddCircle.scaled_exp_map_periodic {T : } :
Function.Periodic (fun (x : ) => Circle.exp ( / T * x)) T
noncomputable def AddCircle.toCircle {T : } :

The canonical map fun x => exp (2 π i x / T) from ℝ / ℤ • T to the unit circle in ℂ. If T = 0 we understand this as the constant function 1.

Equations
Instances For
theorem AddCircle.toCircle_apply_mk {T : } (x : ) :
= Circle.exp ( / T * x)
theorem AddCircle.toCircle_add {T : } (x : ) (y : ) :
(x + y).toCircle = x.toCircle * y.toCircle
theorem AddCircle.continuous_toCircle {T : } :
theorem AddCircle.injective_toCircle {T : } (hT : T 0) :
@[simp]
theorem AddCircle.homeomorphCircle'_apply (θ : Real.Angle) :
@[simp]
theorem AddCircle.homeomorphCircle'_symm_apply (x : Circle) :
= (↑x).arg

The homeomorphism between AddCircle (2 * π) and Circle.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddCircle.homeomorphCircle'_apply_mk (x : ) :
The homeomorphism between AddCircle and Circle.
Alias of isLocalHomeomorph_circleExp.