feat(algebra/order/to_interval_mod): add circular_order instance for add_circle (#17743)

eric-wieser · YaelDillies · collares · eric-wieser · commit 213b0cff7bc5 · 2023-05-10T21:40:00.000Z
This also provides us with the same instance for `real.angle`.



Co-authored-by: Yaël Dillies &lt;yael.dillies@gmail.com&gt;
Co-authored-by: Mauricio Collares &lt;mauricio@collares.org&gt;
diff --git a/src/algebra/order/to_interval_mod.lean b/src/algebra/order/to_interval_mod.lean
@@ -9,6 +9,7 @@ import algebra.order.archimedean
 import algebra.periodic
 import data.int.succ_pred
 import group_theory.quotient_group
+import order.circular
 
 /-!
 # Reducing to an interval modulo its length
@@ -32,8 +33,6 @@ interval.
 
 noncomputable theory
 
-open add_comm_group
-
 section linear_ordered_add_comm_group
 
 variables {α : Type*} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p)
@@ -562,6 +561,8 @@ end
 
 end Ico_Ioc
 
+open add_comm_group
+
 lemma to_Ico_mod_eq_self : to_Ico_mod hp a b = b ↔ b ∈ set.Ico a (a + p) :=
 by { rw [to_Ico_mod_eq_iff, and_iff_left], exact ⟨0, by simp⟩ }
 
@@ -590,6 +591,37 @@ to_Ico_mod_add_right hp a
 lemma to_Ioc_mod_periodic (a : α) : function.periodic (to_Ioc_mod hp a) p :=
 to_Ioc_mod_add_right hp a
 
+-- helper lemmas for when `a = 0`
+section zero
+
+lemma to_Ico_mod_zero_sub_comm (a b : α) : to_Ico_mod hp 0 (a - b) = p - to_Ioc_mod hp 0 (b - a) :=
+by rw [←neg_sub, to_Ico_mod_neg, neg_zero]
+
+lemma to_Ioc_mod_zero_sub_comm (a b : α) : to_Ioc_mod hp 0 (a - b) = p - to_Ico_mod hp 0 (b - a) :=
+by rw [←neg_sub, to_Ioc_mod_neg, neg_zero]
+
+lemma to_Ico_div_eq_sub (a b : α) : to_Ico_div hp a b = to_Ico_div hp 0 (b - a) :=
+by rw [to_Ico_div_sub_eq_to_Ico_div_add, zero_add]
+
+lemma to_Ioc_div_eq_sub (a b : α) : to_Ioc_div hp a b = to_Ioc_div hp 0 (b - a) :=
+by rw [to_Ioc_div_sub_eq_to_Ioc_div_add, zero_add]
+
+lemma to_Ico_mod_eq_sub (a b : α) : to_Ico_mod hp a b = to_Ico_mod hp 0 (b - a) + a :=
+by rw [to_Ico_mod_sub_eq_sub, zero_add, sub_add_cancel]
+
+lemma to_Ioc_mod_eq_sub (a b : α) : to_Ioc_mod hp a b = to_Ioc_mod hp 0 (b - a) + a :=
+by rw [to_Ioc_mod_sub_eq_sub, zero_add, sub_add_cancel]
+
+lemma to_Ico_mod_add_to_Ioc_mod_zero (a b : α) :
+  to_Ico_mod hp 0 (a - b) + to_Ioc_mod hp 0 (b - a) = p :=
+by rw [to_Ico_mod_zero_sub_comm, sub_add_cancel]
+
+lemma to_Ioc_mod_add_to_Ico_mod_zero (a b : α) :
+  to_Ioc_mod hp 0 (a - b) + to_Ico_mod hp 0 (b - a) = p :=
+by rw [add_comm, to_Ico_mod_add_to_Ioc_mod_zero]
+
+end zero
+
 /-- `to_Ico_mod` as an equiv from the quotient. -/
 @[simps symm_apply]
 def quotient_add_group.equiv_Ico_mod (a : α) :
@@ -610,7 +642,12 @@ lemma quotient_add_group.equiv_Ico_mod_coe (a b : α) :
   quotient_add_group.equiv_Ico_mod hp a ↑b = ⟨to_Ico_mod hp a b, to_Ico_mod_mem_Ico hp a _⟩ :=
 rfl
 
-/-- `to_Ioc_mod` as an equiv  from the quotient. -/
+@[simp]
+lemma quotient_add_group.equiv_Ico_mod_zero (a : α) :
+  quotient_add_group.equiv_Ico_mod hp a 0 = ⟨to_Ico_mod hp a 0, to_Ico_mod_mem_Ico hp a _⟩ :=
+rfl
+
+/-- `to_Ioc_mod` as an equiv from the quotient. -/
 @[simps symm_apply]
 def quotient_add_group.equiv_Ioc_mod (a : α) :
   (α ⧸ add_subgroup.zmultiples p) ≃ set.Ioc a (a + p) :=
