mathlib3 documentation

analysis.special_functions.complex.circle

Maps on the unit circle #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove some basic lemmas about exp_map_circle and the restriction of complex.arg to the unit circle. These two maps define a local equivalence between circle and ℝ, see circle.arg_local_equiv and circle.arg_equiv, that sends the whole circle to (-π, π].

theorem circle.injective_arg :

function.injective (λ (z : ↥circle), ↑z.arg)

@[simp]

theorem circle.arg_eq_arg {z w : ↥circle} :

↑z.arg = ↑w.arg ↔ z = w

theorem arg_exp_map_circle {x : ℝ} (h₁ : -real.pi < x) (h₂ : x ≤ real.pi) :

↑(⇑exp_map_circle x).arg = x

@[simp]

theorem exp_map_circle_arg (z : ↥circle) :

⇑exp_map_circle ↑z.arg = z

@[simp]

theorem circle.arg_local_equiv_symm_apply :

⇑(circle.arg_local_equiv.symm) = ⇑exp_map_circle

@[simp]

theorem circle.arg_local_equiv_source :

circle.arg_local_equiv.source = set.univ

noncomputable def circle.arg_local_equiv :

local_equiv ↥circle ℝ

complex.arg ∘ coe and exp_map_circle define a local equivalence between circle andℝwithsource = set.univandtarget = set.Ioc (-π) π`.

Equations

circle.arg_local_equiv = {to_fun := complex.arg ∘ coe, inv_fun := ⇑exp_map_circle, source := set.univ ↥circle, target := set.Ioc (-real.pi) real.pi, map_source' := circle.arg_local_equiv._proof_1, map_target' := circle.arg_local_equiv._proof_2, left_inv' := circle.arg_local_equiv._proof_3, right_inv' := circle.arg_local_equiv._proof_4}

@[simp]

theorem circle.arg_local_equiv_target :

circle.arg_local_equiv.target = set.Ioc (-real.pi) real.pi

@[simp]

theorem circle.arg_local_equiv_apply :

⇑circle.arg_local_equiv = complex.arg ∘ coe

@[simp]

theorem circle.arg_equiv_apply_coe (z : ↥circle) :

↑(⇑circle.arg_equiv z) = ↑z.arg

@[simp]

theorem circle.arg_equiv_symm_apply :

⇑(circle.arg_equiv.symm) = ⇑exp_map_circle ∘ coe

noncomputable def circle.arg_equiv :

↥circle ≃ ↥(set.Ioc (-real.pi) real.pi)

complex.arg and exp_map_circle define an equivalence between circle and(-π, π]`.

Equations

circle.arg_equiv = {to_fun := λ (z : ↥circle), ⟨↑z.arg, _⟩, inv_fun := ⇑exp_map_circle ∘ coe, left_inv := circle.arg_equiv._proof_2, right_inv := circle.arg_equiv._proof_3}

theorem left_inverse_exp_map_circle_arg :

function.left_inverse ⇑exp_map_circle (complex.arg ∘ coe)

theorem inv_on_arg_exp_map_circle :

set.inv_on (complex.arg ∘ coe) ⇑exp_map_circle (set.Ioc (-real.pi) real.pi) set.univ

theorem surj_on_exp_map_circle_neg_pi_pi :

set.surj_on ⇑exp_map_circle (set.Ioc (-real.pi) real.pi) set.univ

theorem exp_map_circle_eq_exp_map_circle {x y : ℝ} :

⇑exp_map_circle x = ⇑exp_map_circle y ↔ ∃ (m : ℤ), x = y + ↑m * (2 * real.pi)

theorem periodic_exp_map_circle :

function.periodic ⇑exp_map_circle (2 * real.pi)

@[simp]

theorem exp_map_circle_two_pi :

⇑exp_map_circle (2 * real.pi) = 1

theorem exp_map_circle_sub_two_pi (x : ℝ) :

⇑exp_map_circle (x - 2 * real.pi) = ⇑exp_map_circle x

theorem exp_map_circle_add_two_pi (x : ℝ) :

⇑exp_map_circle (x + 2 * real.pi) = ⇑exp_map_circle x

noncomputable def real.angle.exp_map_circle (θ : real.angle) :

exp_map_circle, applied to a real.angle.

Equations

θ.exp_map_circle = periodic_exp_map_circle.lift θ

@[simp]

theorem real.angle.exp_map_circle_coe (x : ℝ) :

↑x.exp_map_circle = ⇑exp_map_circle x

theorem real.angle.coe_exp_map_circle (θ : real.angle) :

↑(θ.exp_map_circle) = ↑(θ.cos) + ↑(θ.sin) * complex.I

@[simp]

theorem real.angle.exp_map_circle_zero :

0.exp_map_circle = 1

@[simp]

theorem real.angle.exp_map_circle_neg (θ : real.angle) :

(-θ).exp_map_circle = (θ.exp_map_circle)⁻¹

@[simp]

theorem real.angle.exp_map_circle_add (θ₁ θ₂ : real.angle) :

(θ₁ + θ₂).exp_map_circle = θ₁.exp_map_circle * θ₂.exp_map_circle

@[simp]

theorem real.angle.arg_exp_map_circle (θ : real.angle) :

↑(↑(θ.exp_map_circle).arg) = θ