Apostol I 3.

Better organize concepts in `common` and continue adding more to parts
of I 3 proofs.

common/Common.lean

@@ -1,3 +1,3 @@
-import Common.Sequence.Arithmetic
+import Common.Data.Real.Set
-import Common.Sequence.Geometric
+import Common.Data.Real.Sequence
 import Common.Tuple

common/Common/Data/Real/Sequence.lean

@@ -115,3 +115,92 @@ theorem sum_recursive_closed (seq : Arithmetic) (n : Nat)
       _ = seq.sum_closed (n + 1) := rfl
 
 end Arithmetic
+
+/--
+A `0th`-indexed geometric sequence.
+-/
+structure Geometric where
+  a₀ : Real
+  r : Real
+
+namespace Geometric
+
+/--
+Returns the value of the `n`th term of a geometric sequence.
+
+This function calculates the value of this term directly. Keep in mind the
+sequence is `0`th-indexed.
+-/
+def termClosed (seq : Geometric) (n : Nat) : Real :=
+  seq.a₀ * seq.r ^ n
+
+/--
+Returns the value of the `n`th term of a geometric sequence.
+
+This function calculates the value of this term recursively. Keep in mind the
+sequence is `0`th-indexed.
+-/
+def termRecursive : Geometric → Nat → Real
+  | seq,       0 => seq.a₀
+  | seq, (n + 1) => seq.r * (seq.termRecursive n)
+
+/--
+The recursive and closed term definitions of a geometric sequence agree with
+one another.
+-/
+theorem term_recursive_closed (seq : Geometric) (n : Nat)
+  : seq.termRecursive n = seq.termClosed n := by
+  induction n with
+  | zero => unfold termClosed termRecursive; norm_num
+  | succ n ih => calc
+      seq.termRecursive (n + 1)
+      _ = seq.r * (seq.termRecursive n) := rfl
+      _ = seq.r * (seq.termClosed n) := by rw [ih]
+      _ = seq.r * (seq.a₀ * seq.r ^ n) := rfl
+      _ = seq.a₀ * seq.r ^ (n + 1) := by ring
+      _ = seq.termClosed (n + 1) := rfl
+
+/--
+The summation of the first `n + 1` terms of a geometric sequence.
+
+This function calculates the sum directly.
+-/
+noncomputable def sum_closed_ratio_neq_one (seq : Geometric) (n : Nat)
+  : seq.r ≠ 1 → Real :=
+  fun _ => (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r)
+
+/--
+The summation of the first `n + 1` terms of a geometric sequence.
+
+This function calculates the sum recursively.
+-/
+def sum_recursive : Geometric → Nat → Real
+  | seq,       0 => seq.a₀
+  | seq, (n + 1) => seq.termClosed (n + 1) + seq.sum_recursive n
+
+/--
+The recursive and closed definitions of the sum of a geometric sequence agree
+with one another.
+-/
+theorem sum_recursive_closed (seq : Geometric) (n : Nat) (p : seq.r ≠ 1)
+  : sum_recursive seq n = sum_closed_ratio_neq_one seq n p := by
+  have h : 1 - seq.r ≠ 0 := by
+    intro h
+    rw [sub_eq_iff_eq_add, zero_add] at h
+    exact False.elim (p (Eq.symm h))
+  induction n with
+  | zero =>
+    unfold sum_recursive sum_closed_ratio_neq_one
+    simp
+    rw [mul_div_assoc, div_self h, mul_one] 
+  | succ n ih =>
+    calc
+      sum_recursive seq (n + 1)
+      _ = seq.termClosed (n + 1) + seq.sum_recursive n := rfl
+      _ = seq.termClosed (n + 1) + sum_closed_ratio_neq_one seq n p := by rw [ih]
+      _ = seq.a₀ * seq.r ^ (n + 1) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := rfl
+      _ = seq.a₀ * seq.r ^ (n + 1) * (1 - seq.r) / (1 - seq.r) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := by rw [mul_div_cancel _ h]
+      _ = (seq.a₀ * (1 - seq.r ^ (n + 1 + 1))) / (1 - seq.r) := by ring_nf
+      _ = sum_closed_ratio_neq_one seq (n + 1) p := rfl
+
+end Geometric

common/Common/Data/Real/Sequence.tex

