Partially answer Apostol exercises I 3.12.

Include basic ideas around rational numbers.

one-variable-calculus/Apostol/Chapter_1_6.lean

@@ -138,8 +138,7 @@ If there exists some `k` satisfying the description in the above `def`, then `Q`
 is measurable.
 -/
 axiom exhaustion_exists_unique_imp_measurable (Q : Set ℝ²)
-  : (∃ k : ℝ, forall_subset_between_step_imp_le_between_area k Q ∧
+  : (∃! k : ℝ, forall_subset_between_step_imp_le_between_area k Q)
-      (∀ x : ℝ, forall_subset_between_step_imp_le_between_area x Q → x = k))
   → Q ∈ 𝓜
 
 /--

one-variable-calculus/Apostol/Exercises/Exercises_I_3_12.lean

@@ -3,6 +3,14 @@ Exercises I 3.12
 
 A Set of Axioms for the Real-Number System
 -/
+import Mathlib.Algebra.Order.Floor
+import Mathlib.Data.PNat.Basic
+import Mathlib.Data.Real.Basic
+import Mathlib.Data.Real.Sqrt
+import Mathlib.Tactic.LibrarySearch
+
+import Apostol.Chapter_I_3
+import Bookshelf.Real.Rational
 
 -- ========================================
 -- Exercise 1
@@ -11,7 +19,17 @@ A Set of Axioms for the Real-Number System
 -- at least one real `z` satisfying `x < z < y`.
 -- ========================================
 
--- # TODO
+example (x y : ℝ) (h : x < y) : ∃ z, x < z ∧ z < y := by
+  have ⟨z, hz⟩ := exists_pos_add_of_lt' h
+  refine ⟨x + z / 2, ⟨?_, ?_⟩⟩
+  · have hz' : z / 2 > 0 := by
+      have hr := div_lt_div_of_lt (show (0 : ℝ) < 2 by simp) hz.left
+      rwa [zero_div] at hr
+    exact (lt_add_iff_pos_right x).mpr hz'
+  · have hz' : z / 2 < z := div_lt_self hz.left (show 1 < 2 by norm_num)
+    calc x + z / 2
+      _ < x + z := (add_lt_add_iff_left x).mpr hz'
+      _ = y := hz.right
 
 -- ========================================
 -- Exercise 2
@@ -20,7 +38,8 @@ A Set of Axioms for the Real-Number System
 -- such that `m < x < n`.
 -- ========================================
 
--- # TODO
+example (x : ℝ) : ∃ m n : ℝ, m < x ∧ x < n := by
+  refine ⟨x - 1, ⟨x + 1, ⟨?_, ?_⟩⟩⟩ <;> norm_num
 
 -- ========================================
 -- Exercise 3
@@ -28,7 +47,12 @@ A Set of Axioms for the Real-Number System
 -- If `x > 0`, prove that there is a positive integer `n` such that `1 / n < x`.
 -- ========================================
 
--- # TODO
+example (x : ℝ) (h : x > 0) : ∃ n : ℕ+, 1 / n < x := by
+  have ⟨n, hn⟩ := @Real.exists_pnat_mul_self_geq_of_pos x 1 h
+  refine ⟨n, ?_⟩
+  have hr := mul_lt_mul_of_pos_right hn (show 0 < 1 / ↑↑n by norm_num)
+  conv at hr => arg 2; rw [mul_comm, ← mul_assoc]; simp
+  rwa [one_mul] at hr
 
 -- ========================================
 -- Exercise 4
@@ -39,7 +63,13 @@ A Set of Axioms for the Real-Number System
 -- `⌊5 / 2⌋ = 2`, `⌊-8/3⌋ = -3`.
 -- ========================================
 
