add chapter 5 epilogue

README.md

@@ -38,7 +38,7 @@ In order to align the formalization with Mathlib conventions, a small number of
   - Section 5.3: Construction of the real numbers ([Verso page](https://teorth.github.io/analysis/sec53/)) ([Documentation](https://teorth.github.io/analysis/docs/Analysis/Section_5_3.html)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_5_3.lean))
   - Section 5.4: Ordering the reals ([Verso page](https://teorth.github.io/analysis/sec54/)) ([Documentation](https://teorth.github.io/analysis/docs/Analysis/Section_5_4.html)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_5_4.lean))
   - Section 5.5: The least upper bound property (_Verso page_) ([Documentation](https://teorth.github.io/analysis/docs/Analysis/Section_5_5.html)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_5_5.lean))
-  - Chapter 5 epilogue: Isomorphism with the Mathlib real numbers (planned)
+  - Chapter 5 epilogue: Isomorphism with the Mathlib real numbers  (_Verso page_) ([Documentation](https://teorth.github.io/analysis/docs/Analysis/Section_5_epilogue.html)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_5_epilogue.lean))
 - Chapter 6: Limits of sequences
   - _Section 6.1: Convergence and limit laws (planned)_
   - _Section 6.2: The extended real number system (planned)_

analysis/Analysis.lean

@@ -11,3 +11,4 @@ import Analysis.Section_5_2
 import Analysis.Section_5_3
 import Analysis.Section_5_4
 import Analysis.Section_5_5
+import Analysis.Section_5_epilogue

analysis/Analysis/Section_2_epilogue.lean

@@ -6,7 +6,6 @@ import Analysis.Section_2_3
 
 In this (technical) epilogue, we show that the "Chapter 2" natural numbers `Chapter2.Nat` are isomorphic in various standard senses to the standard natural numbers `ℕ`.
 
-
 From this point onwards, `Chapter2.Nat` will be deprecated, and we will use the standard natural numbers `ℕ` instead.  In particular, one should use the full Mathlib API for `ℕ` for all subsequent chapters, in lieu of the `Chapter2.Nat` API.
 
 Filling the sorries here requires both the Chapter2.Nat API and the Mathlib API for the standard natural numbers `ℕ`.  As such, they are excellent exercises to prepare you for the aforementioned transition.

analysis/Analysis/Section_5_5.lean

@@ -353,5 +353,6 @@ noncomputable instance Real.inst_SupSet : SupSet Real where
 noncomputable instance Real.inst_conditionallyCompleteLattice : ConditionallyCompleteLattice Real := conditionallyCompleteLatticeOfsSup Real (fun _ _ ↦ Set.Finite.bddAbove (by norm_num)) (fun _ _ ↦ Set.Finite.bddBelow (by norm_num))
 (by intro E hbound hnon; exact ExtendedReal.sup_of_bounded hnon hbound)
 
+theorem ExtendedReal.sSup_of_bounded {E: Set Real} (hnon: E.Nonempty) (hb: BddAbove E) : IsLUB E (sSup E) := sup_of_bounded hnon hb
 
 end Chapter5

analysis/Analysis/Section_5_epilogue.lean

@@ -0,0 +1,119 @@
+import Mathlib.Tactic
+import Analysis.Section_5_5
+
+/-!
+# Analysis I, Chapter 5 epilogue
+
+In this (technical) epilogue, we show that the "Chapter 5" real numbers `Chapter5.Real` are isomorphic in various standard senses to the standard real numbers `ℝ`.  This we do by matching both structures with Dedekind cuts of the (Mathlib) rational numbers `ℚ`.
+
+From this point onwards, `Chapter5.Real` will be deprecated, and we will use the standard real numbers `ℝ` instead.  In particular, one should use the full Mathlib API for `ℝ` for all subsequent chapters, in lieu of the `Chapter5.Real` API.
+
+Filling the sorries here requires both the Chapter5.Real API and the Mathlib API for the standard natural numbers `ℝ`.  As such, they are excellent exercises to prepare you for the aforementioned transition.
+
+--/
+
+namespace Chapter5
+
+structure DedekindCut where
+  E : Set ℚ
+  nonempty : E.Nonempty
+  bounded : BddAbove E
+  lower: IsLowerSet E
+
+abbrev Real.toSet_Rat (x:Real) : Set ℚ := { q | (q:Real) ≤ x }
+
+lemma Real.toSet_Rat_nonempty (x:Real) : x.toSet_Rat.Nonempty := by sorry
+
+lemma Real.toSet_Rat_bounded (x:Real) : BddAbove x.toSet_Rat := by sorry
+
+lemma Real.toSet_Rat_lower (x:Real) : IsLowerSet x.toSet_Rat := by sorry
+
+abbrev Real.toCut (x:Real) : DedekindCut :=
+ {
+   E := x.toSet_Rat
+   nonempty := x.toSet_Rat_nonempty
+   bounded := x.toSet_Rat_bounded
+   lower := x.toSet_Rat_lower
+ }
+
+abbrev DedekindCut.toSet_Real (c: DedekindCut) : Set Real := (fun (q:ℚ) ↦ (q:Real)) '' c.E
+
+lemma DedekindCut.toSet_Real_nonempty (c: DedekindCut) : c.toSet_Real.Nonempty := by sorry
+
+lemma DedekindCut.toSet_Real_bounded (c: DedekindCut) : BddAbove c.toSet_Real := by sorry
+
+noncomputable abbrev DedekindCut.toReal (c: DedekindCut) : Real := sSup c.toSet_Real
+
+lemma DedekindCut.toReal_isLUB (c: DedekindCut) : IsLUB c.toSet_Real c.toReal := ExtendedReal.sSup_of_bounded c.toSet_Real_nonempty c.toSet_Real_bounded
+
+noncomputable abbrev Real.equivCut : Real ≃ DedekindCut where
+  toFun := Real.toCut
+  invFun := DedekindCut.toReal
+  left_inv x := by
+    sorry
+  right_inv c := by
+    sorry
+
+end Chapter5
+
+/-- Now to develop analogous results for the Mathlib reals. -/
+
+abbrev Real.toSet_Rat (x:ℝ) : Set ℚ := { q | (q:ℝ) ≤ x }
+
+lemma Real.toSet_Rat_nonempty (x:ℝ) : x.toSet_Rat.Nonempty := by sorry
+
+lemma Real.toSet_Rat_bounded (x:ℝ) : BddAbove x.toSet_Rat := by sorry
+
+lemma Real.toSet_Rat_lower (x:ℝ) : IsLowerSet x.toSet_Rat := by sorry
+
+abbrev Real.toCut (x:ℝ) : Chapter5.DedekindCut :=
+ {
+   E := x.toSet_Rat
+   nonempty := x.toSet_Rat_nonempty
+   bounded := x.toSet_Rat_bounded
+   lower := x.toSet_Rat_lower
+ }
+
+namespace Chapter5
+
+abbrev DedekindCut.toSet_R (c: DedekindCut) : Set ℝ := (fun (q:ℚ) ↦ (q:ℝ)) '' c.E
+
+lemma DedekindCut.toSet_R_nonempty (c: DedekindCut) : c.toSet_R.Nonempty := by sorry
+
+lemma DedekindCut.toSet_R_bounded (c: DedekindCut) : BddAbove c.toSet_R := by sorry
+
+noncomputable abbrev DedekindCut.toR (c: DedekindCut) : ℝ := sSup c.toSet_R
+
+lemma DedekindCut.toR_isLUB (c: DedekindCut) : IsLUB c.toSet_R c.toR := isLUB_csSup c.toSet_R_nonempty c.toSet_R_bounded
+
+end Chapter5
+
+noncomputable abbrev Real.equivCut : ℝ ≃ Chapter5.DedekindCut where
+  toFun := _root_.Real.toCut
+  invFun := Chapter5.DedekindCut.toR
+  left_inv x := by
+    sorry
+  right_inv c := by
+    sorry
+
+namespace Chapter5
+
+/-- The isomorphism between the Chapter 5 reals and the Mathlib reals. -/
+noncomputable abbrev Real.equivR : Real ≃ ℝ := Real.equivCut.trans _root_.Real.equivCut.symm
+
+lemma Real.equivR_iff (x : Real) (y : ℝ) : y = Real.equivR x ↔ y.toCut = x.toCut := by
+  simp only [equivR, Equiv.trans_apply, ←Equiv.apply_eq_iff_eq_symm_apply]
+  rfl
+
+/-- The isomorphism preserves order -/
+noncomputable abbrev Real.equivR_order : Real ≃o ℝ where
+  toEquiv := equivR
+  map_rel_iff' := by sorry
+
+/-- The isomorphism preserves ring operations -/
+noncomputable abbrev Real.equivR_ring : Real ≃+* ℝ where
+  toEquiv := equivR
+  map_add' := by sorry
+  map_mul' := by sorry
+
+end Chapter5