Apostol. Begin working through floor/ceiling exercises.

Also discovered the basic interval module so replaced custom
interval syntax with it.

Bookshelf/Apostol/Chapter_1_11.lean

@@ -1,7 +1,5 @@
 import Mathlib.Data.Real.Basic
 
-import Common.Real.Int
-
 /-! # Apostol.Chapter_1_11 -/
 
 namespace Apostol.Chapter_1_11
@@ -15,18 +13,35 @@ Prove that the greatest-integer function has the properties indicated.
 
 `⌊x + n⌋ = ⌊x⌋ + n` for every integer `n`.
 -/
-theorem exercise_4a (x : ℝ) (n : ℤ) : ⌊x + n⌋ = ⌊x⌋ + n := by
+theorem exercise_4a (x : ℝ) (n : ℤ) : ⌊x + n⌋ = ⌊x⌋ + n :=
-  sorry
+  Int.floor_add_int x n
 
-/-- ### Exercise 4b
+/-- ### Exercise 4b.1
 
 `⌊-x⌋ = -⌊x⌋` if `x` is an integer.
+-/
+theorem exercise_4b_1 (x : ℤ) : ⌊-x⌋ = -⌊x⌋ := by
+  simp only [Int.floor_int, id_eq]
+
+/-- ### Exercise 4b.2
+
 `⌊-x⌋ = -⌊x⌋ - 1` otherwise.
 -/
-theorem exercise_4b (x : ℝ)
+theorem exercise_4b_2 (x : ℝ) (h : ∃ n : ℤ, x ∈ Set.Ioo ↑n (↑n + (1 : ℝ)))
-  : (Real.isInt x → ⌊-x⌋ = -⌊x⌋)
+  : ⌊-x⌋ = -⌊x⌋ - 1 := by
-  ∨ (¬Real.isInt x → ⌊-x⌋ = -⌊x⌋ - 1) := by
+  rw [Int.floor_neg]
-  sorry
+  suffices ⌈x⌉ = ⌊x⌋ + 1 by
+    have := congrArg (HMul.hMul (-1)) this
+    simp only [neg_mul, one_mul, neg_add_rev, add_comm] at this
+    exact this
+  have ⟨n, hn⟩ := h
+  have hn' : x ∈ Set.Ico ↑n (↑n + (1 : ℝ)) :=
+    Set.mem_of_subset_of_mem Set.Ioo_subset_Ico_self hn
+  rw [Int.ceil_eq_iff, Int.floor_eq_on_Ico n x hn']
+  simp only [Int.cast_add, Int.cast_one, add_sub_cancel]
+  apply And.intro
+  · exact (Set.mem_Ioo.mp hn).left
+  · exact le_of_lt (Set.mem_Ico.mp hn').right
 
 /-- ### Exercise 4c
 

Common/Real.lean

@@ -1,7 +1,6 @@
 import Common.Real.Basic
 import Common.Real.Function
 import Common.Real.Geometry
-import Common.Real.Int
 import Common.Real.Rational
 import Common.Real.Sequence
 import Common.Real.Set

Common/Real/Function/Step.lean

@@ -14,7 +14,7 @@ open Partition
 Any member of a subinterval of a partition `P` must also be a member of `P`.
 -/
 lemma mem_open_subinterval_imp_mem_partition {p : Partition}
-  (hI : I ∈ p.xs.pairwise (fun x₁ x₂ => i(x₁, x₂)))
+  (hI : I ∈ p.xs.pairwise (fun x₁ x₂ => Set.Ioo x₁ x₂))
   (hy : y ∈ I) : y ∈ p := by
   cases h : p.xs with
   | nil =>
@@ -50,7 +50,7 @@ structure Step where
   p : Partition
   f : ∀ x ∈ p, ℝ
   const_open_subintervals :
-    ∀ (hI : I ∈ p.xs.pairwise (fun x₁ x₂ => i(x₁, x₂))),
+    ∀ (hI : I ∈ p.xs.pairwise (fun x₁ x₂ => Set.Ioo x₁ x₂)),
       ∃ c : ℝ, ∀ (hy : y ∈ I),
         f y (mem_open_subinterval_imp_mem_partition hI hy) = c
 

Common/Real/Int.lean

@@ -1,15 +0,0 @@
-import Mathlib.Data.Real.Basic
-
-/-! # Common.Real.Int
-
-Additional theorems and definitions useful in the context of integers.
--/
-
-namespace Real
-
-/--
-Check whether a real number is an integer.
--/
-def isInt (x : ℝ) := x = Int.floor x
-
-end Real

Common/Real/Set.lean

@@ -1,3 +1,2 @@
 import Common.Real.Set.Basic
-import Common.Real.Set.Interval
 import Common.Real.Set.Partition

Common/Real/Set/Interval.lean

@@ -1,39 +0,0 @@
-import Mathlib.Data.Real.Basic
-
-/-! # Common.Real.Set.Interval
-
-A syntactic description of the various types of continuous intervals permitted
-on the real number line.
--/
-
-/--
-Representation of a closed interval.
--/
-syntax (priority := high) "i[" term "," term "]" : term
-
-macro_rules
-  | `(i[$a, $b]) => `({ z | $a ≤ z ∧ z ≤ $b })
-
-/--
-Representation of an open interval.
--/
-syntax (priority := high) "i(" term "," term ")" : term
-
-macro_rules
-  | `(i($a, $b)) => `({ z | $a < z ∧ z < $b })
-
-/--
-Representation of a left half-open interval.
--/
-syntax (priority := high) "i(" term "," term "]" : term
-
-macro_rules
-  | `(i($a, $b]) => `({ z | $a < z ∧ z ≤ $b })
-
-/--
-Representation of a right half-open interval.
--/
-syntax (priority := high) "i[" term "," term ")" : term
-
-macro_rules
-  | `(i[$a, $b)) => `({ z | $a ≤ z ∧ z < $b })

Common/Real/Set/Partition.lean

@@ -1,7 +1,7 @@
+import Mathlib.Data.Real.Basic
 import Mathlib.Data.List.Sort
 
 import Common.List.Basic
-import Common.Real.Set.Interval
 
 /-! # Common.Real.Set.Partition