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

theorem Circle.injective_arg :

Function.Injective fun (z : Circle) => (↑z).arg

@[simp]

theorem Circle.arg_eq_arg {z w : Circle} :

(↑z).arg = (↑w).arg ↔ z = w

theorem Circle.arg_exp {x : ℝ} (h₁ : -Real.pi < x) (h₂ : x ≤ Real.pi) :

(↑(Circle.exp x)).arg = x

@[simp]

theorem Circle.exp_arg (z : Circle) :

Circle.exp (↑z).arg = z

@[deprecated Circle.arg_exp]

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

(↑(Circle.exp x)).arg = x

Alias of Circle.arg_exp.

@[deprecated Circle.exp_arg]

theorem expMapCircle_arg (z : Circle) :

Circle.exp (↑z).arg = z

Alias of Circle.exp_arg.

noncomputable def Circle.argPartialEquiv :

PartialEquiv 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]

theorem Circle.argPartialEquiv_target :

Circle.argPartialEquiv.target = Set.Ioc (-Real.pi) Real.pi

@[simp]

theorem Circle.argPartialEquiv_symm_apply :

↑Circle.argPartialEquiv.symm = ⇑Circle.exp

@[simp]

theorem Circle.argPartialEquiv_apply :

↑Circle.argPartialEquiv = Complex.arg ∘ Subtype.val

@[simp]

theorem Circle.argPartialEquiv_source :

Circle.argPartialEquiv.source = Set.univ

noncomputable def Circle.argEquiv :

Circle ≃ ↑(Set.Ioc (-Real.pi) Real.pi)

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

Equations

Circle.argEquiv = { toFun := fun (z : Circle) => ⟨(↑z).arg, ⋯⟩, invFun := ⇑Circle.exp ∘ Subtype.val, left_inv := ⋯, right_inv := Circle.argEquiv.proof_2 }

Instances For

@[simp]

theorem Circle.argEquiv_apply_coe (z : Circle) :

↑(Circle.argEquiv z) = (↑z).arg

@[simp]

theorem Circle.argEquiv_symm_apply :

⇑Circle.argEquiv.symm = ⇑Circle.exp ∘ Subtype.val

theorem Circle.leftInverse_exp_arg :

Function.LeftInverse (⇑Circle.exp) (Complex.arg ∘ Subtype.val)

theorem Circle.invOn_arg_exp :

Set.InvOn (Complex.arg ∘ Subtype.val) (⇑Circle.exp) (Set.Ioc (-Real.pi) Real.pi) Set.univ

theorem Circle.surjOn_exp_neg_pi_pi :

Set.SurjOn (⇑Circle.exp) (Set.Ioc (-Real.pi) Real.pi) Set.univ

theorem Circle.exp_eq_exp {x y : ℝ} :

Circle.exp x = Circle.exp y ↔ ∃ (m : ℤ), x = y + ↑m * (2 * Real.pi)

theorem Circle.periodic_exp :

Function.Periodic (⇑Circle.exp) (2 * Real.pi)

@[simp]

theorem Circle.exp_two_pi :

Circle.exp (2 * Real.pi) = 1

theorem Circle.exp_int_mul_two_pi (n : ℤ) :

Circle.exp (↑n * (2 * Real.pi)) = 1

theorem Circle.exp_two_pi_mul_int (n : ℤ) :

Circle.exp (2 * Real.pi * ↑n) = 1

theorem Circle.exp_eq_one {r : ℝ} :

Circle.exp r = 1 ↔ ∃ (n : ℤ), r = ↑n * (2 * Real.pi)

theorem Circle.exp_inj {r s : ℝ} :

Circle.exp r = Circle.exp s ↔ r ≡ s [PMOD 2 * Real.pi]

theorem Circle.exp_sub_two_pi (x : ℝ) :

Circle.exp (x - 2 * Real.pi) = Circle.exp x

theorem Circle.exp_add_two_pi (x : ℝ) :

Circle.exp (x + 2 * Real.pi) = Circle.exp x

@[deprecated Circle.leftInverse_exp_arg]

theorem leftInverse_expMapCircle_arg :

Function.LeftInverse (⇑Circle.exp) (Complex.arg ∘ Subtype.val)

Alias of Circle.leftInverse_exp_arg.

@[deprecated Circle.surjOn_exp_neg_pi_pi]

theorem surjOn_expMapCircle_neg_pi_pi :

Set.SurjOn (⇑Circle.exp) (Set.Ioc (-Real.pi) Real.pi) Set.univ

Alias of Circle.surjOn_exp_neg_pi_pi.

@[deprecated Circle.invOn_arg_exp]

theorem invOn_arg_expMapCircle :

Set.InvOn (Complex.arg ∘ Subtype.val) (⇑Circle.exp) (Set.Ioc (-Real.pi) Real.pi) Set.univ

Alias of Circle.invOn_arg_exp.

@[deprecated Circle.exp_eq_exp]

theorem expMapCircle_eq_expMapCircle {x y : ℝ} :

Circle.exp x = Circle.exp y ↔ ∃ (m : ℤ), x = y + ↑m * (2 * Real.pi)

Alias of Circle.exp_eq_exp.

@[deprecated Circle.periodic_exp]

theorem periodic_expMapCircle :

Function.Periodic (⇑Circle.exp) (2 * Real.pi)

Alias of Circle.periodic_exp.

