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 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) :
@[simp]
theorem expMapCircle_arg (z : { x // x circle }) :
noncomputable def circle.argLocalEquiv :

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

Instances For
    @[simp]
    theorem circle.argEquiv_apply_coe (z : { x // x circle }) :
    @[simp]
    noncomputable def circle.argEquiv :
    { x // x circle } ↑(Set.Ioc (-Real.pi) Real.pi)

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

    Instances For
      theorem expMapCircle_eq_expMapCircle {x : } {y : } :
      expMapCircle x = expMapCircle y m, x = y + m * (2 * Real.pi)
      noncomputable def Real.Angle.expMapCircle (θ : Real.Angle) :
      { x // x circle }

      expMapCircle, applied to a Real.Angle.

      Instances For