Maps on the unit circle

In this file we prove some basic lemmas about Circle.exp 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

@[simp]

theorem Circle.arg_eq_zero {z : Circle} : (↑z).arg = 0 ↔ z = 1

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

@[simp]

theorem Circle.exp_arg (z : Circle) : exp (↑z).arg = z

noncomputable def Circle.argPartialEquiv : PartialEquiv Circle ℝ

Complex.arg ∘ (↑) and Circle.exp 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.argPartialEquiv_symm_apply : ↑argPartialEquiv.symm = ⇑exp

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def Circle.argEquiv : Circle ≃ ↑(Set.Ioc (-Real.pi) Real.pi)

Complex.arg and Circle.exp ∘ (↑) 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_3 }

@[simp]

theorem Circle.argEquiv_apply_coe (z : Circle) : ↑(argEquiv z) = (↑z).arg

@[simp]

theorem Circle.argEquiv_symm_apply : ⇑argEquiv.symm = ⇑exp ∘ Subtype.val

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

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

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

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

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

@[simp]

theorem Circle.exp_two_pi : exp (2 * Real.pi) = 1

theorem Circle.exp_int_mul_two_pi (n : ℤ) : exp (↑n * (2 * Real.pi)) = 1

theorem Circle.exp_two_pi_mul_int (n : ℤ) : exp (2 * Real.pi * ↑n) = 1

theorem Circle.exp_eq_one {r : ℝ} : exp r = 1 ↔ ∃ (n : ℤ), r = ↑n * (2 * Real.pi)

theorem Circle.exp_inj {r s : ℝ} : exp r = exp s ↔ r ≡ s [PMOD 2 * Real.pi]

theorem Circle.exp_sub_two_pi (x : ℝ) : exp (x - 2 * Real.pi) = exp x

theorem Circle.exp_add_two_pi (x : ℝ) : exp (x + 2 * Real.pi) = exp x

theorem Circle.exp_injOn_of_forall_sub_mem_Ioo {s : Set ℝ} (hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Set.Ioo (-2 * Real.pi) (2 * Real.pi)) : Set.InjOn (⇑exp) s

theorem Circle.exp_injOn_Icc {a b : ℝ} (h : b - a < 2 * Real.pi) : Set.InjOn (⇑exp) (Set.Icc a b)

theorem Circle.exp_injOn_Ico {a b : ℝ} (h : b - a ≤ 2 * Real.pi) : Set.InjOn (⇑exp) (Set.Ico a b)

theorem Circle.exp_injOn_Ioc {a b : ℝ} (h : b - a ≤ 2 * Real.pi) : Set.InjOn (⇑exp) (Set.Ioc a b)

def Circle.centeredArc (r : ℝ) : Set Circle

The image under Circle.exp of the interval of angles (-r, r).

Equations

• Circle.centeredArc r = ⇑Circle.exp '' {x : ℝ | |x| < r}

theorem Circle.bijOn_exp_Ioo_centeredArc {r : ℝ} (hr : r ≤ Real.pi) : Set.BijOn (⇑exp) (Set.Ioo (-r) r) (centeredArc r)

theorem Circle.centeredArc_mono {r s : ℝ} (h : r ≤ s) : centeredArc r ⊆ centeredArc s

theorem Circle.mem_centeredArc {r : ℝ} (hr : r ≤ Real.pi) {z : Circle} : z ∈ centeredArc r ↔ |(↑z).arg| < r

theorem Circle.centeredArc_eq_empty {r : ℝ} (hr : r ≤ 0) : centeredArc r = ∅

@[simp]

theorem Circle.centeredArc_zero : centeredArc 0 = ∅

theorem Circle.mem_centeredArc_div {z : Circle} {s : ℝ} {n : ℕ} (hs : s ≤ Real.pi) (h1 : z ∈ centeredArc (Real.pi / ↑n)) (h2 : z ^ n ∈ centeredArc s) : z ∈ centeredArc (s / ↑n)

theorem Circle.exp_surjective : Function.Surjective ⇑exp

instance Circle.instPathConnectedSpace : PathConnectedSpace Circle

noncomputable def Circle.angleDiff (x y : Circle) : ℝ

