Documentation

Mathlib.Analysis.SpecialFunctions.Complex.Circle

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 (-π, π].

@[simp]
theorem circle.arg_eq_arg {z : circle} {w : circle} :
Complex.arg z = Complex.arg w z = w
theorem arg_expMapCircle {x : } (h₁ : -Real.pi < x) (h₂ : x Real.pi) :
@[simp]
theorem expMapCircle_arg (z : circle) :

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]
    noncomputable def circle.argEquiv :

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem expMapCircle_eq_expMapCircle {x : } {y : } :
      expMapCircle x = expMapCircle y ∃ (m : ), x = y + m * (2 * Real.pi)