chore(algebra/order/archimedean): Move material to correct files (#15290

)

Move `round` and some `floor` lemmas to `algebra.order.floor`. Move the `rat.cast` lemmas about `floor` and `ceil` to `data.rat.floor`. Merge a few sections together now that unrelated lemmas are gone.

src/algebra/order/archimedean.lean

@@ -20,8 +20,6 @@ number `n` such that `x ≤ n • y`.
   property.
 * `archimedean.floor_ring` defines a floor function on an archimedean linearly ordered ring making
   it into a `floor_ring`.
-* `round` defines a function rounding to the nearest integer for a linearly ordered field which is
-  also a floor ring.
 
 ## Main statements
 
@@ -154,15 +152,12 @@ end
 end linear_ordered_ring
 
 section linear_ordered_field
-
-variables [linear_ordered_field α]
+variables [linear_ordered_field α] [archimedean α] {x y ε : α}
 
 /-- Every positive `x` is between two successive integer powers of
 another `y` greater than one. This is the same as `exists_mem_Ioc_zpow`,
 but with ≤ and < the other way around. -/
-lemma exists_mem_Ico_zpow [archimedean α]
-  {x : α} {y : α} (hx : 0 < x) (hy : 1 < y) :
-  ∃ n : ℤ, x ∈ set.Ico (y ^ n) (y ^ (n + 1)) :=
+lemma exists_mem_Ico_zpow (hx : 0 < x) (hy : 1 < y) : ∃ n : ℤ, x ∈ Ico (y ^ n) (y ^ (n + 1)) :=
 by classical; exact
 let ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy in
   have he: ∃ m : ℤ, y ^ m ≤ x, from
@@ -179,9 +174,7 @@ let ⟨n, hn₁, hn₂⟩ := int.exists_greatest_of_bdd hb he in
 /-- Every positive `x` is between two successive integer powers of
 another `y` greater than one. This is the same as `exists_mem_Ico_zpow`,
 but with ≤ and < the other way around. -/
-lemma exists_mem_Ioc_zpow [archimedean α]
-  {x : α} {y : α} (hx : 0 < x) (hy : 1 < y) :
-  ∃ n : ℤ, x ∈ set.Ioc (y ^ n) (y ^ (n + 1)) :=
+lemma exists_mem_Ioc_zpow (hx : 0 < x) (hy : 1 < y) : ∃ n : ℤ, x ∈ Ioc (y ^ n) (y ^ (n + 1)) :=
 let ⟨m, hle, hlt⟩ := exists_mem_Ico_zpow (inv_pos.2 hx) hy in
 have hyp : 0 < y, from lt_trans zero_lt_one hy,
 ⟨-(m+1),
@@ -190,8 +183,7 @@ by rwa [neg_add, neg_add_cancel_right, zpow_neg,
         le_inv hx (zpow_pos_of_pos hyp _)]⟩
 
 /-- For any `y < 1` and any positive `x`, there exists `n : ℕ` with `y ^ n < x`. -/
-lemma exists_pow_lt_of_lt_one [archimedean α] {x y : α} (hx : 0 < x) (hy : y < 1) :
-  ∃ n : ℕ, y ^ n < x :=
+lemma exists_pow_lt_of_lt_one (hx : 0 < x) (hy : y < 1) : ∃ n : ℕ, y ^ n < x :=
 begin
   by_cases y_pos : y ≤ 0,
   { use 1, simp only [pow_one], linarith, },
@@ -202,8 +194,7 @@ end
 
 /-- Given `x` and `y` between `0` and `1`, `x` is between two successive powers of `y`.
 This is the same as `exists_nat_pow_near`, but for elements between `0` and `1` -/
-lemma exists_nat_pow_near_of_lt_one [archimedean α]
-  {x : α} {y : α} (xpos : 0 < x) (hx : x ≤ 1) (ypos : 0 < y) (hy : y < 1) :
+lemma exists_nat_pow_near_of_lt_one (xpos : 0 < x) (hx : x ≤ 1) (ypos : 0 < y) (hy : y < 1) :
   ∃ n : ℕ, y ^ (n + 1) < x ∧ x ≤ y ^ n :=
 begin
   rcases exists_nat_pow_near (one_le_inv_iff.2 ⟨xpos, hx⟩) (one_lt_inv_iff.2 ⟨ypos, hy⟩)
