feat(algebra/order): Unions of interval translates by ℤ (#18427)

Write a linearly ordered abelian group as a union of pairwise disjoint intervals `⋃ (n : ℤ), Ioc (a + n • b) (a + (n + 1) • b)` (in multiple variations). Split off from #18425, which in turn was split from #18392.

Author: loefflerd

src/algebra/order/to_interval_mod.lean

@@ -733,3 +733,77 @@ lemma to_Ico_mod_zero_one (x : α) : to_Ico_mod (0 : α) zero_lt_one x = int.fra
 by simp [to_Ico_mod_eq_add_fract_mul]
 
 end linear_ordered_field
+
+/-! ### Lemmas about unions of translates of intervals -/
+section union
+
+open set int
+
+section linear_ordered_add_comm_group
+
+variables {α : Type*} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b)
+include hb
+
+lemma Union_Ioc_add_zsmul : (⋃ (n : ℤ), Ioc (a + n • b) (a + (n + 1) • b)) = univ :=
+begin
+  refine eq_univ_iff_forall.mpr (λ x, mem_Union.mpr _),
+  rcases sub_to_Ioc_div_zsmul_mem_Ioc a hb x with ⟨hl, hr⟩,
+  refine ⟨to_Ioc_div a hb x, ⟨lt_sub_iff_add_lt.mp hl, _⟩⟩,
+  rw [add_smul, one_smul, ←add_assoc],
+  convert sub_le_iff_le_add.mp hr using 1, abel,
+end
+
+lemma Union_Ico_add_zsmul : (⋃ (n : ℤ), Ico (a + n • b) (a + (n + 1) • b)) = univ :=
+begin
+  refine eq_univ_iff_forall.mpr (λ x, mem_Union.mpr _),
+  rcases sub_to_Ico_div_zsmul_mem_Ico a hb x with ⟨hl, hr⟩,
+  refine ⟨to_Ico_div a hb x, ⟨le_sub_iff_add_le.mp hl, _⟩⟩,
+  rw [add_smul, one_smul, ←add_assoc],
+  convert sub_lt_iff_lt_add.mp hr using 1, abel,
+end
+
+lemma Union_Icc_add_zsmul : (⋃ (n : ℤ), Icc (a + n • b) (a + (n + 1) • b)) = univ :=
+by simpa only [Union_Ioc_add_zsmul a hb, univ_subset_iff] using
+  Union_mono (λ n : ℤ, (Ioc_subset_Icc_self : Ioc (a + n • b) (a + (n + 1) • b) ⊆ Icc _ _))
+
+lemma Union_Ioc_zsmul : (⋃ (n : ℤ), Ioc (n • b) ((n + 1) • b)) = univ :=
+by simpa only [zero_add] using Union_Ioc_add_zsmul 0 hb
+
+lemma Union_Ico_zsmul : (⋃ (n : ℤ), Ico (n • b) ((n + 1) • b)) = univ :=
+by simpa only [zero_add] using Union_Ico_add_zsmul 0 hb
+
+lemma Union_Icc_zsmul : (⋃ (n : ℤ), Icc (n • b) ((n + 1) • b)) = univ :=
+by simpa only [zero_add] using Union_Icc_add_zsmul 0 hb
+
+end linear_ordered_add_comm_group
+
+section linear_ordered_ring
+
+variables {α : Type*} [linear_ordered_ring α] [archimedean α] (a : α)
+
+lemma Union_Ioc_add_int_cast : (⋃ (n : ℤ), Ioc (a + n) (a + n + 1)) = set.univ :=
+by simpa only [zsmul_one, int.cast_add, int.cast_one, ←add_assoc]
+  using Union_Ioc_add_zsmul a zero_lt_one
+
+lemma Union_Ico_add_int_cast : (⋃ (n : ℤ), Ico (a + n) (a + n + 1)) = set.univ :=
+by simpa only [zsmul_one, int.cast_add, int.cast_one, ←add_assoc]
+  using Union_Ico_add_zsmul a zero_lt_one
+
+lemma Union_Icc_add_int_cast : (⋃ (n : ℤ), Icc (a + n) (a + n + 1)) = set.univ :=
+by simpa only [zsmul_one, int.cast_add, int.cast_one, ←add_assoc]
+  using Union_Icc_add_zsmul a (zero_lt_one' α)
+
+variables (α)
+
+lemma Union_Ioc_int_cast : (⋃ (n : ℤ), Ioc (n : α) (n + 1)) = set.univ :=
+by simpa only [zero_add] using Union_Ioc_add_int_cast (0 : α)
+
+lemma Union_Ico_int_cast : (⋃ (n : ℤ), Ico (n : α) (n + 1)) = set.univ :=
+by simpa only [zero_add] using Union_Ico_add_int_cast (0 : α)
+
+lemma Union_Icc_int_cast : (⋃ (n : ℤ), Icc (n : α) (n + 1)) = set.univ :=
+by simpa only [zero_add] using Union_Icc_add_int_cast (0 : α)
+
+end linear_ordered_ring
+
+end union

src/data/set/intervals/group.lean

@@ -4,12 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot, Yury Kudryashov, Rémy Degenne
 -/
 import data.set.intervals.basic
+import data.set.pairwise
 import algebra.order.group.abs
+import algebra.group_power.lemmas
 
-/-! ### Lemmas about arithmetic operations and intervals. 
+/-! ### Lemmas about arithmetic operations and intervals.
 
 > THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
-> Any changes to this file require a corresponding PR to mathlib4.-/
+> Any changes to this file require a corresponding PR to mathlib4.
+-/
 
 variables {α : Type*}
 
@@ -98,4 +101,99 @@ end
 
 end linear_ordered_add_comm_group
 
+/-! ### Lemmas about disjointness of translates of intervals -/
+section pairwise_disjoint
+
+section ordered_comm_group
+
+variables [ordered_comm_group α] (a b : α)
+
+@[to_additive]
+lemma pairwise_disjoint_Ioc_mul_zpow  :
+  pairwise (disjoint on λ n : ℤ, Ioc (a * b ^ n) (a * b ^ (n + 1))) :=
+begin
+  simp_rw [function.on_fun, set.disjoint_iff],
+  intros m n hmn x hx,
+  apply hmn,
+  have hb : 1 < b,
+  { have : a * b ^ m < a * b ^ (m + 1), from hx.1.1.trans_le hx.1.2,
+    rwa [mul_lt_mul_iff_left, ←mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this },
+  have i1 := hx.1.1.trans_le hx.2.2,
+  have i2 := hx.2.1.trans_le hx.1.2,
+  rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff hb, int.lt_add_one_iff] at i1 i2,
+  exact le_antisymm i1 i2
+end
+
+@[to_additive]
+lemma pairwise_disjoint_Ico_mul_zpow :
+  pairwise (disjoint on λ n : ℤ, Ico (a * b ^ n) (a * b ^ (n + 1))) :=
+begin
+  simp_rw [function.on_fun, set.disjoint_iff],
+  intros m n hmn x hx,
+  apply hmn,
+  have hb : 1 < b,
+  { have : a * b ^ m < a * b ^ (m + 1), from hx.1.1.trans_lt hx.1.2,
+    rwa [mul_lt_mul_iff_left, ←mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this },
+  have i1 := hx.1.1.trans_lt hx.2.2,
+  have i2 := hx.2.1.trans_lt hx.1.2,
+  rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff hb, int.lt_add_one_iff] at i1 i2,
+  exact le_antisymm i1 i2,
+end
+
+@[to_additive]
+lemma pairwise_disjoint_Ioo_mul_zpow :
+  pairwise (disjoint on λ n : ℤ, Ioo (a * b ^ n) (a * b ^ (n + 1))) :=
+λ m n hmn, (pairwise_disjoint_Ioc_mul_zpow a b hmn).mono Ioo_subset_Ioc_self Ioo_subset_Ioc_self
+
+@[to_additive]
+lemma pairwise_disjoint_Ioc_zpow :
+  pairwise (disjoint on λ n : ℤ, Ioc (b ^ n) (b ^ (n + 1))) :=
+by simpa only [one_mul] using pairwise_disjoint_Ioc_mul_zpow 1 b
+
+@[to_additive]
+lemma pairwise_disjoint_Ico_zpow :
+  pairwise (disjoint on λ n : ℤ, Ico (b ^ n) (b ^ (n + 1))) :=
+by simpa only [one_mul] using pairwise_disjoint_Ico_mul_zpow 1 b
+
+@[to_additive]
+lemma pairwise_disjoint_Ioo_zpow :
+  pairwise (disjoint on λ n : ℤ, Ioo (b ^ n) (b ^ (n + 1))) :=
+by simpa only [one_mul] using pairwise_disjoint_Ioo_mul_zpow 1 b
+
+end ordered_comm_group
+
+section ordered_ring
+
+variables [ordered_ring α] (a : α)
+
+lemma pairwise_disjoint_Ioc_add_int_cast :
+  pairwise (disjoint on λ n : ℤ, Ioc (a + n) (a + n + 1)) :=
+by simpa only [zsmul_one, int.cast_add, int.cast_one, ←add_assoc]
+  using pairwise_disjoint_Ioc_add_zsmul a (1 : α)
+
+lemma pairwise_disjoint_Ico_add_int_cast :
+  pairwise (disjoint on λ n : ℤ, Ico (a + n) (a + n + 1)) :=
+by simpa only [zsmul_one, int.cast_add, int.cast_one, ←add_assoc]
+  using pairwise_disjoint_Ico_add_zsmul a (1 : α)
+
+lemma pairwise_disjoint_Ioo_add_int_cast :
+  pairwise (disjoint on λ n : ℤ, Ioo (a + n) (a + n + 1)) :=
+by simpa only [zsmul_one, int.cast_add, int.cast_one, ←add_assoc]
+  using pairwise_disjoint_Ioo_add_zsmul a (1 : α)
+
+variables (α)
+
+lemma pairwise_disjoint_Ico_int_cast : pairwise (disjoint on λ n : ℤ, Ico (n : α) (n + 1)) :=
+by simpa only [zero_add] using pairwise_disjoint_Ico_add_int_cast (0 : α)
+
+lemma pairwise_disjoint_Ioo_int_cast : pairwise (disjoint on λ n : ℤ, Ioo (n : α) (n + 1)) :=
+by simpa only [zero_add] using pairwise_disjoint_Ioo_add_int_cast (0 : α)
+
+lemma pairwise_disjoint_Ioc_int_cast : pairwise (disjoint on λ n : ℤ, Ioc (n : α) (n + 1)) :=
+by simpa only [zero_add] using pairwise_disjoint_Ioc_add_int_cast (0 : α)
+
+end ordered_ring
+
+end pairwise_disjoint
+
 end set