@@ -630,8 +667,170 @@ lemma quotient_add_group.equiv_Ioc_mod_coe (a b : α) :
   quotient_add_group.equiv_Ioc_mod hp a ↑b = ⟨to_Ioc_mod hp a b, to_Ioc_mod_mem_Ioc hp a _⟩ :=
 rfl
 
+@[simp]
+lemma quotient_add_group.equiv_Ioc_mod_zero (a : α) :
+  quotient_add_group.equiv_Ioc_mod hp a 0 = ⟨to_Ioc_mod hp a 0, to_Ioc_mod_mem_Ioc hp a _⟩ :=
+rfl
+
+/-!
+### The circular order structure on `α ⧸ add_subgroup.zmultiples p`
+-/
+
+section circular
+
+private lemma to_Ixx_mod_iff (x₁ x₂ x₃ : α) :
+  to_Ico_mod hp x₁ x₂ ≤ to_Ioc_mod hp x₁ x₃ ↔
+  to_Ico_mod hp 0 (x₂ - x₁) + to_Ico_mod hp 0 (x₁ - x₃) ≤ p :=
+by rw [to_Ico_mod_eq_sub, to_Ioc_mod_eq_sub _ x₁, add_le_add_iff_right, ←neg_sub x₁ x₃,
+    to_Ioc_mod_neg, neg_zero, le_sub_iff_add_le]
+
+private lemma to_Ixx_mod_cyclic_left {x₁ x₂ x₃ : α}
+  (h : to_Ico_mod hp x₁ x₂ ≤ to_Ioc_mod hp x₁ x₃) :
+  to_Ico_mod hp x₂ x₃ ≤ to_Ioc_mod hp x₂ x₁ :=
+begin
+  let x₂' := to_Ico_mod hp x₁ x₂,
+  let x₃' := to_Ico_mod hp x₂' x₃,
+  have h : x₂' ≤ to_Ioc_mod hp x₁ x₃' := by simpa,
+  have h₂₁ : x₂' < x₁ + p := to_Ico_mod_lt_right _ _ _,
+  have h₃₂ : x₃' - p < x₂' := sub_lt_iff_lt_add.2 (to_Ico_mod_lt_right _ _ _),
+
+  suffices hequiv : x₃' ≤ to_Ioc_mod hp x₂' x₁,
+  { obtain ⟨z, hd⟩ : ∃ (z : ℤ), x₂ = x₂' + z • p := ((to_Ico_mod_eq_iff hp).1 rfl).2,
+    simpa [hd] },
+
+  cases le_or_lt x₃' (x₁ + p) with h₃₁ h₁₃,
+  { suffices hIoc₂₁ : to_Ioc_mod hp x₂' x₁ = x₁ + p,
+    { exact hIoc₂₁.symm.trans_ge h₃₁ },
+    apply (to_Ioc_mod_eq_iff hp).2,
+    exact ⟨⟨h₂₁, by simp [left_le_to_Ico_mod]⟩, -1, by simp⟩ },
+
+  have hIoc₁₃ : to_Ioc_mod hp x₁ x₃' = x₃' - p,
+  { apply (to_Ioc_mod_eq_iff hp).2,
+    exact ⟨⟨lt_sub_iff_add_lt.2 h₁₃, le_of_lt (h₃₂.trans h₂₁)⟩, 1, by simp⟩ },
+  have not_h₃₂ := (h.trans hIoc₁₃.le).not_lt,
+  contradiction
+end
+
+private lemma to_Ixx_mod_antisymm (h₁₂₃ : to_Ico_mod hp a b ≤ to_Ioc_mod hp a c)
+  (h₁₃₂ : to_Ico_mod hp a c ≤ to_Ioc_mod hp a b) :
+  b ≡ a [PMOD p] ∨ c ≡ b [PMOD p] ∨ a ≡ c [PMOD p] :=
+begin
+  by_contra' h,
+  rw modeq_comm at h,
+  rw ←(not_modeq_iff_to_Ico_mod_eq_to_Ioc_mod hp).mp h.2.2 at h₁₂₃,
+  rw ←(not_modeq_iff_to_Ico_mod_eq_to_Ioc_mod hp).mp h.1 at h₁₃₂,
+  exact h.2.1 ((to_Ico_mod_inj _).1 $ h₁₃₂.antisymm h₁₂₃),
+end
+
+private lemma to_Ixx_mod_total' (a b c : α) :
+  to_Ico_mod hp b a ≤ to_Ioc_mod hp b c ∨ to_Ico_mod hp b c ≤ to_Ioc_mod hp b a :=
+begin
+  /- an essential ingredient is the lemma sabing {a-b} + {b-a} = period if a ≠ b (and = 0 if a = b).
+  Thus if a ≠ b and b ≠ c then ({a-b} + {b-c}) + ({c-b} + {b-a}) = 2 * period, so one of
+  `{a-b} + {b-c}` and `{c-b} + {b-a}` must be `≤ period` -/
+  have := congr_arg2 (+)
+    (to_Ico_mod_add_to_Ioc_mod_zero hp a b) (to_Ico_mod_add_to_Ioc_mod_zero hp c b),
+  rw [add_add_add_comm, add_comm (to_Ioc_mod _ _ _), add_add_add_comm, ←two_nsmul] at this,
+  replace := min_le_of_add_le_two_nsmul this.le,
+  rw min_le_iff at this,
+  rw [to_Ixx_mod_iff, to_Ixx_mod_iff],
+  refine this.imp (le_trans $ add_le_add_left _ _) (le_trans $ add_le_add_left _ _),
+  { apply to_Ico_mod_le_to_Ioc_mod },
+  { apply to_Ico_mod_le_to_Ioc_mod }
+end
+
+private lemma to_Ixx_mod_total (a b c : α) :
+  to_Ico_mod hp a b ≤ to_Ioc_mod hp a c ∨ to_Ico_mod hp c b ≤ to_Ioc_mod hp c a :=
+(to_Ixx_mod_total' _ _ _ _).imp_right $ to_Ixx_mod_cyclic_left _
+
+private lemma to_Ixx_mod_trans {x₁ x₂ x₃ x₄ : α}
+  (h₁₂₃ : to_Ico_mod hp x₁ x₂ ≤ to_Ioc_mod hp x₁ x₃
+    ∧ ¬to_Ico_mod hp x₃ x₂ ≤ to_Ioc_mod hp x₃ x₁)
+  (h₂₃₄ : to_Ico_mod hp x₂ x₄ ≤ to_Ioc_mod hp x₂ x₃
+    ∧ ¬to_Ico_mod hp x₃ x₄ ≤ to_Ioc_mod hp x₃ x₂) :
+  to_Ico_mod hp x₁ x₄ ≤ to_Ioc_mod hp x₁ x₃
+    ∧ ¬to_Ico_mod hp x₃ x₄ ≤ to_Ioc_mod hp x₃ x₁ :=
+begin
+  split,
+  { suffices h : ¬x₃ ≡ x₂ [PMOD p],
+    { have h₁₂₃' := to_Ixx_mod_cyclic_left _ (to_Ixx_mod_cyclic_left _ h₁₂₃.1),
+      have h₂₃₄' := to_Ixx_mod_cyclic_left _ (to_Ixx_mod_cyclic_left _ h₂₃₄.1),
+      rw [(not_modeq_iff_to_Ico_mod_eq_to_Ioc_mod hp).1 h] at h₂₃₄',
+      exact to_Ixx_mod_cyclic_left _ (h₁₂₃'.trans h₂₃₄') },
+    by_contra,
+    rw [(modeq_iff_to_Ico_mod_eq_left hp).1 h] at h₁₂₃,
+    exact h₁₂₃.2 (left_lt_to_Ioc_mod _ _ _).le },
+  { rw [not_le] at h₁₂₃ h₂₃₄ ⊢,
+    exact (h₁₂₃.2.trans_le (to_Ico_mod_le_to_Ioc_mod _ x₃ x₂)).trans h₂₃₄.2 },
+end
+
+namespace quotient_add_group
+variables [hp' : fact (0 < p)]
+include hp'
+
+instance : has_btw (α ⧸ add_subgroup.zmultiples p) :=
+{ btw := λ x₁ x₂ x₃, (equiv_Ico_mod hp'.out 0 (x₂ - x₁) : α) ≤ equiv_Ioc_mod hp'.out 0 (x₃ - x₁) }
+
+lemma btw_coe_iff' {x₁ x₂ x₃ : α} :
+  has_btw.btw (x₁ : α ⧸ add_subgroup.zmultiples p) x₂ x₃ ↔
+    to_Ico_mod hp'.out 0 (x₂ - x₁) ≤ to_Ioc_mod hp'.out 0 (x₃ - x₁) :=
+iff.rfl
+
+-- maybe harder to use than the primed one?
+lemma btw_coe_iff {x₁ x₂ x₃ : α} :
+  has_btw.btw (x₁ : α ⧸ add_subgroup.zmultiples p) x₂ x₃ ↔
+    to_Ico_mod hp'.out x₁ x₂ ≤ to_Ioc_mod hp'.out x₁ x₃ :=
+by rw [btw_coe_iff', to_Ioc_mod_sub_eq_sub, to_Ico_mod_sub_eq_sub, zero_add, sub_le_sub_iff_right]
+
+instance circular_preorder : circular_preorder (α ⧸ add_subgroup.zmultiples p) :=
+{ btw_refl := λ x, show _ ≤ _, by simp [sub_self, hp'.out.le],
+  btw_cyclic_left := λ x₁ x₂ x₃ h, begin
+    induction x₁ using quotient_add_group.induction_on',
+    induction x₂ using quotient_add_group.induction_on',
+    induction x₃ using quotient_add_group.induction_on',
+    simp_rw [btw_coe_iff] at h ⊢,
+    apply to_Ixx_mod_cyclic_left _ h,
+  end,
+  sbtw := _,
+  sbtw_iff_btw_not_btw := λ _ _ _, iff.rfl,
+  sbtw_trans_left := λ x₁ x₂ x₃ x₄ (h₁₂₃ : _ ∧ _) (h₂₃₄ : _ ∧ _), show _ ∧ _, begin
+    induction x₁ using quotient_add_group.induction_on',
+    induction x₂ using quotient_add_group.induction_on',
+    induction x₃ using quotient_add_group.induction_on',
+    induction x₄ using quotient_add_group.induction_on',
+    simp_rw [btw_coe_iff] at h₁₂₃ h₂₃₄ ⊢,
+    apply to_Ixx_mod_trans _ h₁₂₃ h₂₃₄,
+  end }
+
+instance circular_order : circular_order (α ⧸ add_subgroup.zmultiples p) :=
+{ btw_antisymm := λ x₁ x₂ x₃ h₁₂₃ h₃₂₁, begin
+    induction x₁ using quotient_add_group.induction_on',
+    induction x₂ using quotient_add_group.induction_on',
+    induction x₃ using quotient_add_group.induction_on',
+    rw btw_cyclic at h₃₂₁,
+    simp_rw [btw_coe_iff] at h₁₂₃ h₃₂₁,
+    simp_rw ←modeq_iff_eq_mod_zmultiples,
+    exact to_Ixx_mod_antisymm _ h₁₂₃ h₃₂₁,
+  end,
+  btw_total := λ x₁ x₂ x₃, begin
+    induction x₁ using quotient_add_group.induction_on',
+    induction x₂ using quotient_add_group.induction_on',
+    induction x₃ using quotient_add_group.induction_on',
+    simp_rw [btw_coe_iff] at ⊢,
+    apply to_Ixx_mod_total,
+  end,
+  ..quotient_add_group.circular_preorder }
+
+end quotient_add_group
+
+end circular
+
 end linear_ordered_add_comm_group
 
+/-!
+### Connections to `int.floor` and `int.fract`
+-/
+
 section linear_ordered_field
 
 variables {α : Type*} [linear_ordered_field α] [floor_ring α] {p : α} (hp : 0 < p)
diff --git a/src/analysis/special_functions/trigonometric/angle.lean b/src/analysis/special_functions/trigonometric/angle.lean
@@ -27,6 +27,9 @@ def angle : Type := add_circle (2 * π)
 
 namespace angle
 
+instance : circular_order real.angle :=
+@add_circle.circular_order _ _ _ _ _ ⟨by norm_num [pi_pos]⟩ _
+
 @[continuity] lemma continuous_coe : continuous (coe : ℝ → angle) :=
 continuous_quotient_mk
 
diff --git a/src/order/circular.lean b/src/order/circular.lean
@@ -70,7 +70,7 @@ What is the correct generality of "rolling the necklace" open? At least, this wo
 `β × α` where `α` is a circular order and `β` is a linear order.
 
 What's next is to define circular groups and provide instances for `zmod n`, the usual circle group
-`circle`, `real.angle`, and `roots_of_unity M`. What conditions do we need on `M` for this last one
+`circle`, and `roots_of_unity M`. What conditions do we need on `M` for this last one
 to work?
 
 We should have circular order homomorphisms. The typical example is
diff --git a/src/topology/instances/add_circle.lean b/src/topology/instances/add_circle.lean
@@ -154,6 +154,9 @@ include hp
 
 variables (a : 𝕜) [archimedean 𝕜]
 
+instance : circular_order (add_circle p) :=
+quotient_add_group.circular_order
+
 /-- The equivalence between `add_circle p` and the half-open interval `[a, a + p)`, whose inverse
 is the natural quotient map. -/
 def equiv_Ico : add_circle p ≃ Ico a (a + p) := quotient_add_group.equiv_Ico_mod hp.out a