@@ -0,0 +1,35 @@
+\documentclass{article}
+
+\input{../../../preamble}
+
+\begin{document}
+
+\begin{theorem}[Sum of Arithmetic Series]
+
+  Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$.
+  Then for some $n \in \mathbb{N}$,
+  $$\sum_{i=0}^n a_i = \frac{(n + 1)(a_0 + a_n)}{2}.$$
+
+\end{theorem}
+
+\begin{proof}
+
+  \href{Sequence.lean}{Common.Data.Real.Sequence.Arithmetic.sum_recursive_closed}
+
+\end{proof}
+
+\begin{theorem}[Sum of Geometric Series]
+
+  Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$.
+  Then for some $n \in \mathbb{N}$,
+  $$\sum_{i=0}^n a_i = \frac{a_0(1 - r^{n+1})}{1 - r}.$$
+
+\end{theorem}
+
+\begin{proof}
+
+  \href{Sequence.lean}{Common.Data.Real.Sequence.Geometric.sum_recursive_closed}
+
+\end{proof}
+
+\end{document}

common/Common/Data/Real/Set.lean

@@ -0,0 +1,12 @@
+import Mathlib.Data.Real.Basic
+
+namespace Real
+
+/--
+The Minkowski sum of two sets `s` and `t` is the set
+`s + t = { a + b : a ∈ s, b ∈ t }`.
+-/
+def minkowski_sum (s t : Set ℝ) :=
+  { x | ∃ a ∈ s, ∃ b ∈ t, x = a + b }
+
+end Real

common/Common/Sequence/Arithmetic.tex

@@ -1,21 +0,0 @@
-\documentclass{article}
-
-\input{../../preamble}
-
-\begin{document}
-
-\begin{theorem}[Sum of Arithmetic Series]
-
-  Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$.
-  Then for some $n \in \mathbb{N}$,
-  $$\sum_{i=0}^n a_i = \frac{(n + 1)(a_0 + a_n)}{2}.$$
-
-\end{theorem}
-
-\begin{proof}
-
-  \href{Arithmetic.lean}{Common.Sequence.Arithmetic.sum_recursive_closed}
-
-\end{proof}
-
-\end{document}

common/Common/Sequence/Geometric.lean

@@ -1,92 +0,0 @@
-import Mathlib.Data.Real.Basic
-import Mathlib.Tactic.NormNum
-import Mathlib.Tactic.Ring
-
-/--
-A `0th`-indexed geometric sequence.
--/
-structure Geometric where
-  a₀ : Real
-  r : Real
-
-namespace Geometric
-
-/--
-Returns the value of the `n`th term of a geometric sequence.
-
-This function calculates the value of this term directly. Keep in mind the
-sequence is `0`th-indexed.
--/
-def termClosed (seq : Geometric) (n : Nat) : Real :=
-  seq.a₀ * seq.r ^ n
-
-/--
-Returns the value of the `n`th term of a geometric sequence.
-
-This function calculates the value of this term recursively. Keep in mind the
-sequence is `0`th-indexed.
--/
-def termRecursive : Geometric → Nat → Real
-  | seq,       0 => seq.a₀
-  | seq, (n + 1) => seq.r * (seq.termRecursive n)
-
-/--
-The recursive and closed term definitions of a geometric sequence agree with
-one another.
--/
-theorem term_recursive_closed (seq : Geometric) (n : Nat)
-  : seq.termRecursive n = seq.termClosed n := by
-  induction n with
-  | zero => unfold termClosed termRecursive; norm_num
-  | succ n ih => calc
-      seq.termRecursive (n + 1)
-      _ = seq.r * (seq.termRecursive n) := rfl
-      _ = seq.r * (seq.termClosed n) := by rw [ih]
-      _ = seq.r * (seq.a₀ * seq.r ^ n) := rfl
-      _ = seq.a₀ * seq.r ^ (n + 1) := by ring
-      _ = seq.termClosed (n + 1) := rfl
-
-/--
-The summation of the first `n + 1` terms of a geometric sequence.
-
-This function calculates the sum directly.
--/
-noncomputable def sum_closed_ratio_neq_one (seq : Geometric) (n : Nat)
-  : seq.r ≠ 1 → Real :=
-  fun _ => (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r)
-
-/--
-The summation of the first `n + 1` terms of a geometric sequence.
-
-This function calculates the sum recursively.
--/
-def sum_recursive : Geometric → Nat → Real
-  | seq,       0 => seq.a₀
-  | seq, (n + 1) => seq.termClosed (n + 1) + seq.sum_recursive n
-
-/--
-The recursive and closed definitions of the sum of a geometric sequence agree
-with one another.
--/
-theorem sum_recursive_closed (seq : Geometric) (n : Nat) (p : seq.r ≠ 1)
-  : sum_recursive seq n = sum_closed_ratio_neq_one seq n p := by
-  have h : 1 - seq.r ≠ 0 := by
-    intro h
-    rw [sub_eq_iff_eq_add, zero_add] at h
-    exact False.elim (p (Eq.symm h))
-  induction n with
-  | zero =>
-    unfold sum_recursive sum_closed_ratio_neq_one
-    simp
-    rw [mul_div_assoc, div_self h, mul_one] 
-  | succ n ih =>
-    calc
-      sum_recursive seq (n + 1)
-      _ = seq.termClosed (n + 1) + seq.sum_recursive n := rfl
-      _ = seq.termClosed (n + 1) + sum_closed_ratio_neq_one seq n p := by rw [ih]
-      _ = seq.a₀ * seq.r ^ (n + 1) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := rfl
-      _ = seq.a₀ * seq.r ^ (n + 1) * (1 - seq.r) / (1 - seq.r) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := by rw [mul_div_cancel _ h]
-      _ = (seq.a₀ * (1 - seq.r ^ (n + 1 + 1))) / (1 - seq.r) := by ring_nf
-      _ = sum_closed_ratio_neq_one seq (n + 1) p := rfl
-
-end Geometric