@@ -213,78 +204,9 @@ begin
   { rwa [inv_pow, inv_le_inv (pow_pos ypos _) xpos] at hn }
 end
 
-variables [floor_ring α]
-
-lemma sub_floor_div_mul_nonneg (x : α) {y : α} (hy : 0 < y) :
-  0 ≤ x - ⌊x / y⌋ * y :=
-begin
-  conv in x {rw ← div_mul_cancel x (ne_of_lt hy).symm},
-  rw ← sub_mul,
-  exact mul_nonneg (sub_nonneg.2 (floor_le _)) (le_of_lt hy)
-end
-
-lemma sub_floor_div_mul_lt (x : α) {y : α} (hy : 0 < y) :
-  x - ⌊x / y⌋ * y < y :=
-sub_lt_iff_lt_add.2 begin
-  conv in y {rw ← one_mul y},
-  conv in x {rw ← div_mul_cancel x (ne_of_lt hy).symm},
-  rw ← add_mul,
-  exact (mul_lt_mul_right hy).2 (by rw add_comm; exact lt_floor_add_one _),
-end
-
-end linear_ordered_field
-
-instance : archimedean ℕ :=
-⟨λ n m m0, ⟨n, by simpa only [mul_one, nat.nsmul_eq_mul] using nat.mul_le_mul_left n m0⟩⟩
-
-instance : archimedean ℤ :=
-⟨λ n m m0, ⟨n.to_nat, le_trans (int.le_to_nat _) $
-by simpa only [nsmul_eq_mul, zero_add, mul_one]
-  using mul_le_mul_of_nonneg_left (int.add_one_le_iff.2 m0) (int.coe_zero_le n.to_nat)⟩⟩
-
-/-- A linear ordered archimedean ring is a floor ring. This is not an `instance` because in some
-cases we have a computable `floor` function. -/
-noncomputable def archimedean.floor_ring (α)
-  [linear_ordered_ring α] [archimedean α] : floor_ring α :=
-floor_ring.of_floor α (λ a, classical.some (exists_floor a))
-  (λ z a, (classical.some_spec (exists_floor a) z).symm)
-
-section linear_ordered_field
-variables [linear_ordered_field α]
-
-theorem archimedean_iff_nat_lt :
-  archimedean α ↔ ∀ x : α, ∃ n : ℕ, x < n :=
-⟨@exists_nat_gt α _ _, λ H, ⟨λ x y y0,
-  (H (x / y)).imp $ λ n h, le_of_lt $
-  by rwa [div_lt_iff y0, ← nsmul_eq_mul] at h⟩⟩
-
-theorem archimedean_iff_nat_le :
-  archimedean α ↔ ∀ x : α, ∃ n : ℕ, x ≤ n :=
-archimedean_iff_nat_lt.trans
-⟨λ H x, (H x).imp $ λ _, le_of_lt,
- λ H x, let ⟨n, h⟩ := H x in ⟨n+1,
-   lt_of_le_of_lt h (nat.cast_lt.2 (lt_add_one _))⟩⟩
-
-theorem exists_rat_gt [archimedean α] (x : α) : ∃ q : ℚ, x < q :=
+lemma exists_rat_gt (x : α) : ∃ q : ℚ, x < q :=
 let ⟨n, h⟩ := exists_nat_gt x in ⟨n, by rwa rat.cast_coe_nat⟩
 
-theorem archimedean_iff_rat_lt :
-  archimedean α ↔ ∀ x : α, ∃ q : ℚ, x < q :=
-⟨@exists_rat_gt α _,
-  λ H, archimedean_iff_nat_lt.2 $ λ x,
-  let ⟨q, h⟩ := H x in
-  ⟨⌈q⌉₊, lt_of_lt_of_le h $
-    by simpa only [rat.cast_coe_nat] using (@rat.cast_le α _ _ _).2 (nat.le_ceil _)⟩⟩
-
-theorem archimedean_iff_rat_le :
-  archimedean α ↔ ∀ x : α, ∃ q : ℚ, x ≤ q :=
-archimedean_iff_rat_lt.trans
-⟨λ H x, (H x).imp $ λ _, le_of_lt,
- λ H x, let ⟨n, h⟩ := H x in ⟨n+1,
-   lt_of_le_of_lt h (rat.cast_lt.2 (lt_add_one _))⟩⟩
-
-variables [archimedean α] {x y : α}
-
 theorem exists_rat_lt (x : α) : ∃ q : ℚ, (q : α) < x :=
 let ⟨n, h⟩ := exists_int_lt x in ⟨n, by rwa rat.cast_coe_int⟩
 
