From 5473b3a2bfc0ab231999909b6add1eee4d559967 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Tue, 12 Mar 2024 10:05:39 -0700 Subject: [PATCH 01/16] results --- .../SpecialFunctions/Complex/Circle.lean | 39 +++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean index 687fe7258d91e..5bc20d7db7134 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean @@ -5,6 +5,7 @@ Authors: Yury G. Kudryashov -/ import Mathlib.Analysis.Complex.Circle import Mathlib.Analysis.SpecialFunctions.Complex.Log +import Mathlib.Topology.IsLocalHomeomorph #align_import analysis.special_functions.complex.circle from "leanprover-community/mathlib"@"f333194f5ecd1482191452c5ea60b37d4d6afa08" @@ -68,6 +69,29 @@ noncomputable def argEquiv : circle ≃ Ioc (-π) π where right_inv x := Subtype.ext <| argPartialEquiv.right_inv x.2 #align circle.arg_equiv circle.argEquiv +/-- `Complex.arg ∘ (↑)` and `expMapCircle` define a partial equivalence between `circle` and `ℝ` +with `source = Set.univ` and `target = Set.Ioo (-π) π`. -/ +@[simps (config := .asFn)] +noncomputable def argPartialHomeomorph : PartialHomeomorph circle ℝ := + let fund : ∀ x : circle, Complex.arg x = Real.pi ↔ x = expMapCircle Real.pi := + fun x ↦ ⟨fun hx ↦ hx ▸ (expMapCircle_arg x).symm, + fun hx ↦ hx ▸ arg_expMapCircle (neg_lt_self pi_pos) le_rfl⟩ + { toFun := arg ∘ (↑) + invFun := expMapCircle + source := {expMapCircle π}ᶜ + target := Set.Ioo (-π) π + map_source' := fun x hx ↦ let h := arg_mem_Ioc x; ⟨h.1, lt_of_le_of_ne h.2 (hx ∘ (fund x).mp)⟩ + map_target' := fun x hx hx' ↦ hx.2.ne + (by rwa [mem_singleton_iff, ← fund, arg_expMapCircle hx.1 hx.2.le] at hx') + left_inv' := fun x _ ↦ expMapCircle_arg x + right_inv' := fun x hx ↦ arg_expMapCircle hx.1 hx.2.le + open_source := isOpen_compl_singleton + open_target := isOpen_Ioo + continuousOn_toFun := (ContinuousAt.continuousOn fun _ ↦ continuousAt_arg).comp + continuous_induced_dom.continuousOn + (fun x h ↦ mem_slitPlane_iff_arg.mpr ⟨mt (fund x).mp h, ne_zero_of_mem_circle x⟩) + continuousOn_invFun := Continuous.continuousOn (by continuity) } + end circle theorem leftInverse_expMapCircle_arg : LeftInverse expMapCircle (arg ∘ (↑)) := @@ -150,3 +174,18 @@ theorem Real.Angle.arg_expMapCircle (θ : Real.Angle) : rw [Real.Angle.expMapCircle_coe, expMapCircle_apply, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ← Real.Angle.cos_coe, ← Real.Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle] #align real.angle.arg_exp_map_circle Real.Angle.arg_expMapCircle + +-- todo: upgrade this to `IsCoveringMap expMapCircle`. +lemma isLocalHomeomorph_expMapCircle : IsLocalHomeomorph expMapCircle := by + intro t + let e1 : PartialHomeomorph ℝ circle := circle.argPartialHomeomorph.symm + let e2 : PartialHomeomorph ℝ ℝ := ((Homeomorph.addRight t).toPartialHomeomorphOfImageEq + (Ioo (-π) π) (isOpen_Ioo) (Ioo (-π + t) (π + t)) (image_add_const_Ioo t (-π) π)).symm + let e3 : PartialHomeomorph circle circle := + (Homeomorph.mulRight (expMapCircle t)).toPartialHomeomorphOfImageEq + {expMapCircle Real.pi}ᶜ isOpen_compl_singleton {expMapCircle (Real.pi + t)}ᶜ + (by rw [image_compl_eq (Homeomorph.mulRight (expMapCircle t)).bijective, + image_singleton, Homeomorph.coe_mulRight, expMapCircle_add]) + let e4 : PartialHomeomorph ℝ circle := e2.trans' (e1.trans' e3 rfl) rfl + exact ⟨e4, ⟨add_lt_of_neg_left t (neg_neg_of_pos pi_pos), lt_add_of_pos_left t pi_pos⟩, + funext fun x ↦ (congrArg _ (sub_add_cancel x t).symm).trans (expMapCircle_add (x - t) t)⟩ From eb084ff803bd78b9feb1be009845c47646fc6788 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Tue, 12 Mar 2024 12:27:03 -0700 Subject: [PATCH 02/16] cleanup --- .../SpecialFunctions/Complex/Circle.lean | 27 ++++++++++--------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean index 5bc20d7db7134..adf86d0b0706c 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean @@ -46,6 +46,9 @@ theorem expMapCircle_arg (z : circle) : expMapCircle (arg z) = z := namespace circle +theorem arg_eq_pi_iff {z : circle} : arg z = π ↔ z = expMapCircle π := + ⟨fun h ↦ h ▸ (expMapCircle_arg z).symm, fun h ↦ h ▸ arg_expMapCircle (neg_lt_self pi_pos) le_rfl⟩ + /-- `Complex.arg ∘ (↑)` and `expMapCircle` define a partial equivalence between `circle` and `ℝ` with `source = Set.univ` and `target = Set.Ioc (-π) π`. -/ @[simps (config := .asFn)] @@ -73,23 +76,21 @@ noncomputable def argEquiv : circle ≃ Ioc (-π) π where with `source = Set.univ` and `target = Set.Ioo (-π) π`. -/ @[simps (config := .asFn)] noncomputable def argPartialHomeomorph : PartialHomeomorph circle ℝ := - let fund : ∀ x : circle, Complex.arg x = Real.pi ↔ x = expMapCircle Real.pi := - fun x ↦ ⟨fun hx ↦ hx ▸ (expMapCircle_arg x).symm, - fun hx ↦ hx ▸ arg_expMapCircle (neg_lt_self pi_pos) le_rfl⟩ { toFun := arg ∘ (↑) invFun := expMapCircle source := {expMapCircle π}ᶜ target := Set.Ioo (-π) π - map_source' := fun x hx ↦ let h := arg_mem_Ioc x; ⟨h.1, lt_of_le_of_ne h.2 (hx ∘ (fund x).mp)⟩ - map_target' := fun x hx hx' ↦ hx.2.ne - (by rwa [mem_singleton_iff, ← fund, arg_expMapCircle hx.1 hx.2.le] at hx') + map_source' := + fun x h ↦ let h' := arg_mem_Ioc x; ⟨h'.1, lt_of_le_of_ne h'.2 (h ∘ arg_eq_pi_iff.mp)⟩ + map_target' := + fun x h h' ↦ h.2.ne ((arg_expMapCircle h.1 h.2.le).symm.trans (arg_eq_pi_iff.mpr h')) left_inv' := fun x _ ↦ expMapCircle_arg x right_inv' := fun x hx ↦ arg_expMapCircle hx.1 hx.2.le open_source := isOpen_compl_singleton open_target := isOpen_Ioo - continuousOn_toFun := (ContinuousAt.continuousOn fun _ ↦ continuousAt_arg).comp - continuous_induced_dom.continuousOn - (fun x h ↦ mem_slitPlane_iff_arg.mpr ⟨mt (fund x).mp h, ne_zero_of_mem_circle x⟩) + continuousOn_toFun := ContinuousAt.continuousOn fun x h ↦ (continuousAt_arg + (mem_slitPlane_iff_arg.mpr ⟨mt arg_eq_pi_iff.mp h, ne_zero_of_mem_circle x⟩)).comp + continuousAt_subtype_val continuousOn_invFun := Continuous.continuousOn (by continuity) } end circle @@ -180,12 +181,12 @@ lemma isLocalHomeomorph_expMapCircle : IsLocalHomeomorph expMapCircle := by intro t let e1 : PartialHomeomorph ℝ circle := circle.argPartialHomeomorph.symm let e2 : PartialHomeomorph ℝ ℝ := ((Homeomorph.addRight t).toPartialHomeomorphOfImageEq - (Ioo (-π) π) (isOpen_Ioo) (Ioo (-π + t) (π + t)) (image_add_const_Ioo t (-π) π)).symm + (Ioo (-π) π) isOpen_Ioo (Ioo (-π + t) (π + t)) (image_add_const_Ioo t (-π) π)).symm let e3 : PartialHomeomorph circle circle := (Homeomorph.mulRight (expMapCircle t)).toPartialHomeomorphOfImageEq - {expMapCircle Real.pi}ᶜ isOpen_compl_singleton {expMapCircle (Real.pi + t)}ᶜ - (by rw [image_compl_eq (Homeomorph.mulRight (expMapCircle t)).bijective, - image_singleton, Homeomorph.coe_mulRight, expMapCircle_add]) + {expMapCircle π}ᶜ isOpen_compl_singleton {expMapCircle (π + t)}ᶜ + (by rw [image_compl_eq (Homeomorph.bijective _), image_singleton, + Homeomorph.coe_mulRight, expMapCircle_add]) let e4 : PartialHomeomorph ℝ circle := e2.trans' (e1.trans' e3 rfl) rfl exact ⟨e4, ⟨add_lt_of_neg_left t (neg_neg_of_pos pi_pos), lt_add_of_pos_left t pi_pos⟩, funext fun x ↦ (congrArg _ (sub_add_cancel x t).symm).trans (expMapCircle_add (x - t) t)⟩ From 3461eeb7ac5fc7db4eb68600279b61f19e354eff Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Sat, 6 Apr 2024 18:58:21 -0700 Subject: [PATCH 03/16] temp --- Mathlib/Analysis/Fourier/AddCircle.lean | 41 ------- .../SpecialFunctions/Complex/Circle.lean | 108 ++++++++++++------ Mathlib/Topology/Instances/AddCircle.lean | 30 +++++ 3 files changed, 105 insertions(+), 74 deletions(-) diff --git a/Mathlib/Analysis/Fourier/AddCircle.lean b/Mathlib/Analysis/Fourier/AddCircle.lean index 3cd0850d72495..7f419b527511a 100644 --- a/Mathlib/Analysis/Fourier/AddCircle.lean +++ b/Mathlib/Analysis/Fourier/AddCircle.lean @@ -71,47 +71,6 @@ variable {T : ℝ} namespace AddCircle -/-! ### Map from `AddCircle` to `Circle` -/ - - -theorem scaled_exp_map_periodic : Function.Periodic (fun x => expMapCircle (2 * π / T * x)) T := by - -- The case T = 0 is not interesting, but it is true, so we prove it to save hypotheses - rcases eq_or_ne T 0 with (rfl | hT) - · intro x; simp - · intro x; simp_rw [mul_add]; rw [div_mul_cancel _ hT, periodic_expMapCircle] -#align add_circle.scaled_exp_map_periodic AddCircle.scaled_exp_map_periodic - -/-- 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. -/ -def toCircle : AddCircle T → circle := - (@scaled_exp_map_periodic T).lift -#align add_circle.to_circle AddCircle.toCircle - -theorem toCircle_add (x : AddCircle T) (y : AddCircle T) : - @toCircle T (x + y) = toCircle x * toCircle y := by - induction x using QuotientAddGroup.induction_on' - induction y using QuotientAddGroup.induction_on' - rw [← QuotientAddGroup.mk_add] - simp_rw [toCircle, Function.Periodic.lift_coe, mul_add, expMapCircle_add] -#align add_circle.to_circle_add AddCircle.toCircle_add - -theorem continuous_toCircle : Continuous (@toCircle T) := - continuous_coinduced_dom.mpr (expMapCircle.continuous.comp <| continuous_const.mul continuous_id') -#align add_circle.continuous_to_circle AddCircle.continuous_toCircle - -theorem injective_toCircle (hT : T ≠ 0) : Function.Injective (@toCircle T) := by - intro a b h - induction a using QuotientAddGroup.induction_on' - induction b using QuotientAddGroup.induction_on' - simp_rw [toCircle, Function.Periodic.lift_coe] at h - obtain ⟨m, hm⟩ := expMapCircle_eq_expMapCircle.mp h.symm - rw [QuotientAddGroup.eq]; simp_rw [AddSubgroup.mem_zmultiples_iff, zsmul_eq_mul] - use m - field_simp at hm - rw [← mul_right_inj' Real.two_pi_pos.ne'] - linarith -#align add_circle.injective_to_circle AddCircle.injective_toCircle - /-! ### Measure on `AddCircle T` In this file we use the Haar measure on `AddCircle T` normalised to have total measure 1 (which is diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean index adf86d0b0706c..6428fe1eb2c92 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean @@ -5,6 +5,7 @@ Authors: Yury G. Kudryashov -/ import Mathlib.Analysis.Complex.Circle import Mathlib.Analysis.SpecialFunctions.Complex.Log +import Mathlib.Topology.Instances.AddCircle import Mathlib.Topology.IsLocalHomeomorph #align_import analysis.special_functions.complex.circle from "leanprover-community/mathlib"@"f333194f5ecd1482191452c5ea60b37d4d6afa08" @@ -72,27 +73,6 @@ noncomputable def argEquiv : circle ≃ Ioc (-π) π where right_inv x := Subtype.ext <| argPartialEquiv.right_inv x.2 #align circle.arg_equiv circle.argEquiv -/-- `Complex.arg ∘ (↑)` and `expMapCircle` define a partial equivalence between `circle` and `ℝ` -with `source = Set.univ` and `target = Set.Ioo (-π) π`. -/ -@[simps (config := .asFn)] -noncomputable def argPartialHomeomorph : PartialHomeomorph circle ℝ := - { toFun := arg ∘ (↑) - invFun := expMapCircle - source := {expMapCircle π}ᶜ - target := Set.Ioo (-π) π - map_source' := - fun x h ↦ let h' := arg_mem_Ioc x; ⟨h'.1, lt_of_le_of_ne h'.2 (h ∘ arg_eq_pi_iff.mp)⟩ - map_target' := - fun x h h' ↦ h.2.ne ((arg_expMapCircle h.1 h.2.le).symm.trans (arg_eq_pi_iff.mpr h')) - left_inv' := fun x _ ↦ expMapCircle_arg x - right_inv' := fun x hx ↦ arg_expMapCircle hx.1 hx.2.le - open_source := isOpen_compl_singleton - open_target := isOpen_Ioo - continuousOn_toFun := ContinuousAt.continuousOn fun x h ↦ (continuousAt_arg - (mem_slitPlane_iff_arg.mpr ⟨mt arg_eq_pi_iff.mp h, ne_zero_of_mem_circle x⟩)).comp - continuousAt_subtype_val - continuousOn_invFun := Continuous.continuousOn (by continuity) } - end circle theorem leftInverse_expMapCircle_arg : LeftInverse expMapCircle (arg ∘ (↑)) := @@ -176,17 +156,79 @@ theorem Real.Angle.arg_expMapCircle (θ : Real.Angle) : Real.Angle.cos_coe, ← Real.Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle] #align real.angle.arg_exp_map_circle Real.Angle.arg_expMapCircle +namespace AddCircle + +variable {T : ℝ} + +/-! ### Map from `AddCircle` to `Circle` -/ + +theorem scaled_exp_map_periodic : Function.Periodic (fun x => expMapCircle (2 * π / T * x)) T := by + -- The case T = 0 is not interesting, but it is true, so we prove it to save hypotheses + rcases eq_or_ne T 0 with (rfl | hT) + · intro x; simp + · intro x; simp_rw [mul_add]; rw [div_mul_cancel _ hT, periodic_expMapCircle] +#align add_circle.scaled_exp_map_periodic AddCircle.scaled_exp_map_periodic + +/-- 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. -/ +noncomputable def toCircle : AddCircle T → circle := + (@scaled_exp_map_periodic T).lift +#align add_circle.to_circle AddCircle.toCircle + +/-- 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. -/ +noncomputable def toCircleHomeomorph : AddCircle T ≃ₜ circle := + { toFun := (@scaled_exp_map_periodic T).lift + invFun := fun x ↦ (2 * π / T)⁻¹ * Complex.arg x + left_inv := by + intro x + simp only + have key : ∃ y : ℝ, x = y := sorry + change ↑((2 * π / T)⁻¹ * arg ↑(_)) = x + change ↑((2 * π / T)⁻¹ * arg ↑(expMapCircle (2 * π / T * x))) = x + change ↑((_ : ℝ) * (_ : ℝ)) = _ + right_inv := sorry + continuous_toFun := sorry + continuous_invFun := sorry } + +theorem toCircle_add (x : AddCircle T) (y : AddCircle T) : + @toCircle T (x + y) = toCircle x * toCircle y := by + induction x using QuotientAddGroup.induction_on' + induction y using QuotientAddGroup.induction_on' + rw [← QuotientAddGroup.mk_add] + simp_rw [toCircle, Function.Periodic.lift_coe, mul_add, expMapCircle_add] +#align add_circle.to_circle_add AddCircle.toCircle_add + +theorem continuous_toCircle : Continuous (@toCircle T) := + continuous_coinduced_dom.mpr (expMapCircle.continuous.comp <| continuous_const.mul continuous_id') +#align add_circle.continuous_to_circle AddCircle.continuous_toCircle + +theorem injective_toCircle (hT : T ≠ 0) : Function.Injective (@toCircle T) := by + intro a b h + induction a using QuotientAddGroup.induction_on' + induction b using QuotientAddGroup.induction_on' + simp_rw [toCircle, Function.Periodic.lift_coe] at h + obtain ⟨m, hm⟩ := expMapCircle_eq_expMapCircle.mp h.symm + rw [QuotientAddGroup.eq]; simp_rw [AddSubgroup.mem_zmultiples_iff, zsmul_eq_mul] + use m + field_simp at hm + rw [← mul_right_inj' Real.two_pi_pos.ne'] + linarith +#align add_circle.injective_to_circle AddCircle.injective_toCircle + +end AddCircle + -- todo: upgrade this to `IsCoveringMap expMapCircle`. lemma isLocalHomeomorph_expMapCircle : IsLocalHomeomorph expMapCircle := by - intro t - let e1 : PartialHomeomorph ℝ circle := circle.argPartialHomeomorph.symm - let e2 : PartialHomeomorph ℝ ℝ := ((Homeomorph.addRight t).toPartialHomeomorphOfImageEq - (Ioo (-π) π) isOpen_Ioo (Ioo (-π + t) (π + t)) (image_add_const_Ioo t (-π) π)).symm - let e3 : PartialHomeomorph circle circle := - (Homeomorph.mulRight (expMapCircle t)).toPartialHomeomorphOfImageEq - {expMapCircle π}ᶜ isOpen_compl_singleton {expMapCircle (π + t)}ᶜ - (by rw [image_compl_eq (Homeomorph.bijective _), image_singleton, - Homeomorph.coe_mulRight, expMapCircle_add]) - let e4 : PartialHomeomorph ℝ circle := e2.trans' (e1.trans' e3 rfl) rfl - exact ⟨e4, ⟨add_lt_of_neg_left t (neg_neg_of_pos pi_pos), lt_add_of_pos_left t pi_pos⟩, - funext fun x ↦ (congrArg _ (sub_add_cancel x t).symm).trans (expMapCircle_add (x - t) t)⟩ + let T : ℝ := 1 + have : Fact (0 < T) := ⟨one_pos⟩ + have key : expMapCircle = AddCircle.toCircle (T := T) ∘ ((↑) : ℝ → AddCircle T) ∘ (fun x ↦ (2 * π / T)⁻¹ * x) := by + ext x + congr + exact (mul_inv_cancel_left₀ (by positivity) x).symm + rw [key] + refine' IsLocalHomeomorph.comp _ (IsLocalHomeomorph.comp (AddCircle.isLocalHomeomorph_coe T) + (Homeomorph.mulLeft₀ ((2 * π / T)⁻¹) (by positivity)).isLocalHomeomorph) + + sorry + -- have key := AddCircle.IsLocalHomeomorph_coe diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean index edf005871afb3..f3c8aa1a45345 100644 --- a/Mathlib/Topology/Instances/AddCircle.lean +++ b/Mathlib/Topology/Instances/AddCircle.lean @@ -11,6 +11,7 @@ import Mathlib.Algebra.Order.Floor import Mathlib.Algebra.Order.ToIntervalMod import Mathlib.Topology.Instances.Real import Mathlib.Topology.Connected.PathConnected +import Mathlib.Topology.Covering #align_import topology.instances.add_circle from "leanprover-community/mathlib"@"213b0cff7bc5ab6696ee07cceec80829ce42efec" @@ -267,6 +268,35 @@ theorem continuousAt_equivIoc : ContinuousAt (equivIoc p a) x := by exact (continuousAt_toIocMod hp.out a hx).codRestrict _ #align add_circle.continuous_at_equiv_Ioc AddCircle.continuousAt_equivIoc +def partialHomeomorphCoe [DiscreteTopology (zmultiples p)] : PartialHomeomorph 𝕜 (AddCircle p) := + { toFun := (↑) + invFun := fun x ↦ equivIco p a x + source := Ioo a (a + p) + target := {↑a}ᶜ + map_source' := by + intro x hx hx' + exact hx.1.ne' ((coe_eq_coe_iff_of_mem_Ico (Ioo_subset_Ico_self hx) + (left_mem_Ico.mpr (lt_add_of_pos_right a hp.out))).mp hx') + map_target' := by + intro x hx + exact (eq_left_or_mem_Ioo_of_mem_Ico (equivIco p a x).2).resolve_left + (hx ∘ ((equivIco p a).symm_apply_apply x).symm.trans ∘ congrArg _) + left_inv' := + fun x hx ↦ congrArg _ ((equivIco p a).apply_symm_apply ⟨x, Ioo_subset_Ico_self hx⟩) + right_inv' := fun x _ ↦ (equivIco p a).symm_apply_apply x + open_source := isOpen_Ioo + open_target := isOpen_compl_singleton + continuousOn_toFun := (AddCircle.continuous_mk' p).continuousOn + continuousOn_invFun := by + exact ContinuousAt.continuousOn + (fun _ ↦ continuousAt_subtype_val.comp ∘ continuousAt_equivIco p a) } + +lemma isLocalHomeomorph_coe [DiscreteTopology (zmultiples p)] [DenselyOrdered 𝕜] : + IsLocalHomeomorph ((↑) : 𝕜 → AddCircle p) := by + intro a + obtain ⟨b, hb⟩ := nonempty_Ioo_subtype (sub_lt_self a hp.out) + exact ⟨partialHomeomorphCoe p b, ⟨hb.2, lt_add_of_sub_right_lt hb.1⟩, rfl⟩ + end Continuity /-- The image of the closed-open interval `[a, a + p)` under the quotient map `𝕜 → AddCircle p` is From 4645a8e77e1450e0a3c3a064fd3c57273fb05916 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Mon, 8 Apr 2024 14:50:04 -0700 Subject: [PATCH 04/16] proved --- .../SpecialFunctions/Complex/Circle.lean | 66 +++++++++++-------- Mathlib/Topology/Instances/AddCircle.lean | 6 ++ 2 files changed, 45 insertions(+), 27 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean index 1b4e6f6a264e2..901c55a5d12db 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean @@ -175,21 +175,8 @@ noncomputable def toCircle : AddCircle T → circle := (@scaled_exp_map_periodic T).lift #align add_circle.to_circle AddCircle.toCircle -/-- 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. -/ -noncomputable def toCircleHomeomorph : AddCircle T ≃ₜ circle := - { toFun := (@scaled_exp_map_periodic T).lift - invFun := fun x ↦ (2 * π / T)⁻¹ * Complex.arg x - left_inv := by - intro x - simp only - have key : ∃ y : ℝ, x = y := sorry - change ↑((2 * π / T)⁻¹ * arg ↑(_)) = x - change ↑((2 * π / T)⁻¹ * arg ↑(expMapCircle (2 * π / T * x))) = x - change ↑((_ : ℝ) * (_ : ℝ)) = _ - right_inv := sorry - continuous_toFun := sorry - continuous_invFun := sorry } +@[simp] +theorem toCircle_coe (x : ℝ) : @toCircle T x = expMapCircle (2 * π / T * x) := rfl theorem toCircle_add (x : AddCircle T) (y : AddCircle T) : @toCircle T (x + y) = toCircle x * toCircle y := by @@ -216,19 +203,44 @@ theorem injective_toCircle (hT : T ≠ 0) : Function.Injective (@toCircle T) := linarith #align add_circle.injective_to_circle AddCircle.injective_toCircle +private noncomputable def homeomorphCircle' : AddCircle (2 * π) ≃ₜ circle := + { toFun := Real.Angle.expMapCircle + invFun := fun x ↦ arg x + left_inv := Real.Angle.arg_expMapCircle + right_inv := expMapCircle_arg + continuous_toFun := continuous_coinduced_dom.mpr expMapCircle.continuous + continuous_invFun := by + let f : circle → Real.Angle := fun x ↦ arg x + change Continuous f + have hf : ∀ x y, f (x * y) = f x + f y := by + intro x y + conv_lhs => rw [← expMapCircle_arg x, ← expMapCircle_arg y, ← expMapCircle_add] + exact Real.Angle.arg_expMapCircle (arg x + arg y) + rw [continuous_iff_continuousAt] + intro x + have hg : f = (fun y ↦ y - f x⁻¹) ∘ f ∘ (fun y ↦ y * x⁻¹) := by + ext y + rw [comp_apply, comp_apply, hf, add_sub_cancel_right] + rw [hg] + exact (continuous_sub_right (f x⁻¹)).continuousAt.comp + (((continuousAt_arg_coe_angle (ne_zero_of_mem_circle _)).comp + (continuousAt_subtype_val)).comp + (continuous_mul_right x⁻¹).continuousAt) } + +noncomputable def homeomorphCircle (hT : T ≠ 0) : AddCircle T ≃ₜ circle := + (homeomorphAddCircle T (2 * π) hT (by positivity)).trans homeomorphCircle' + +theorem homeomorphCircle_apply (hT : T ≠ 0) (x : AddCircle T) : + homeomorphCircle hT x = toCircle x := by + induction' x using QuotientAddGroup.induction_on' with x + change expMapCircle _ = expMapCircle _ + congr; simp; ring + end AddCircle +open AddCircle + -- todo: upgrade this to `IsCoveringMap expMapCircle`. lemma isLocalHomeomorph_expMapCircle : IsLocalHomeomorph expMapCircle := by - let T : ℝ := 1 - have : Fact (0 < T) := ⟨one_pos⟩ - have key : expMapCircle = AddCircle.toCircle (T := T) ∘ ((↑) : ℝ → AddCircle T) ∘ (fun x ↦ (2 * π / T)⁻¹ * x) := by - ext x - congr - exact (mul_inv_cancel_left₀ (by positivity) x).symm - rw [key] - refine' IsLocalHomeomorph.comp _ (IsLocalHomeomorph.comp (AddCircle.isLocalHomeomorph_coe T) - (Homeomorph.mulLeft₀ ((2 * π / T)⁻¹) (by positivity)).isLocalHomeomorph) - - sorry - -- have key := AddCircle.IsLocalHomeomorph_coe + have : Fact (0 < 2 * π) := ⟨by positivity⟩ + exact homeomorphCircle'.isLocalHomeomorph.comp (isLocalHomeomorph_coe (2 * π)) diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean index 6e2ba68aaf416..8f15fad9e41cd 100644 --- a/Mathlib/Topology/Instances/AddCircle.lean +++ b/Mathlib/Topology/Instances/AddCircle.lean @@ -347,6 +347,12 @@ theorem equivAddCircle_symm_apply_mk (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) : rfl #align add_circle.equiv_add_circle_symm_apply_mk AddCircle.equivAddCircle_symm_apply_mk +/-- The rescaling equivalence between additive circles with different periods. -/ +def homeomorphAddCircle (hp : p ≠ 0) (hq : q ≠ 0) : AddCircle p ≃ₜ AddCircle q := + ⟨equivAddCircle p q hp hq, + (continuous_quotient_mk'.comp (continuous_mul_right (p⁻¹ * q))).quotient_lift _, + (continuous_quotient_mk'.comp (continuous_mul_right (q⁻¹ * p))).quotient_lift _⟩ + variable [hp : Fact (0 < p)] section FloorRing From c21c5482b6380704906cdfc4e7e2807c1b50cfc0 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Mon, 8 Apr 2024 14:52:17 -0700 Subject: [PATCH 05/16] cleanup --- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean | 6 ------ 1 file changed, 6 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean index 901c55a5d12db..ff8a9ed367dd8 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean @@ -47,9 +47,6 @@ theorem expMapCircle_arg (z : circle) : expMapCircle (arg z) = z := namespace circle -theorem arg_eq_pi_iff {z : circle} : arg z = π ↔ z = expMapCircle π := - ⟨fun h ↦ h ▸ (expMapCircle_arg z).symm, fun h ↦ h ▸ arg_expMapCircle (neg_lt_self pi_pos) le_rfl⟩ - /-- `Complex.arg ∘ (↑)` and `expMapCircle` define a partial equivalence between `circle` and `ℝ` with `source = Set.univ` and `target = Set.Ioc (-π) π`. -/ @[simps (config := .asFn)] @@ -175,9 +172,6 @@ noncomputable def toCircle : AddCircle T → circle := (@scaled_exp_map_periodic T).lift #align add_circle.to_circle AddCircle.toCircle -@[simp] -theorem toCircle_coe (x : ℝ) : @toCircle T x = expMapCircle (2 * π / T * x) := rfl - theorem toCircle_add (x : AddCircle T) (y : AddCircle T) : @toCircle T (x + y) = toCircle x * toCircle y := by induction x using QuotientAddGroup.induction_on' From 84519cf803fc4cfc9d70a529f62905fe0ddfd4fc Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Mon, 8 Apr 2024 14:53:24 -0700 Subject: [PATCH 06/16] fix imports --- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean | 1 - Mathlib/Topology/Instances/AddCircle.lean | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean index ff8a9ed367dd8..5951ae901c995 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean @@ -6,7 +6,6 @@ Authors: Yury G. Kudryashov import Mathlib.Analysis.Complex.Circle import Mathlib.Analysis.SpecialFunctions.Complex.Log import Mathlib.Topology.Instances.AddCircle -import Mathlib.Topology.IsLocalHomeomorph #align_import analysis.special_functions.complex.circle from "leanprover-community/mathlib"@"f333194f5ecd1482191452c5ea60b37d4d6afa08" diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean index 8f15fad9e41cd..e40d10f82f016 100644 --- a/Mathlib/Topology/Instances/AddCircle.lean +++ b/Mathlib/Topology/Instances/AddCircle.lean @@ -11,7 +11,7 @@ import Mathlib.Algebra.Order.Floor import Mathlib.Algebra.Order.ToIntervalMod import Mathlib.Topology.Instances.Real import Mathlib.Topology.Connected.PathConnected -import Mathlib.Topology.Covering +import Mathlib.Topology.IsLocalHomeomorph #align_import topology.instances.add_circle from "leanprover-community/mathlib"@"213b0cff7bc5ab6696ee07cceec80829ce42efec" From bf19c1417c8429d00b89e5d80b128dfae383088d Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Mon, 8 Apr 2024 14:53:44 -0700 Subject: [PATCH 07/16] fix imports --- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean index 5951ae901c995..dfff8724bbadc 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean @@ -5,7 +5,6 @@ Authors: Yury G. Kudryashov -/ import Mathlib.Analysis.Complex.Circle import Mathlib.Analysis.SpecialFunctions.Complex.Log -import Mathlib.Topology.Instances.AddCircle #align_import analysis.special_functions.complex.circle from "leanprover-community/mathlib"@"f333194f5ecd1482191452c5ea60b37d4d6afa08" From ef643ae953cb4876a1730d5191fadbaefd7bbe99 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Mon, 8 Apr 2024 21:55:11 -0700 Subject: [PATCH 08/16] lint --- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean | 1 + Mathlib/Topology/Instances/AddCircle.lean | 1 + 2 files changed, 2 insertions(+) diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean index dfff8724bbadc..b1a70ac15d98d 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean @@ -219,6 +219,7 @@ private noncomputable def homeomorphCircle' : AddCircle (2 * π) ≃ₜ circle : (continuousAt_subtype_val)).comp (continuous_mul_right x⁻¹).continuousAt) } +/-- The homeomorphism between `AddCircle` and `circle`. -/ noncomputable def homeomorphCircle (hT : T ≠ 0) : AddCircle T ≃ₜ circle := (homeomorphAddCircle T (2 * π) hT (by positivity)).trans homeomorphCircle' diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean index e40d10f82f016..baee67a2d9e50 100644 --- a/Mathlib/Topology/Instances/AddCircle.lean +++ b/Mathlib/Topology/Instances/AddCircle.lean @@ -268,6 +268,7 @@ theorem continuousAt_equivIoc : ContinuousAt (equivIoc p a) x := by exact (continuousAt_toIocMod hp.out a hx).codRestrict _ #align add_circle.continuous_at_equiv_Ioc AddCircle.continuousAt_equivIoc +/-- The quotient map `𝕜 → AddCircle p` as a partial homeomorphism. -/ def partialHomeomorphCoe [DiscreteTopology (zmultiples p)] : PartialHomeomorph 𝕜 (AddCircle p) := { toFun := (↑) invFun := fun x ↦ equivIco p a x From e70baf7dfd513b98f463f5db035850c7ca2a4cb0 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Mon, 15 Apr 2024 10:54:37 -0700 Subject: [PATCH 09/16] first round --- .../SpecialFunctions/Complex/Circle.lean | 34 +++++-------- Mathlib/Topology/Instances/AddCircle.lean | 49 ++++++++++--------- 2 files changed, 36 insertions(+), 47 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean index b1a70ac15d98d..ca154fd404437 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean @@ -195,29 +195,17 @@ theorem injective_toCircle (hT : T ≠ 0) : Function.Injective (@toCircle T) := linarith #align add_circle.injective_to_circle AddCircle.injective_toCircle -private noncomputable def homeomorphCircle' : AddCircle (2 * π) ≃ₜ circle := - { toFun := Real.Angle.expMapCircle - invFun := fun x ↦ arg x - left_inv := Real.Angle.arg_expMapCircle - right_inv := expMapCircle_arg - continuous_toFun := continuous_coinduced_dom.mpr expMapCircle.continuous - continuous_invFun := by - let f : circle → Real.Angle := fun x ↦ arg x - change Continuous f - have hf : ∀ x y, f (x * y) = f x + f y := by - intro x y - conv_lhs => rw [← expMapCircle_arg x, ← expMapCircle_arg y, ← expMapCircle_add] - exact Real.Angle.arg_expMapCircle (arg x + arg y) - rw [continuous_iff_continuousAt] - intro x - have hg : f = (fun y ↦ y - f x⁻¹) ∘ f ∘ (fun y ↦ y * x⁻¹) := by - ext y - rw [comp_apply, comp_apply, hf, add_sub_cancel_right] - rw [hg] - exact (continuous_sub_right (f x⁻¹)).continuousAt.comp - (((continuousAt_arg_coe_angle (ne_zero_of_mem_circle _)).comp - (continuousAt_subtype_val)).comp - (continuous_mul_right x⁻¹).continuousAt) } +private noncomputable def homeomorphCircle' : AddCircle (2 * π) ≃ₜ circle where + toFun := Real.Angle.expMapCircle + invFun := fun x ↦ arg x + left_inv := Real.Angle.arg_expMapCircle + right_inv := expMapCircle_arg + continuous_toFun := continuous_coinduced_dom.mpr expMapCircle.continuous + continuous_invFun := by + rw [continuous_iff_continuousAt] + intro x + apply (continuousAt_arg_coe_angle (ne_zero_of_mem_circle x)).comp + continuousAt_subtype_val /-- The homeomorphism between `AddCircle` and `circle`. -/ noncomputable def homeomorphCircle (hT : T ≠ 0) : AddCircle T ≃ₜ circle := diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean index baee67a2d9e50..e5881f3da8ef1 100644 --- a/Mathlib/Topology/Instances/AddCircle.lean +++ b/Mathlib/Topology/Instances/AddCircle.lean @@ -269,34 +269,35 @@ theorem continuousAt_equivIoc : ContinuousAt (equivIoc p a) x := by #align add_circle.continuous_at_equiv_Ioc AddCircle.continuousAt_equivIoc /-- The quotient map `𝕜 → AddCircle p` as a partial homeomorphism. -/ -def partialHomeomorphCoe [DiscreteTopology (zmultiples p)] : PartialHomeomorph 𝕜 (AddCircle p) := - { toFun := (↑) - invFun := fun x ↦ equivIco p a x - source := Ioo a (a + p) - target := {↑a}ᶜ - map_source' := by - intro x hx hx' - exact hx.1.ne' ((coe_eq_coe_iff_of_mem_Ico (Ioo_subset_Ico_self hx) - (left_mem_Ico.mpr (lt_add_of_pos_right a hp.out))).mp hx') - map_target' := by - intro x hx - exact (eq_left_or_mem_Ioo_of_mem_Ico (equivIco p a x).2).resolve_left - (hx ∘ ((equivIco p a).symm_apply_apply x).symm.trans ∘ congrArg _) - left_inv' := - fun x hx ↦ congrArg _ ((equivIco p a).apply_symm_apply ⟨x, Ioo_subset_Ico_self hx⟩) - right_inv' := fun x _ ↦ (equivIco p a).symm_apply_apply x - open_source := isOpen_Ioo - open_target := isOpen_compl_singleton - continuousOn_toFun := (AddCircle.continuous_mk' p).continuousOn - continuousOn_invFun := by - exact ContinuousAt.continuousOn - (fun _ ↦ continuousAt_subtype_val.comp ∘ continuousAt_equivIco p a) } +def partialHomeomorphCoe [DiscreteTopology (zmultiples p)] : + PartialHomeomorph 𝕜 (AddCircle p) where + toFun := (↑) + invFun := fun x ↦ equivIco p a x + source := Ioo a (a + p) + target := {↑a}ᶜ + map_source' := by + intro x hx hx' + exact hx.1.ne' ((coe_eq_coe_iff_of_mem_Ico (Ioo_subset_Ico_self hx) + (left_mem_Ico.mpr (lt_add_of_pos_right a hp.out))).mp hx') + map_target' := by + intro x hx + exact (eq_left_or_mem_Ioo_of_mem_Ico (equivIco p a x).2).resolve_left + (hx ∘ ((equivIco p a).symm_apply_apply x).symm.trans ∘ congrArg _) + left_inv' := + fun x hx ↦ congrArg _ ((equivIco p a).apply_symm_apply ⟨x, Ioo_subset_Ico_self hx⟩) + right_inv' := fun x _ ↦ (equivIco p a).symm_apply_apply x + open_source := isOpen_Ioo + open_target := isOpen_compl_singleton + continuousOn_toFun := (AddCircle.continuous_mk' p).continuousOn + continuousOn_invFun := by + exact ContinuousAt.continuousOn + (fun _ ↦ continuousAt_subtype_val.comp ∘ continuousAt_equivIco p a) lemma isLocalHomeomorph_coe [DiscreteTopology (zmultiples p)] [DenselyOrdered 𝕜] : IsLocalHomeomorph ((↑) : 𝕜 → AddCircle p) := by intro a - obtain ⟨b, hb⟩ := nonempty_Ioo_subtype (sub_lt_self a hp.out) - exact ⟨partialHomeomorphCoe p b, ⟨hb.2, lt_add_of_sub_right_lt hb.1⟩, rfl⟩ + obtain ⟨b, hb1, hb2⟩ := exists_between (sub_lt_self a hp.out) + exact ⟨partialHomeomorphCoe p b, ⟨hb2, lt_add_of_sub_right_lt hb1⟩, rfl⟩ end Continuity From 150ae4d58143ce36dade4b0825ec670c2d89311f Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Mon, 15 Apr 2024 10:57:17 -0700 Subject: [PATCH 10/16] second round --- Mathlib/Topology/Instances/AddCircle.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean index e5881f3da8ef1..e5ef1cafc42a8 100644 --- a/Mathlib/Topology/Instances/AddCircle.lean +++ b/Mathlib/Topology/Instances/AddCircle.lean @@ -269,7 +269,7 @@ theorem continuousAt_equivIoc : ContinuousAt (equivIoc p a) x := by #align add_circle.continuous_at_equiv_Ioc AddCircle.continuousAt_equivIoc /-- The quotient map `𝕜 → AddCircle p` as a partial homeomorphism. -/ -def partialHomeomorphCoe [DiscreteTopology (zmultiples p)] : +@[simps] def partialHomeomorphCoe [DiscreteTopology (zmultiples p)] : PartialHomeomorph 𝕜 (AddCircle p) where toFun := (↑) invFun := fun x ↦ equivIco p a x From 10e450a4a947367b378cccbb4e42c7d4dd8906f7 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Mon, 15 Apr 2024 10:57:27 -0700 Subject: [PATCH 11/16] third round --- Mathlib/Topology/Instances/AddCircle.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean index e5ef1cafc42a8..3501d2e2c4f87 100644 --- a/Mathlib/Topology/Instances/AddCircle.lean +++ b/Mathlib/Topology/Instances/AddCircle.lean @@ -3,13 +3,10 @@ Copyright (c) 2022 Oliver Nash. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Oliver Nash -/ -import Mathlib.Data.Nat.Totient +import Mathlib.Algebra.Order.ToIntervalMod import Mathlib.Algebra.Ring.AddAut import Mathlib.GroupTheory.Divisible -import Mathlib.GroupTheory.OrderOfElement -import Mathlib.Algebra.Order.Floor -import Mathlib.Algebra.Order.ToIntervalMod -import Mathlib.Topology.Instances.Real +import Mathlib.Data.Nat.Totient import Mathlib.Topology.Connected.PathConnected import Mathlib.Topology.IsLocalHomeomorph From e1e882afbdfe1b398a19d0cb3dfbf378ae60c7a1 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Mon, 15 Apr 2024 10:58:14 -0700 Subject: [PATCH 12/16] reorder --- Mathlib/Topology/Instances/AddCircle.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean index 3501d2e2c4f87..5bea917016f5a 100644 --- a/Mathlib/Topology/Instances/AddCircle.lean +++ b/Mathlib/Topology/Instances/AddCircle.lean @@ -5,8 +5,8 @@ Authors: Oliver Nash -/ import Mathlib.Algebra.Order.ToIntervalMod import Mathlib.Algebra.Ring.AddAut -import Mathlib.GroupTheory.Divisible import Mathlib.Data.Nat.Totient +import Mathlib.GroupTheory.Divisible import Mathlib.Topology.Connected.PathConnected import Mathlib.Topology.IsLocalHomeomorph From 705adf6ec49f08a95a4d669b65d09fea6ae40319 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Mon, 15 Apr 2024 11:19:14 -0700 Subject: [PATCH 13/16] avoid change --- .../SpecialFunctions/Complex/Circle.lean | 29 ++++++++++++++----- Mathlib/Topology/Instances/AddCircle.lean | 10 +++++++ 2 files changed, 31 insertions(+), 8 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean index ca154fd404437..11802da90da64 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean @@ -170,12 +170,14 @@ noncomputable def toCircle : AddCircle T → circle := (@scaled_exp_map_periodic T).lift #align add_circle.to_circle AddCircle.toCircle +theorem toCircle_apply_mk (x : ℝ) : @toCircle T x = expMapCircle (2 * π / T * x) := + rfl + theorem toCircle_add (x : AddCircle T) (y : AddCircle T) : @toCircle T (x + y) = toCircle x * toCircle y := by induction x using QuotientAddGroup.induction_on' induction y using QuotientAddGroup.induction_on' - rw [← QuotientAddGroup.mk_add] - simp_rw [toCircle, Function.Periodic.lift_coe, mul_add, expMapCircle_add] + simp_rw [← coe_add, toCircle_apply_mk, mul_add, expMapCircle_add] #align add_circle.to_circle_add AddCircle.toCircle_add theorem continuous_toCircle : Continuous (@toCircle T) := @@ -186,7 +188,7 @@ theorem injective_toCircle (hT : T ≠ 0) : Function.Injective (@toCircle T) := intro a b h induction a using QuotientAddGroup.induction_on' induction b using QuotientAddGroup.induction_on' - simp_rw [toCircle, Function.Periodic.lift_coe] at h + simp_rw [toCircle_apply_mk] at h obtain ⟨m, hm⟩ := expMapCircle_eq_expMapCircle.mp h.symm rw [QuotientAddGroup.eq]; simp_rw [AddSubgroup.mem_zmultiples_iff, zsmul_eq_mul] use m @@ -195,10 +197,10 @@ theorem injective_toCircle (hT : T ≠ 0) : Function.Injective (@toCircle T) := linarith #align add_circle.injective_to_circle AddCircle.injective_toCircle -private noncomputable def homeomorphCircle' : AddCircle (2 * π) ≃ₜ circle where - toFun := Real.Angle.expMapCircle +noncomputable def homeomorphCircle' : AddCircle (2 * π) ≃ₜ circle where + toFun := Angle.expMapCircle invFun := fun x ↦ arg x - left_inv := Real.Angle.arg_expMapCircle + left_inv := Angle.arg_expMapCircle right_inv := expMapCircle_arg continuous_toFun := continuous_coinduced_dom.mpr expMapCircle.continuous continuous_invFun := by @@ -207,6 +209,16 @@ private noncomputable def homeomorphCircle' : AddCircle (2 * π) ≃ₜ circle w apply (continuousAt_arg_coe_angle (ne_zero_of_mem_circle x)).comp continuousAt_subtype_val +theorem homeomorphCircle'_apply_mk (x : ℝ) : homeomorphCircle' x = expMapCircle x := + rfl + +theorem homeomorphCircle'_apply (x : AddCircle (2 * π)) : + homeomorphCircle' x = Angle.expMapCircle x := + rfl + +theorem homeomorphCircle'_symm_apply (x : circle) : homeomorphCircle'.symm x = arg x := + rfl + /-- The homeomorphism between `AddCircle` and `circle`. -/ noncomputable def homeomorphCircle (hT : T ≠ 0) : AddCircle T ≃ₜ circle := (homeomorphAddCircle T (2 * π) hT (by positivity)).trans homeomorphCircle' @@ -214,8 +226,9 @@ noncomputable def homeomorphCircle (hT : T ≠ 0) : AddCircle T ≃ₜ circle := theorem homeomorphCircle_apply (hT : T ≠ 0) (x : AddCircle T) : homeomorphCircle hT x = toCircle x := by induction' x using QuotientAddGroup.induction_on' with x - change expMapCircle _ = expMapCircle _ - congr; simp; ring + rw [homeomorphCircle, Homeomorph.trans_apply, + homeomorphAddCircle_apply_mk, homeomorphCircle'_apply_mk, toCircle_apply_mk] + ring_nf end AddCircle diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean index 5bea917016f5a..cc430b19b6e13 100644 --- a/Mathlib/Topology/Instances/AddCircle.lean +++ b/Mathlib/Topology/Instances/AddCircle.lean @@ -352,6 +352,16 @@ def homeomorphAddCircle (hp : p ≠ 0) (hq : q ≠ 0) : AddCircle p ≃ₜ AddCi (continuous_quotient_mk'.comp (continuous_mul_right (p⁻¹ * q))).quotient_lift _, (continuous_quotient_mk'.comp (continuous_mul_right (q⁻¹ * p))).quotient_lift _⟩ +@[simp] +theorem homeomorphAddCircle_apply_mk (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) : + homeomorphAddCircle p q hp hq (x : 𝕜) = (x * (p⁻¹ * q) : 𝕜) := + rfl + +@[simp] +theorem homeomorphAddCircle_symm_apply_mk (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) : + (homeomorphAddCircle p q hp hq).symm (x : 𝕜) = (x * (q⁻¹ * p) : 𝕜) := + rfl + variable [hp : Fact (0 < p)] section FloorRing From 9d293714d0833c5e6522343fdfc2d5d143aae906 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Mon, 15 Apr 2024 11:23:02 -0700 Subject: [PATCH 14/16] docstring --- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean index 11802da90da64..e4be1926ea7a7 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean @@ -197,6 +197,7 @@ theorem injective_toCircle (hT : T ≠ 0) : Function.Injective (@toCircle T) := linarith #align add_circle.injective_to_circle AddCircle.injective_toCircle +/-- The homeomorphism between `AddCircle (2 * π)` and `circle`. -/ noncomputable def homeomorphCircle' : AddCircle (2 * π) ≃ₜ circle where toFun := Angle.expMapCircle invFun := fun x ↦ arg x From ada10f46019b69283ba3ff04b9069d717a8f016b Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Mon, 15 Apr 2024 11:24:03 -0700 Subject: [PATCH 15/16] docstring --- Mathlib/Topology/Instances/AddCircle.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean index cc430b19b6e13..a3b71039f874a 100644 --- a/Mathlib/Topology/Instances/AddCircle.lean +++ b/Mathlib/Topology/Instances/AddCircle.lean @@ -346,7 +346,7 @@ theorem equivAddCircle_symm_apply_mk (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) : rfl #align add_circle.equiv_add_circle_symm_apply_mk AddCircle.equivAddCircle_symm_apply_mk -/-- The rescaling equivalence between additive circles with different periods. -/ +/-- The rescaling homeomorphism between additive circles with different periods. -/ def homeomorphAddCircle (hp : p ≠ 0) (hq : q ≠ 0) : AddCircle p ≃ₜ AddCircle q := ⟨equivAddCircle p q hp hq, (continuous_quotient_mk'.comp (continuous_mul_right (p⁻¹ * q))).quotient_lift _, From 811cd11064b42a45895eac0e3edfd21d2fedd6ff Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Mon, 15 Apr 2024 23:03:09 -0700 Subject: [PATCH 16/16] simps --- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean index e4be1926ea7a7..aea45153304e9 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean @@ -198,7 +198,7 @@ theorem injective_toCircle (hT : T ≠ 0) : Function.Injective (@toCircle T) := #align add_circle.injective_to_circle AddCircle.injective_toCircle /-- The homeomorphism between `AddCircle (2 * π)` and `circle`. -/ -noncomputable def homeomorphCircle' : AddCircle (2 * π) ≃ₜ circle where +@[simps] noncomputable def homeomorphCircle' : AddCircle (2 * π) ≃ₜ circle where toFun := Angle.expMapCircle invFun := fun x ↦ arg x left_inv := Angle.arg_expMapCircle @@ -213,13 +213,6 @@ noncomputable def homeomorphCircle' : AddCircle (2 * π) ≃ₜ circle where theorem homeomorphCircle'_apply_mk (x : ℝ) : homeomorphCircle' x = expMapCircle x := rfl -theorem homeomorphCircle'_apply (x : AddCircle (2 * π)) : - homeomorphCircle' x = Angle.expMapCircle x := - rfl - -theorem homeomorphCircle'_symm_apply (x : circle) : homeomorphCircle'.symm x = arg x := - rfl - /-- The homeomorphism between `AddCircle` and `circle`. -/ noncomputable def homeomorphCircle (hT : T ≠ 0) : AddCircle T ≃ₜ circle := (homeomorphAddCircle T (2 * π) hT (by positivity)).trans homeomorphCircle'