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 local equivalence between circle
and ℝ
, see
circle.argLocalEquiv
and circle.argEquiv
, that sends the whole circle to (-π, π]
.
@[simp]
theorem
circle.arg_eq_arg
{z : { x // x ∈ circle }}
{w : { x // x ∈ circle }}
:
Complex.arg ↑z = Complex.arg ↑w ↔ z = w
theorem
arg_expMapCircle
{x : ℝ}
(h₁ : -Real.pi < x)
(h₂ : x ≤ Real.pi)
:
Complex.arg ↑(↑expMapCircle x) = x
@[simp]
@[simp]
@[simp]
Complex.arg ∘ (↑)
and expMapCircle
define a local equivalence between circle
and ℝ
with source = Set.univ
and target = Set.Ioc (-π) π
.
Instances For
@[simp]
@[simp]
Complex.arg
and expMapCircle
define an equivalence between circle
and (-π, π]
.
Instances For
theorem
leftInverse_expMapCircle_arg :
Function.LeftInverse (↑expMapCircle) (Complex.arg ∘ Subtype.val)
theorem
invOn_arg_expMapCircle :
Set.InvOn (Complex.arg ∘ Subtype.val) (↑expMapCircle) (Set.Ioc (-Real.pi) Real.pi) Set.univ
theorem
surjOn_expMapCircle_neg_pi_pi :
Set.SurjOn (↑expMapCircle) (Set.Ioc (-Real.pi) Real.pi) Set.univ
theorem
expMapCircle_eq_expMapCircle
{x : ℝ}
{y : ℝ}
:
↑expMapCircle x = ↑expMapCircle y ↔ ∃ m, x = y + ↑m * (2 * Real.pi)
expMapCircle
, applied to a Real.Angle
.
Instances For
@[simp]
theorem
Real.Angle.coe_expMapCircle
(θ : Real.Angle)
:
↑(Real.Angle.expMapCircle θ) = ↑(Real.Angle.cos θ) + ↑(Real.Angle.sin θ) * Complex.I
@[simp]
@[simp]
theorem
Real.Angle.expMapCircle_add
(θ₁ : Real.Angle)
(θ₂ : Real.Angle)
:
Real.Angle.expMapCircle (θ₁ + θ₂) = Real.Angle.expMapCircle θ₁ * Real.Angle.expMapCircle θ₂
@[simp]
theorem
Real.Angle.arg_expMapCircle
(θ : Real.Angle)
:
↑(Complex.arg ↑(Real.Angle.expMapCircle θ)) = θ