Length of the anti-clockwise arc from x to y.

Equations

• x.angleDiff y = if (↑x).arg ≤ (↑y).arg then (↑y).arg - (↑x).arg else 2 * Real.pi + (↑y).arg - (↑x).arg

@[simp]

theorem Circle.angleDiff_nonneg (x y : Circle) : 0 ≤ x.angleDiff y

theorem Circle.angleDiff_pos {x y : Circle} (h : x ≠ y) : 0 < x.angleDiff y

theorem Circle.angleDiff_lt_two_pi (x y : Circle) : x.angleDiff y < 2 * Real.pi

@[simp]

theorem Circle.angleDiff_add_angleDiff {x y : Circle} (h : x ≠ y) : x.angleDiff y + y.angleDiff x = 2 * Real.pi

@[simp]

theorem Circle.exp_angleDiff_mul {x y : Circle} : exp (x.angleDiff y) * x = y

theorem Circle.Icc_union_Icc_angleDiff_add_arg {x y : Circle} (h : x ≠ y) : Set.Icc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Set.Icc (↑y).arg (y.angleDiff x + (↑y).arg) = Set.Icc (min (↑x).arg (↑y).arg) (min (↑x).arg (↑y).arg + 2 * Real.pi)

theorem Circle.Ico_union_Ico_angleDiff_add_arg {x y : Circle} (h : x ≠ y) : Set.Ico (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Set.Ico (↑y).arg (y.angleDiff x + (↑y).arg) = Set.Ico (min (↑x).arg (↑y).arg) (min (↑x).arg (↑y).arg + 2 * Real.pi)

theorem Circle.Ioc_union_Ioc_angleDiff_add_arg {x y : Circle} (h : x ≠ y) : Set.Ioc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Set.Ioc (↑y).arg (y.angleDiff x + (↑y).arg) = Set.Ioc (min (↑x).arg (↑y).arg) (min (↑x).arg (↑y).arg + 2 * Real.pi)

noncomputable def Circle.path (x y : Circle) : Path x y

Path from x to y on the circle traversing in anti-clockwise direction.

Equations

• x.path y = ((Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)).map Circle.path._proof_5).cast ⋯ ⋯

@[simp]

theorem Circle.path_apply (x y : Circle) (a : ↑unitInterval) : (x.path y) a = exp ((Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)) a)

@[simp]

theorem Circle.coe_path (x y : Circle) : ⇑(x.path y) = ⇑exp ∘ ⇑(Path.segment (↑x).arg (x.angleDiff y + (↑x).arg))

@[simp]

theorem Circle.path_self (x : Circle) : x.path x = Path.refl x

theorem Circle.path_injective_of_ne {x y : Circle} (hne : x ≠ y) : Function.Injective ⇑(x.path y)

theorem Circle.range_path (x y : Circle) : Set.range ⇑(x.path y) = ⇑exp '' Set.Icc (↑x).arg (x.angleDiff y + (↑x).arg)

theorem Circle.path_image_Ico_of_ne {x y : Circle} (h : x ≠ y) : ⇑(x.path y) '' Set.Ico 0 1 = ⇑exp '' Set.Ico (↑x).arg (x.angleDiff y + (↑x).arg)

theorem Circle.path_image_Ioc_of_ne {x y : Circle} (h : x ≠ y) : ⇑(x.path y) '' Set.Ioc 0 1 = ⇑exp '' Set.Ioc (↑x).arg (x.angleDiff y + (↑x).arg)

theorem Circle.range_path_union_range_path {x y : Circle} (h : x ≠ y) : Set.range ⇑(x.path y) ∪ Set.range ⇑(y.path x) = Set.univ

theorem Circle.path_image_Ioc_union {x y : Circle} (h : x ≠ y) : ⇑(x.path y) '' Set.Ioc 0 1 ∪ ⇑(y.path x) '' Set.Ioc 0 1 = Set.univ

theorem Circle.disjoint_path_image_Ioc {x y : Circle} (h : x ≠ y) : Disjoint (⇑(x.path y) '' Set.Ioc 0 1) (⇑(y.path x) '' Set.Ioc 0 1)