--- # TODO
+example (x : ℝ) : ∃! n : ℤ, n ≤ x ∧ x < n + 1 := by
+  let n := Int.floor x
+  refine ⟨n, ⟨?_, ?_⟩⟩
+  · exact ⟨Int.floor_le x, Int.lt_floor_add_one x⟩
+  · intro y hy
+    rw [← Int.floor_eq_iff] at hy
+    exact Eq.symm hy
 
 -- ========================================
 -- Exercise 5
@@ -48,7 +78,19 @@ A Set of Axioms for the Real-Number System
 -- `n` which satisfies `x ≤ n < x + 1`.
 -- ========================================
 
--- # TODO
+example (x : ℝ) : ∃! n : ℤ, x ≤ n ∧ n < x + 1 := by
+  let n := Int.ceil x
+  refine ⟨n, ⟨?_, ?_⟩⟩
+  · exact ⟨Int.le_ceil x, Int.ceil_lt_add_one x⟩
+  · simp only
+    intro y hy
+    suffices y - 1 < x ∧ x ≤ y by
+      rw [← Int.ceil_eq_iff] at this
+      exact Eq.symm this
+    apply And.intro
+    · have := (sub_lt_sub_iff_right 1).mpr hy.right
+      rwa [add_sub_cancel] at this
+    · exact hy.left
 
 -- ========================================
 -- Exercise 6
@@ -59,7 +101,8 @@ A Set of Axioms for the Real-Number System
 -- are *dense* in the real-number system.
 -- ========================================
 
--- # TODO
+example (x y : ℝ) (h : x < y) : ∃ r : ℚ, x < r ∧ r < y := by
+  sorry
 
 -- ========================================
 -- Exercise 7
@@ -68,7 +111,25 @@ A Set of Axioms for the Real-Number System
 -- `xy`, `x / y`, and `y / x` are all irrational.
 -- ========================================
 
--- # TODO
+example (x : ℚ) (hx : x ≠ 0) (y : ℝ) (hy : irrational y)
+  : irrational (x + y) := by
+  sorry
+
+example (x : ℚ) (hx : x ≠ 0) (y : ℝ) (hy : irrational y)
+  : irrational (x - y) :=
+  sorry
+
+example (x : ℚ) (hx : x ≠ 0) (y : ℝ) (hy : irrational y)
+  : irrational (x * y) :=
+  sorry
+
+example (x : ℚ) (hx : x ≠ 0) (y : ℝ) (hy : irrational y)
+  : y ≠ 0 → irrational (x / y) :=
+  sorry
+
+example (x : ℚ) (hx : x ≠ 0) (y : ℝ) (hy : irrational y)
+  : irrational (y / x) :=
+  sorry
 
 -- ========================================
 -- Exercise 8
@@ -76,7 +137,10 @@ A Set of Axioms for the Real-Number System
 -- Is the sum or product of two irrational numbers always irrational?
 -- ========================================
 
--- # TODO
+-- No. Here is a counterexample.
+
+example (hx : x = Real.sqrt 2): irrational x ∧ rational (x * x) := by
+  sorry
 
 -- ========================================
 -- Exercise 9
@@ -86,7 +150,8 @@ A Set of Axioms for the Real-Number System
 -- infinitely many.
 -- ========================================
 
--- # TODO
+example (x y : ℝ) (h : x < y) : ∃ z : ℝ, irrational z ∧ x < z ∧ z < y := by
+  sorry
 
 -- ========================================
 -- Exercise 10
@@ -94,17 +159,46 @@ A Set of Axioms for the Real-Number System
 -- An integer `n` is called *even* if `n = 2m` for some integer `m`, and *odd*
 -- if `n + 1` is even. Prove the following statements:
 --
--- (a) An integer cannot be both even and odd.
--- (b) Every integer is either even or odd.
--- (c) The sum or product of two even integers is even. What can you say about
--- the sum or product of two odd integers?
--- (d) If `n²` is even, so is `n`. If `a² = 2b²`, where `a` and `b` are
--- integers, then both `a` and `b` are even.
 -- (e) Every rational number can be expressed in the form `a / b`, where `a` and
 -- `b` are integers, at least one of which is odd.
 -- ========================================
 