@@ -334,50 +256,55 @@ end
 theorem exists_pos_rat_lt {x : α} (x0 : 0 < x) : ∃ q : ℚ, 0 < q ∧ (q : α) < x :=
 by simpa only [rat.cast_pos] using exists_rat_btwn x0
 
-end linear_ordered_field
+lemma exists_rat_near (x : α) (ε0 : 0 < ε) : ∃ q : ℚ, |x - q| < ε :=
+let ⟨q, h₁, h₂⟩ := exists_rat_btwn $ ((sub_lt_self_iff x).2 ε0).trans ((lt_add_iff_pos_left x).2 ε0)
+  in ⟨q, abs_sub_lt_iff.2 ⟨sub_lt.1 h₁, sub_lt_iff_lt_add.2 h₂⟩⟩
 
-section
-variables [linear_ordered_field α] [floor_ring α]
-
-/-- `round` rounds a number to the nearest integer. `round (1 / 2) = 1` -/
-def round (x : α) : ℤ := ⌊x + 1 / 2⌋
-
-@[simp] lemma round_zero : round (0 : α) = 0 := floor_eq_iff.2 (by norm_num)
-@[simp] lemma round_one : round (1 : α) = 1 := floor_eq_iff.2 (by norm_num)
+end linear_ordered_field
 
-lemma abs_sub_round (x : α) : |x - round x| ≤ 1 / 2 :=
-begin
-  rw [round, abs_sub_le_iff],
-  have := floor_le (x + 1 / 2),
-  have := lt_floor_add_one (x + 1 / 2),
-  split; linarith
-end
+section linear_ordered_field
+variables [linear_ordered_field α]
 
-@[simp, norm_cast] theorem rat.floor_cast (x : ℚ) : ⌊(x:α)⌋ = ⌊x⌋ :=
-floor_eq_iff.2 (by exact_mod_cast floor_eq_iff.1 (eq.refl ⌊x⌋))
+lemma archimedean_iff_nat_lt : archimedean α ↔ ∀ x : α, ∃ n : ℕ, x < n :=
+⟨@exists_nat_gt α _ _, λ H, ⟨λ x y y0,
+  (H (x / y)).imp $ λ n h, le_of_lt $
+  by rwa [div_lt_iff y0, ← nsmul_eq_mul] at h⟩⟩
 
-@[simp, norm_cast] theorem rat.ceil_cast (x : ℚ) : ⌈(x:α)⌉ = ⌈x⌉ :=
-by rw [←neg_inj, ←floor_neg, ←floor_neg, ← rat.cast_neg, rat.floor_cast]
+lemma archimedean_iff_nat_le : archimedean α ↔ ∀ x : α, ∃ n : ℕ, x ≤ n :=
+archimedean_iff_nat_lt.trans
+⟨λ H x, (H x).imp $ λ _, le_of_lt,
+ λ H x, let ⟨n, h⟩ := H x in ⟨n+1,
+   lt_of_le_of_lt h (nat.cast_lt.2 (lt_add_one _))⟩⟩
 
-@[simp, norm_cast] theorem rat.round_cast (x : ℚ) : round (x:α) = round x :=
-have ((x + 1 / 2 : ℚ) : α) = x + 1 / 2, by simp,
-by rw [round, round, ← this, rat.floor_cast]
+lemma archimedean_iff_rat_lt : archimedean α ↔ ∀ x : α, ∃ q : ℚ, x < q :=
+⟨@exists_rat_gt α _,
+  λ H, archimedean_iff_nat_lt.2 $ λ x,
+  let ⟨q, h⟩ := H x in
+  ⟨⌈q⌉₊, lt_of_lt_of_le h $
+    by simpa only [rat.cast_coe_nat] using (@rat.cast_le α _ _ _).2 (nat.le_ceil _)⟩⟩
 