common/Common/Sequence/Geometric.tex

@@ -1,21 +0,0 @@
-\documentclass{article}
-
-\input{../../preamble}
-
-\begin{document}
-
-\begin{theorem}[Sum of Geometric Series]
-
-  Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$.
-  Then for some $n \in \mathbb{N}$,
-  $$\sum_{i=0}^n a_i = \frac{a_0(1 - r^{n+1})}{1 - r}.$$
-
-\end{theorem}
-
-\begin{proof}
-
-  \href{Geometric.lean}{Common.Sequence.Geometric.sum_recursive_closed}
-
-\end{proof}
-
-\end{document}

one-variable-calculus/Apostol/Chapter_I_3.lean

@@ -1,4 +1,6 @@
+import Common.Data.Real.Set
 import Mathlib.Data.Real.Basic
+import Mathlib.Data.Set.Basic
 import Mathlib.Data.Set.Pointwise.Basic
 import Mathlib.Tactic.LibrarySearch
 
@@ -7,6 +9,10 @@ import Mathlib.Tactic.LibrarySearch
 
 namespace Real
 
+-- ========================================
+-- The least-upper-bound axiom (completeness axiom)
+-- ========================================
+
 /--
 A property holds for the negation of elements in set `S` if and only if it also
 holds for the elements of the negation of `S`.
@@ -139,6 +145,10 @@ lemma leq_nat_abs_ceil_self (x : ℝ) : x ≤ Int.natAbs ⌈x⌉ := by
       _ ≤ 0 := le_of_lt (lt_of_not_le h)
       _ ≤ ↑(Int.natAbs ⌈x⌉) := GE.ge.le h'    
 
+-- ========================================
+-- The Archimedean property of the real-number system
+-- ========================================
+
 /--
 Theorem I.29
 
@@ -200,14 +210,75 @@ theorem forall_pnat_leq_self_leq_frac_imp_eq {x y a : ℝ}
       _ ≤ a + y / ↑↑n := (h n).right
     simp at this
 
+-- ========================================
+-- Fundamental properties of the supremum and infimum
+-- ========================================
+
+/--
+Every member of a set `S` is less than or equal to some value `ub` if and only
+if `ub` is an upper bound of `S`. 
+-/
+lemma mem_upper_bounds_iff_forall_le {S : Set ℝ}
+  : ub ∈ upperBounds S ↔ (∀ x, x ∈ S → x ≤ ub) := by
+  apply Iff.intro
+  · intro h _ hx
+    exact (h hx)
+  · exact id
+
+/--
+If a set `S` has a least upper bound, it follows every member of `S` is less
+than or equal to that value.
+-/
+lemma forall_lub_imp_forall_le {S : Set ℝ}
+  : IsLUB S ub → (∀ x, x ∈ S → x ≤ ub) := by
+  intro h
+  rw [← mem_upper_bounds_iff_forall_le]
+  exact h.left
+
 /--
 Theorem I.32a
 
 Let `h` be a given positive number and let `S` be a set of real numbers. If `S`
 has a supremum, then for some `x` in `S` we have `x > sup S - h`.
 -/