--- # TODO
+def is_even (n : ℤ) := ∃ m : ℤ, n = 2 * m
+
+def is_odd (n : ℤ) := is_even (n + 1)
+
+-- ----------------------------------------
+-- (a) An integer cannot be both even and odd.
+-- ----------------------------------------
+
+example (n : ℤ) : is_even n = ¬ is_odd n := sorry
+
+-- ----------------------------------------
+-- (b) Every integer is either even or odd.
+-- ----------------------------------------
+
+example (n : ℤ) : is_even n ∨ is_odd n := sorry
+
+-- ----------------------------------------
+-- (c) The sum or product of two even integers is even. What can you say about
+-- the sum or product of two odd integers?
+-- ----------------------------------------
+
+example (m n : ℤ) : is_even m ∧ is_even n → is_even (m * n) := sorry
+
+example (m n : ℤ) :
+  (∃ m n : ℤ, is_odd m ∧ is_odd n ∧ is_even (m * n)) ∧
+  (∃ m n : ℤ, is_odd m ∧ is_odd n ∧ is_odd (m * n)) :=
+  sorry
+
+-- ----------------------------------------
+-- (d) If `n²` is even, so is `n`. If `a² = 2b²`, where `a` and `b` are
+-- integers, then both `a` and `b` are even.
+-- ----------------------------------------
+
+example (n : ℤ) (h : is_even (n ^ 2)) : is_even n := sorry
+
+example (a b : ℤ) (h : a ^ 2 = 2 * b ^ 2) : is_even a ∧ is_even b := sorry
 
 -- ========================================
 -- Exercise 11
@@ -116,16 +210,27 @@ A Set of Axioms for the Real-Number System
 -- contradiction.]
 -- ========================================
 
--- # TODO
+example : ¬ ∃ n : ℝ, rational n → n ^ 2 = 2 := sorry
 
 -- ========================================
 -- Exercise 12
 --
 -- The Archimedean property of the real-number system was deduced as a
 -- consequence of the least-upper-bound axiom. Prove that the set of rational
--- numbers satisfies the Archimedean property but not he least-upper-bound
+-- numbers satisfies the Archimedean property but not the least-upper-bound
 -- property. This shows that the Archimedean property does not imply the
 -- least-upper-bound axiom.
 -- ========================================
 
--- # TODO
+/--
+Shows the set of rational numbers satisfies the Archimedean property.
+-/
+theorem exists_pnat_mul_self_geq_of_pos {x y : ℚ}
+  : x > 0 → ∃ n : ℕ+, n * x > y := sorry
+
+/--
+Show the Archimedean property does not imply the least-upper-bound axiom.
+-/
+example (S : Set ℚ) (hne : S.Nonempty) (hbdd : BddAbove S)
+  : ¬ ∃ x, IsLUB S x :=
+  sorry

shared/Bookshelf/Real.lean

@@ -1,5 +1,6 @@
 import Bookshelf.Real.Basic
 import Bookshelf.Real.Function
 import Bookshelf.Real.Geometry
+import Bookshelf.Real.Rational
 import Bookshelf.Real.Sequence
 import Bookshelf.Real.Set

shared/Bookshelf/Real/Rational.lean

@@ -0,0 +1,14 @@
+import Bookshelf.Real.Basic
+
+/--
+Assert that a real number is rational.
+
+Note this does *not* require the found rational to be in reduced form. Members
+of `ℚ` expect this (by proving the numerator and denominator are coprime).
+-/
+def rational (x : ℝ) := ∃ a : ℤ, ∃ b : ℕ, b ≠ 0 ∧ x = a / b
+
+/--
+Assert that a real number is irrational.
+-/
+def irrational (x : ℝ) := ¬ rational x