theorem Circle.compl_path_image_Ioc {x y : Circle} (h : x ≠ y) : (⇑(x.path y) '' Set.Ioc 0 1)ᶜ = ⇑(y.path x) '' Set.Ioc 0 1

theorem Circle.compl_range_path {x y : Circle} (h : x ≠ y) : (Set.range ⇑(x.path y))ᶜ = ⇑(y.path x) '' Set.Ioo 0 1

theorem Circle.range_path_ssubset_univ (x y : Circle) : Set.range ⇑(x.path y) ⊂ Set.univ

theorem Circle.range_path_inter_range_path {x y : Circle} (h : x ≠ y) : Set.range ⇑(x.path y) ∩ Set.range ⇑(y.path x) = {x, y}

theorem Circle.isPathConnected_compl_singleton (x : Circle) : IsPathConnected {x}ᶜ

theorem Circle.not_isPreconnected_compl_pair {x y : Circle} (hxy : x ≠ y) : ¬IsPreconnected {x, y}ᶜ

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

Circle.exp, applied to a Real.Angle.

Equations

• θ.toCircle = Circle.periodic_exp.lift θ

@[simp]

theorem Real.Angle.toCircle_coe (x : ℝ) : (↑x).toCircle = Circle.exp x

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

@[simp]

theorem Real.Angle.toCircle_zero : toCircle 0 = 1

@[simp]

theorem Real.Angle.toCircle_neg (θ : Angle) : (-θ).toCircle = θ.toCircle⁻¹

@[simp]

theorem Real.Angle.toCircle_add (θ₁ θ₂ : Angle) : (θ₁ + θ₂).toCircle = θ₁.toCircle * θ₂.toCircle

@[simp]

theorem Real.Angle.arg_toCircle (θ : Angle) : ↑(↑θ.toCircle).arg = θ

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

theorem AddCircle.toCircle_apply_mk {T : ℝ} (x : ℝ) : 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 : ℝ} : toCircle 0 = 1

theorem AddCircle.toCircle_neg {T : ℝ} (x : AddCircle T) : (-x).toCircle = x.toCircle⁻¹

theorem AddCircle.toCircle_nsmul {T : ℝ} (x : AddCircle T) (n : ℕ) : (n • x).toCircle = x.toCircle ^ n

theorem AddCircle.toCircle_zsmul {T : ℝ} (x : AddCircle T) (n : ℤ) : (n • x).toCircle = x.toCircle ^ n

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

theorem AddCircle.injective_toCircle {T : ℝ} (hT : T ≠ 0) : Function.Injective 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.

@[simp]

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

@[simp]

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

theorem AddCircle.homeomorphCircle'_apply_mk (x : ℝ) : 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_1).trans AddCircle.homeomorphCircle'

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

theorem Circle.isAddQuotientCoveringMap_exp : IsAddQuotientCoveringMap ⇑exp ↥(AddSubgroup.zmultiples (2 * Real.pi))

theorem Circle.isCoveringMap_exp : IsCoveringMap ⇑exp

theorem isLocalHomeomorph_circleExp : IsLocalHomeomorph ⇑Circle.exp

theorem Circle.hasBasis_centeredArc_div_two_pow : (nhds 1).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => centeredArc (Real.pi / 2 ^ (n + 1))

The centered arcs centeredArc (π / 2 ^ (n + 1)) form a neighborhood basis at 1. This basis is useful because multiplying two sufficiently small arcs stays inside an earlier arc.

theorem Circle.isOpen_centeredArc (r : ℝ) : IsOpen (centeredArc r)

theorem Circle.eq_one_of_forall_pow_mem_centeredArc_pi_div_two {z : Circle} (hz : ∀ n > 0, z ^ n ∈ centeredArc (Real.pi / 2)) : z = 1

If all positive powers of a point on the circle lie in the right half centered arc, then the point is 1.

theorem Circle.isQuotientCoveringMap_zpow (n : ℤ) [NeZero n] : IsQuotientCoveringMap (fun (x : Circle) => x ^ n) ↥(zpowGroupHom n).ker

theorem Circle.isQuotientCoveringMap_npow (n : ℕ) [NeZero n] : IsQuotientCoveringMap (fun (x : Circle) => x ^ n) ↥(powMonoidHom n).ker