-@[simp, norm_cast] theorem rat.cast_fract (x : ℚ) : (↑(fract x) : α) = fract x :=
-by { simp only [fract, rat.cast_sub], simp }
+lemma archimedean_iff_rat_le : archimedean α ↔ ∀ x : α, ∃ q : ℚ, x ≤ q :=
+archimedean_iff_rat_lt.trans
+⟨λ H x, (H x).imp $ λ _, le_of_lt,
+ λ H x, let ⟨n, h⟩ := H x in ⟨n+1,
+   lt_of_le_of_lt h (rat.cast_lt.2 (lt_add_one _))⟩⟩
 
-end
+end linear_ordered_field
 
-section
-variables [linear_ordered_field α] [archimedean α]
+instance : archimedean ℕ :=
+⟨λ n m m0, ⟨n, by simpa only [mul_one, nat.nsmul_eq_mul] using nat.mul_le_mul_left n m0⟩⟩
 
-theorem exists_rat_near (x : α) {ε : α} (ε0 : 0 < ε) :
-  ∃ q : ℚ, |x - q| < ε :=
-let ⟨q, h₁, h₂⟩ := exists_rat_btwn $
-  lt_trans ((sub_lt_self_iff x).2 ε0) ((lt_add_iff_pos_left x).2 ε0) in
-⟨q, abs_sub_lt_iff.2 ⟨sub_lt.1 h₁, sub_lt_iff_lt_add.2 h₂⟩⟩
+instance : archimedean ℤ :=
+⟨λ n m m0, ⟨n.to_nat, le_trans (int.le_to_nat _) $
+by simpa only [nsmul_eq_mul, zero_add, mul_one]
+  using mul_le_mul_of_nonneg_left (int.add_one_le_iff.2 m0) (int.coe_zero_le n.to_nat)⟩⟩
 
 instance : archimedean ℚ :=
 archimedean_iff_rat_le.2 $ λ q, ⟨q, by rw rat.cast_id⟩
 
-end
+/-- A linear ordered archimedean ring is a floor ring. This is not an `instance` because in some
+cases we have a computable `floor` function. -/
+noncomputable def archimedean.floor_ring (α) [linear_ordered_ring α] [archimedean α] :
+  floor_ring α :=
+floor_ring.of_floor α (λ a, classical.some (exists_floor a))
+  (λ z a, (classical.some_spec (exists_floor a) z).symm)

src/algebra/order/floor.lean

@@ -23,6 +23,7 @@ We define the natural- and integer-valued floor and ceil functions on linearly o
 * `int.floor a`: Greatest integer `z` such that `z ≤ a`.
 * `int.ceil a`: Least integer `z` such that `a ≤ z`.
 * `int.fract a`: Fractional part of `a`, defined as `a - floor a`.
+* `round a`: Nearest integer to `a`. It rounds halves towards infinity.
 
 ## Notations
 
@@ -590,7 +591,7 @@ end
 
 section linear_ordered_field
 
-variables {k : Type*} [linear_ordered_field k] [floor_ring k]
+variables {k : Type*} [linear_ordered_field k] [floor_ring k] {b : k}
 
 lemma fract_div_mul_self_mem_Ico (a b : k) (ha : 0 < a) : fract (b/a) * a ∈ Ico 0 a :=
 ⟨(zero_le_mul_right ha).2 (fract_nonneg (b/a)), (mul_lt_iff_lt_one_left ha).2 (fract_lt_one (b/a))⟩
@@ -599,6 +600,12 @@ lemma fract_div_mul_self_add_zsmul_eq (a b : k) (ha : a ≠ 0) :
   fract (b/a) * a + ⌊b/a⌋ • a = b :=
 by rw [zsmul_eq_mul, ← add_mul, fract_add_floor, div_mul_cancel b ha]
 