-theorem arb_close_to_sup (S : Set ℝ) (s h : ℝ) (hp : h > 0)
+theorem sup_imp_exists_gt_sup_sub_delta (S : Set ℝ) (s h : ℝ) (hp : h > 0)
-  : IsLUB S s → ∃ x : S, x > s - h := sorry
+  : IsLUB S s → ∃ x ∈ S, x > s - h := by
+  intro hb
+  -- Suppose all members of our set was less than `s - h`. Then `s` couldn't be
+  -- the *least* upper bound.
+  by_contra nb
+  suffices s - h ∈ upperBounds S by
+    have h' : h < h := calc h
+      _ ≤ 0 := (le_sub_self_iff s).mp (hb.right this)
+      _ < h := hp
+    simp at h'
+  rw [not_exists] at nb
+  have nb' : ∀ x ∈ S, x ≤ s - h := by
+    intro x hx
+    exact le_of_not_gt (not_and.mp (nb x) hx)
+  rw [← mem_upper_bounds_iff_forall_le] at nb'
+  exact nb'
+
+/--
+Every member of a set `S` is greater than or equal to some value `lb` if and
+only if `lb` is a lower bound of `S`. 
+-/
+lemma mem_lower_bounds_iff_forall_ge {S : Set ℝ}
+  : lb ∈ lowerBounds S ↔ (∀ x ∈ S, x ≥ lb) := by
+  apply Iff.intro
+  · intro h _ hx
+    exact (h hx)
+  · exact id
+
+/--
+If a set `S` has a greatest lower bound, it follows every member of `S` is
+greater than or equal to that value.
+-/
+lemma forall_glb_imp_forall_ge {S : Set ℝ}
+  : IsGLB S lb → (∀ x ∈ S, x ≥ lb) := by
+  intro h
+  rw [← mem_lower_bounds_iff_forall_ge]
+  exact h.left
 
 /--
 Theorem I.32b
@@ -215,7 +286,97 @@ Theorem I.32b
 Let `h` be a given positive number and let `S` be a set of real numbers. If `S`
 has an infimum, then for some `x` in `S` we have `x < inf S + h`.
 -/
-theorem arb_close_to_inf (S : Set ℝ) (s h : ℝ) (hp : h > 0)
+theorem inf_imp_exists_lt_inf_add_delta (S : Set ℝ) (s h : ℝ) (hp : h > 0)
-  : IsGLB S s → ∃ x : S, x < s + h := sorry
+  : IsGLB S s → ∃ x ∈ S, x < s + h := by
+  intro hb
+  -- Suppose all members of our set was greater than `s + h`. Then `s` couldn't
+  -- be the *greatest* lower bound.
+  by_contra nb
+  suffices s + h ∈ lowerBounds S by
+    have h' : h < h := calc h
+      _ ≤ 0 := (add_le_iff_nonpos_right s).mp (hb.right this)
+      _ < h := hp
+    simp at h'
+  rw [not_exists] at nb
+  have nb' : ∀ x ∈ S, x ≥ s + h := by
+    intro x hx
+    exact le_of_not_gt (not_and.mp (nb x) hx)
+  rw [← mem_lower_bounds_iff_forall_ge] at nb'
+  exact nb'
+
+/--
+Theorem I.33a (Additive Property)
+
+Given nonempty subsets `A` and `B` of `ℝ`, let `C` denote the set
+`C = {a + b : a ∈ A, b ∈ B}`. If each of `A` and `B` has a supremum, then `C`
+has a supremum, and `sup C = sup A + sup B`.
+-/
+theorem sup_minkowski_sum_eq_sup_add_sup (A B : Set ℝ) (a b : ℝ)
+  (hA : A.Nonempty) (hB : B.Nonempty)
+  (ha : IsLUB A a) (hb : IsLUB B b)
+  : IsLUB (Real.minkowski_sum A B) (a + b) := by
+  let C := Real.minkowski_sum A B
+  -- First we show `a + b` is an upper bound of `C`.
+  have hub : a + b ∈ upperBounds C := by
+    rw [mem_upper_bounds_iff_forall_le]
+    intro x hx
+    have ⟨a', ⟨ha', ⟨b', ⟨hb', hxab⟩⟩⟩⟩: ∃ a ∈ A, ∃ b ∈ B, x = a + b := hx
+    have hs₁ : a' ≤ a := (forall_lub_imp_forall_le ha) a' ha'
+    have hs₂ : b' ≤ b := (forall_lub_imp_forall_le hb) b' hb'
+    exact calc x
+      _ = a' + b' := hxab
+      _ ≤ a + b := add_le_add hs₁ hs₂
+  -- Now we show `a + b` is the *least* upper bound of `C`. If it wasn't, then
+  -- either `¬IsLUB A a` or `¬IsLUB B b`, a contradiction.
+  by_contra nub
+  have h : ¬IsLUB A a ∨ ¬IsLUB B b := by
+    sorry
+  cases h with
+  | inl na => exact absurd ha na
+  | inr nb => exact absurd hb nb
+
+/--
+Theorem I.33b (Additive Property)
+
+Given nonempty subsets `A` and `B` of `ℝ`, let `C` denote the set
+`C = {a + b : a ∈ A, b ∈ B}`. If each of `A` and `B` has an infimum, then `C`
+has an infimum, and `inf C = inf A + inf B`.
+-/
+theorem inf_minkowski_sum_eq_inf_add_inf (A B : Set ℝ)
+  (hA : A.Nonempty) (hB : B.Nonempty)
+  (ha : IsGLB A a) (hb : IsGLB B b)
+  : IsGLB (Real.minkowski_sum A B) (a + b) := by
+  let C := Real.minkowski_sum A B
+  -- First we show `a + b` is a lower bound of `C`.
+  have hub : a + b ∈ lowerBounds C := by
+    rw [mem_lower_bounds_iff_forall_ge]
+    intro x hx
+    have ⟨a', ⟨ha', ⟨b', ⟨hb', hxab⟩⟩⟩⟩: ∃ a ∈ A, ∃ b ∈ B, x = a + b := hx
+    have hs₁ : a' ≥ a := (forall_glb_imp_forall_ge ha) a' ha'
+    have hs₂ : b' ≥ b := (forall_glb_imp_forall_ge hb) b' hb'
+    exact calc x
+      _ = a' + b' := hxab
+      _ ≥ a + b := add_le_add hs₁ hs₂
+  -- Now we show `a + b` is the *greatest* lower bound of `C`. If it wasn't,
+  -- then either `¬IsGLB A a` or `¬IsGLB B b`, a contradiction.
+  by_contra nub
+  have h : ¬IsGLB A a ∨ ¬IsGLB B b := by
+    sorry
+  cases h with
+  | inl na => exact absurd ha na
+  | inr nb => exact absurd hb nb
+
+/--
+Theorem I.34
+
+Given two nonempty subsets `S` and `T` of `ℝ` such that `s ≤ t` for every `s` in
+`S` and every `t` in `T`. Then `S` has a supremum, and `T` has an infimum, and
+they satisfy the inequality `sup S ≤ inf T`.
+-/
+theorem forall_mem_le_forall_mem_imp_sup_le_inf (S T : Set ℝ)
+  (hS : S.Nonempty) (hT : T.Nonempty)
+  (p : ∀ s ∈ S, ∀ t ∈ T, s ≤ t)
+  : ∃ (s : ℝ), IsLUB S s ∧ ∃ (t : ℝ), IsGLB T t ∧ s ≤ t := by
+  sorry
 
 end Real