@[deprecated Circle.exp_two_pi]

theorem expMapCircle_two_pi :

Circle.exp (2 * Real.pi) = 1

Alias of Circle.exp_two_pi.

@[deprecated Circle.exp_sub_two_pi]

theorem expMapCircle_sub_two_pi (x : ℝ) :

Circle.exp (x - 2 * Real.pi) = Circle.exp x

Alias of Circle.exp_sub_two_pi.

@[deprecated Circle.exp_add_two_pi]

theorem expMapCircle_add_two_pi (x : ℝ) :

Circle.exp (x + 2 * Real.pi) = Circle.exp x

Alias of Circle.exp_add_two_pi.

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

Circle.exp, applied to a Real.Angle.

Equations

θ.toCircle = Circle.periodic_exp.lift θ

Instances For

@[simp]

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

(↑x).toCircle = Circle.exp x

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

↑θ.toCircle = ↑θ.cos + ↑θ.sin * Complex.I

@[simp]

theorem Real.Angle.toCircle_zero :

Real.Angle.toCircle 0 = 1

@[simp]

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

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

@[simp]

theorem Real.Angle.toCircle_add (θ₁ θ₂ : Real.Angle) :

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

@[simp]

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

↑(↑θ.toCircle).arg = θ

@[deprecated Real.Angle.toCircle]

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

Alias of Real.Angle.toCircle.

Circle.exp, applied to a Real.Angle.

Equations

Real.Angle.expMapCircle = Real.Angle.toCircle

Instances For

@[deprecated Real.Angle.toCircle_coe]

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

(↑x).toCircle = Circle.exp x

Alias of Real.Angle.toCircle_coe.

@[deprecated Real.Angle.coe_toCircle]

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

↑θ.toCircle = ↑θ.cos + ↑θ.sin * Complex.I

Alias of Real.Angle.coe_toCircle.

@[deprecated Real.Angle.toCircle_zero]

theorem Real.Angle.expMapCircle_zero :

Real.Angle.toCircle 0 = 1

Alias of Real.Angle.toCircle_zero.

@[deprecated Real.Angle.toCircle_neg]

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

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

Alias of Real.Angle.toCircle_neg.

@[deprecated Real.Angle.toCircle_add]

theorem Real.Angle.expMapCircle_add (θ₁ θ₂ : Real.Angle) :

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

Alias of Real.Angle.toCircle_add.

@[deprecated Real.Angle.arg_toCircle]

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

↑(↑θ.toCircle).arg = θ

Alias of Real.Angle.arg_toCircle.

Map from `AddCircle` to `Circle` #

theorem AddCircle.scaled_exp_map_periodic {T : ℝ} :

Function.Periodic (fun (x : ℝ) => Circle.exp (2 * Real.pi / T * x)) T

noncomputable def AddCircle.toCircle {T : ℝ} :

AddCircle T → Circle

The canonical map fun x => exp (2 π i x / T) from ℝ / ℤ • T to the unit circle in ℂ. If T = 0 we understand this as the constant function 1.

Equations

AddCircle.toCircle = ⋯.lift

Instances For

theorem AddCircle.toCircle_apply_mk {T : ℝ} (x : ℝ) :

AddCircle.toCircle ↑x = Circle.exp (2 * Real.pi / T * x)

theorem AddCircle.toCircle_add {T : ℝ} (x y : AddCircle T) :

(x + y).toCircle = x.toCircle * y.toCircle

@[simp]

theorem AddCircle.toCircle_zero {T : ℝ} :

AddCircle.toCircle 0 = 1

theorem AddCircle.continuous_toCircle {T : ℝ} :

Continuous AddCircle.toCircle

theorem AddCircle.injective_toCircle {T : ℝ} (hT : T ≠ 0) :

Function.Injective AddCircle.toCircle

noncomputable def AddCircle.homeomorphCircle' :

AddCircle (2 * Real.pi) ≃ₜ Circle

The homeomorphism between AddCircle (2 * π) and Circle.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem AddCircle.homeomorphCircle'_symm_apply (x : Circle) :

AddCircle.homeomorphCircle'.symm x = ↑(↑x).arg

@[simp]

theorem AddCircle.homeomorphCircle'_apply (θ : Real.Angle) :

AddCircle.homeomorphCircle' θ = θ.toCircle

theorem AddCircle.homeomorphCircle'_apply_mk (x : ℝ) :

AddCircle.homeomorphCircle' ↑x = Circle.exp x

noncomputable def AddCircle.homeomorphCircle {T : ℝ} (hT : T ≠ 0) :

AddCircle T ≃ₜ Circle

The homeomorphism between AddCircle and Circle.

Equations

AddCircle.homeomorphCircle hT = (AddCircle.homeomorphAddCircle T (2 * Real.pi) hT AddCircle.homeomorphCircle.proof_2).trans AddCircle.homeomorphCircle'

Instances For

theorem AddCircle.homeomorphCircle_apply {T : ℝ} (hT : T ≠ 0) (x : AddCircle T) :

(AddCircle.homeomorphCircle hT) x = x.toCircle

theorem isLocalHomeomorph_circleExp :

IsLocalHomeomorph ⇑Circle.exp

@[deprecated isLocalHomeomorph_circleExp]

theorem isLocalHomeomorph_expMapCircle :

IsLocalHomeomorph ⇑Circle.exp

Alias of isLocalHomeomorph_circleExp.