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 : ↥circle} {w : ↥circle} : (↑z).arg = (↑w).arg ↔ z = w

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

@[simp]

theorem expMapCircle_arg (z : ↥circle) : expMapCircle (↑z).arg = z

@[simp]

theorem circle.argPartialEquiv_apply : ↑circle.argPartialEquiv = Complex.arg ∘ Subtype.val

@[simp]

theorem circle.argPartialEquiv_source : circle.argPartialEquiv.source = Set.univ

@[simp]

theorem circle.argPartialEquiv_target : circle.argPartialEquiv.target = Set.Ioc (-Real.pi) Real.pi

@[simp]

theorem circle.argPartialEquiv_symm_apply : ↑circle.argPartialEquiv.symm = ⇑expMapCircle

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.

@[simp]

theorem circle.argEquiv_symm_apply : ⇑circle.argEquiv.symm = ⇑expMapCircle ∘ Subtype.val

@[simp]

theorem circle.argEquiv_apply_coe (z : ↥circle) : ↑(circle.argEquiv z) = (↑z).arg

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 := ⇑expMapCircle ∘ Subtype.val, left_inv := circle.argEquiv.proof_2, right_inv := circle.argEquiv.proof_3 }

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) : ↥circle

expMapCircle, applied to a Real.Angle.

Equations

• θ.expMapCircle = periodic_expMapCircle.lift θ

@[simp]

theorem Real.Angle.expMapCircle_coe (x : ℝ) : (↑x).expMapCircle = expMapCircle x

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

@[simp]

theorem Real.Angle.expMapCircle_zero : Real.Angle.expMapCircle 0 = 1

@[simp]

theorem Real.Angle.expMapCircle_neg (θ : Real.Angle) : (-θ).expMapCircle = θ.expMapCircle⁻¹

@[simp]

theorem Real.Angle.expMapCircle_add (θ₁ : Real.Angle) (θ₂ : Real.Angle) : (θ₁ + θ₂).expMapCircle = θ₁.expMapCircle * θ₂.expMapCircle

@[simp]

theorem Real.Angle.arg_expMapCircle (θ : Real.Angle) : ↑(↑θ.expMapCircle).arg = θ

Map from AddCircle to Circle

theorem AddCircle.scaled_exp_map_periodic {T : ℝ} : Function.Periodic (fun (x : ℝ) => expMapCircle (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

theorem AddCircle.toCircle_apply_mk {T : ℝ} (x : ℝ) : AddCircle.toCircle ↑x = expMapCircle (2 * Real.pi / T * x)

theorem AddCircle.toCircle_add {T : ℝ} (x : AddCircle T) (y : AddCircle T) : (x + y).toCircle = x.toCircle * y.toCircle

theorem AddCircle.continuous_toCircle {T : ℝ} : Continuous AddCircle.toCircle

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

@[simp]

theorem AddCircle.homeomorphCircle'_symm_apply (x : ↥circle) : AddCircle.homeomorphCircle'.symm x = ↑(↑x).arg

@[simp]

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

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.

theorem AddCircle.homeomorphCircle'_apply_mk (x : ℝ) : AddCircle.homeomorphCircle' ↑x = expMapCircle 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'

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

theorem isLocalHomeomorph_expMapCircle : IsLocalHomeomorph ⇑expMapCircle

Additive characters valued in the complex circle

noncomputable def ZMod.toCircle {N : ℕ} [NeZero N] : AddChar (ZMod N) ↥circle

The additive character from ZMod N to the unit circle in ℂ, sending j mod N to exp (2 * π * I * j / N).

Equations

• ZMod.toCircle = { toFun := fun (j : ZMod N) => AddCircle.toCircle (ZMod.toAddCircle j), map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }

theorem ZMod.toCircle_intCast {N : ℕ} [NeZero N] (j : ℤ) : ↑(ZMod.toCircle ↑j) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑j / ↑N)

theorem ZMod.toCircle_natCast {N : ℕ} [NeZero N] (j : ℕ) : ↑(ZMod.toCircle ↑j) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑j / ↑N)

theorem ZMod.toCircle_apply {N : ℕ} [NeZero N] (j : ZMod N) : ↑(ZMod.toCircle j) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑j.val / ↑N)

Explicit formula for toCircle j. Note that this is "evil" because it uses ZMod.val. Where possible, it is recommended to lift j to ℤ and use toCircle_intCast instead.

noncomputable def ZMod.stdAddChar {N : ℕ} [NeZero N] : AddChar (ZMod N) ℂ

The additive character from ZMod N to ℂ, sending j mod N to exp (2 * π * I * j / N).

Equations

• ZMod.stdAddChar = circle.subtype.compAddChar ZMod.toCircle

theorem ZMod.stdAddChar_coe {N : ℕ} [NeZero N] (j : ℤ) : ZMod.stdAddChar ↑j = Complex.exp (2 * ↑Real.pi * Complex.I * ↑j / ↑N)

theorem ZMod.stdAddChar_apply {N : ℕ} [NeZero N] (j : ZMod N) : ZMod.stdAddChar j = ↑(ZMod.toCircle j)