one-variable-calculus/Apostol/Chapter_I_3.tex

@@ -74,10 +74,51 @@
   \  % Force space prior to *Proof.*
 
   \begin{enumerate}[(a)]
-    \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.arb_close_to_sup}
+    \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.sup_imp_exists_gt_sup_sub_delta}
-    \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.arb_close_to_inf}
+    \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.inf_imp_exists_lt_inf_add_delta}
   \end{enumerate}
 
 \end{proof}
 
+\begin{xtheorem}{I.33}[Additive Property]
+
+  Given nonempty subsets $A$ and $B$ of $\mathbb{R}$, let $C$ denote the set
+  $$C = \{a + b : a \in A, b \in B\}.$$
+
+  \begin{enumerate}[(a)]
+    \item If each of $A$ and $B$ has a supremum, then $C$ has a supremum, and
+      $$\sup{C} = \sup{A} + \sup{B}.$$
+    \item If each of $A$ and $B$ has an infimum, then $C$ has an infimum, and
+      $$\inf{C} = \inf{A} + \inf{B}.$$
+  \end{enumerate}
+
+\end{xtheorem}
+
+\begin{proof}
+
+  \  % Force space prior to *Proof.*
+
+  \begin{enumerate}[(a)]
+    \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.sup_minkowski_sum_eq_sup_add_sup}
+    \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.inf_minkowski_sum_eq_inf_add_inf}
+  \end{enumerate}
+
+\end{proof}
+
+\begin{xtheorem}{I.34}
+
+  Given two nonempty subsets $S$ and $T$ of $\mathbb{R}$ such that
+  $$s \leq t$$
+  for every $s$ in $S$ and every $t$ in $T$. Then $S$ has a supremum, and $T$
+  has an infimum, and they satisfy the inequality
+  $$\sup{S} \leq \inf{T}.$$
+
+\end{xtheorem}
+
+\begin{proof}
+
+  \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.forall_mem_le_forall_mem_imp_sup_le_inf}
+
+\end{proof}
+
 \end{document}