+lemma sub_floor_div_mul_nonneg (a : k) (hb : 0 < b) : 0 ≤ a - ⌊a / b⌋ * b :=
+sub_nonneg_of_le $ (le_div_iff hb).1 $ floor_le _
+
+lemma sub_floor_div_mul_lt (a : k) (hb : 0 < b) : a - ⌊a / b⌋ * b < b :=
+sub_lt_iff_lt_add.2 $ by { rw [←one_add_mul, ←div_lt_iff hb, add_comm], exact lt_floor_add_one _ }
+
 end linear_ordered_field
 
 /-! #### Ceil -/
@@ -695,6 +702,29 @@ by { ext, simp [le_floor] }
 
 end int
 
+open int
+
+/-! ### Round -/
+
+section round
+variables [linear_ordered_field α] [floor_ring α]
+
+/-- `round` rounds a number to the nearest integer. `round (1 / 2) = 1` -/
+def round (x : α) : ℤ := ⌊x + 1 / 2⌋
+
+@[simp] lemma round_zero : round (0 : α) = 0 := floor_eq_iff.2 (by norm_num)
+@[simp] lemma round_one : round (1 : α) = 1 := floor_eq_iff.2 (by norm_num)
+
+lemma abs_sub_round (x : α) : |x - round x| ≤ 1 / 2 :=
+begin
+  rw [round, abs_sub_le_iff],
+  have := floor_le (x + 1 / 2),
+  have := lt_floor_add_one (x + 1 / 2),
+  split; linarith
+end
+
+end round
+
 variables {α} [linear_ordered_ring α] [floor_ring α]
 
 /-! #### A floor ring as a floor semiring -/

src/analysis/special_functions/trigonometric/basic.lean

@@ -364,9 +364,9 @@ lemma sin_eq_zero_iff_of_lt_of_lt {x : ℝ} (hx₁ : -π < x) (hx₂ : x < π) :
   λ h, by simp [h]⟩
 
 lemma sin_eq_zero_iff {x : ℝ} : sin x = 0 ↔ ∃ n : ℤ, (n : ℝ) * π = x :=
-⟨λ h, ⟨⌊x / π⌋, le_antisymm (sub_nonneg.1 (sub_floor_div_mul_nonneg _ pi_pos))
+⟨λ h, ⟨⌊x / π⌋, le_antisymm (sub_nonneg.1 (int.sub_floor_div_mul_nonneg _ pi_pos))
   (sub_nonpos.1 $ le_of_not_gt $ λ h₃,
-    (sin_pos_of_pos_of_lt_pi h₃ (sub_floor_div_mul_lt _ pi_pos)).ne
+    (sin_pos_of_pos_of_lt_pi h₃ (int.sub_floor_div_mul_lt _ pi_pos)).ne
     (by simp [sub_eq_add_neg, sin_add, h, sin_int_mul_pi]))⟩,
   λ ⟨n, hn⟩, hn ▸ sin_int_mul_pi _⟩
 

src/data/rat/floor.lean

@@ -22,6 +22,7 @@ rat, rationals, ℚ, floor
 open int
 
 namespace rat
+variables {α : Type*} [linear_ordered_field α] [floor_ring α]
 
 /-- `floor q` is the largest integer `z` such that `z ≤ q` -/
 protected def floor : ℚ → ℤ
@@ -56,6 +57,19 @@ begin
   rwa [←d_eq_c_mul_denom, int.coe_nat_pos],
 end
 
+@[simp, norm_cast] lemma floor_cast (x : ℚ) : ⌊(x : α)⌋ = ⌊x⌋ :=
+floor_eq_iff.2 (by exact_mod_cast floor_eq_iff.1 (eq.refl ⌊x⌋))
+
+@[simp, norm_cast] lemma ceil_cast (x : ℚ) : ⌈(x : α)⌉ = ⌈x⌉ :=
+by rw [←neg_inj, ←floor_neg, ←floor_neg, ← rat.cast_neg, rat.floor_cast]
+
+@[simp, norm_cast] lemma round_cast (x : ℚ) : round (x : α) = round x :=
+have ((x + 1 / 2 : ℚ) : α) = x + 1 / 2, by simp,
+by rw [round, round, ← this, floor_cast]
+
+@[simp, norm_cast] lemma cast_fract (x : ℚ) : (↑(fract x) : α) = fract x :=
+by simp only [fract, cast_sub, cast_coe_int, floor_cast]
+
 end rat