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

theorem circle.injective_arg :

Function.Injective fun z => Complex.arg ↑z

@[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]

theorem expMapCircle_arg (z : { x // x ∈ circle }) :

↑expMapCircle (Complex.arg ↑z) = z

@[simp]

theorem circle.argLocalEquiv_source :

circle.argLocalEquiv.source = Set.univ

@[simp]

theorem circle.argLocalEquiv_symm_apply :

↑(LocalEquiv.symm circle.argLocalEquiv) = ↑expMapCircle

@[simp]

theorem circle.argLocalEquiv_target :

circle.argLocalEquiv.target = Set.Ioc (-Real.pi) Real.pi

@[simp]

theorem circle.argLocalEquiv_apply :

↑circle.argLocalEquiv = Complex.arg ∘ Subtype.val

noncomputable def circle.argLocalEquiv :

LocalEquiv { x // x ∈ circle } ℝ

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 }) :

↑(↑circle.argEquiv z) = Complex.arg ↑z

@[simp]

theorem circle.argEquiv_symm_apply :

↑circle.argEquiv.symm = ↑expMapCircle ∘ Subtype.val

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 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)

theorem periodic_expMapCircle :

Function.Periodic (↑expMapCircle) (2 * Real.pi)

@[simp]

theorem expMapCircle_two_pi :

↑expMapCircle (2 * Real.pi) = 1

theorem expMapCircle_sub_two_pi (x : ℝ) :

↑expMapCircle (x - 2 * Real.pi) = ↑expMapCircle x

theorem expMapCircle_add_two_pi (x : ℝ) :

↑expMapCircle (x + 2 * Real.pi) = ↑expMapCircle x

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

{ x // x ∈ circle }

expMapCircle, applied to a Real.Angle.

Instances For

@[simp]

theorem Real.Angle.expMapCircle_coe (x : ℝ) :

Real.Angle.expMapCircle ↑x = ↑expMapCircle x

theorem Real.Angle.coe_expMapCircle (θ : Real.Angle) :

↑(Real.Angle.expMapCircle θ) = ↑(Real.Angle.cos θ) + ↑(Real.Angle.sin θ) * Complex.I

@[simp]

theorem Real.Angle.expMapCircle_zero :

Real.Angle.expMapCircle 0 = 1

@[simp]

theorem Real.Angle.expMapCircle_neg (θ : Real.Angle) :

Real.Angle.expMapCircle (-θ) = (Real.Angle.expMapCircle θ)⁻¹

@[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 θ)) = θ