Equivalence of reals

Analysis I, Chapter 5 epilogue: Isomorphism with the Mathlib real numbers

In this (technical) epilogue, we show that the "Chapter 5" real numbers Chapter5.Real : TypeChapter5.Real are isomorphic in various standard senses to the standard real numbers ℝ : Typeℝ. This we do by matching both structures with Dedekind cuts of the (Mathlib) rational numbers ℚ : Typeℚ.

From this point onwards, Chapter5.Real : TypeChapter5.Real will be deprecated, and we will use the standard real numbers ℝ : Typeℝ instead. In particular, one should use the full Mathlib API for ℝ : Typeℝ for all subsequent chapters, in lieu of the Chapter5.Real : TypeChapter5.Real API.

Filling the sorries here requires both the Chapter5.Real API and the Mathlib API for the standard natural numbers ℝ : Typeℝ. As such, they are excellent exercises to prepare you for the aforementioned transition.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

  • (Add tip here)

namespace Chapter5structure DedekindCut where E : Set ℚ nonempty : E.Nonempty bounded : BddAbove E lower: IsLowerSet E nomax : ∀ q ∈ E, ∃ r ∈ E, r > qtheorem isLowerSet_iff (E: Set ℚ) : IsLowerSet E ↔ ∀ q r, r < q → q ∈ E → r ∈ E := isLowerSet_iff_forall_ltabbrev Real.toSet_Rat (x:Real) : Set ℚ := { q | (q:Real) < x }lemma declaration uses 'sorry'Real.toSet_Rat_nonempty (x:Real) : x.toSet_Rat.Nonempty := x:Real⊢ x.toSet_Rat.Nonempty All goals completed! 🐙lemma declaration uses 'sorry'Real.toSet_Rat_bounded (x:Real) : BddAbove x.toSet_Rat := x:Real⊢ BddAbove x.toSet_Rat All goals completed! 🐙lemma declaration uses 'sorry'Real.toSet_Rat_lower (x:Real) : IsLowerSet x.toSet_Rat := x:Real⊢ IsLowerSet x.toSet_Rat All goals completed! 🐙lemma declaration uses 'sorry'Real.toSet_Rat_nomax {x:Real} : ∀ q ∈ x.toSet_Rat, ∃ r ∈ x.toSet_Rat, r > q := x:Real⊢ ∀ q ∈ x.toSet_Rat, ∃ r ∈ x.toSet_Rat, r > q All goals completed! 🐙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 nomax := x.toSet_Rat_nomax }abbrev DedekindCut.toSet_Real (c: DedekindCut) : Set Real := (fun (q:ℚ) ↦ (q:Real)) '' c.Elemma declaration uses 'sorry'DedekindCut.toSet_Real_nonempty (c: DedekindCut) : c.toSet_Real.Nonempty := c:DedekindCut⊢ c.toSet_Real.Nonempty All goals completed! 🐙lemma declaration uses 'sorry'DedekindCut.toSet_Real_bounded (c: DedekindCut) : BddAbove c.toSet_Real := c:DedekindCut⊢ BddAbove c.toSet_Real All goals completed! 🐙noncomputable abbrev DedekindCut.toReal (c: DedekindCut) : Real := sSup c.toSet_Reallemma DedekindCut.toReal_isLUB (c: DedekindCut) : IsLUB c.toSet_Real c.toReal := ExtendedReal.sSup_of_bounded c.toSet_Real_nonempty c.toSet_Real_boundednoncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'Real.equivCut : Real ≃ DedekindCut where toFun := toCut invFun := DedekindCut.toReal left_inv x := x:Real⊢ x.toCut.toReal = x All goals completed! 🐙 right_inv c := c:DedekindCut⊢ c.toReal.toCut = c All goals completed! 🐙end Chapter5

Now to develop analogous results for the Mathlib reals.

abbrev Real.toSet_Rat (x:ℝ) : Set ℚ := { q | (q:ℝ) < x }
lemma declaration uses 'sorry'Real.toSet_Rat_nonempty (x:ℝ) : x.toSet_Rat.Nonempty := x:ℝ⊢ x.toSet_Rat.Nonempty All goals completed! 🐙lemma declaration uses 'sorry'Real.toSet_Rat_bounded (x:ℝ) : BddAbove x.toSet_Rat := x:ℝ⊢ BddAbove x.toSet_Rat All goals completed! 🐙lemma declaration uses 'sorry'Real.toSet_Rat_lower (x:ℝ) : IsLowerSet x.toSet_Rat := x:ℝ⊢ IsLowerSet x.toSet_Rat All goals completed! 🐙lemma declaration uses 'sorry'Real.toSet_Rat_nomax (x:ℝ) : ∀ q ∈ x.toSet_Rat, ∃ r ∈ x.toSet_Rat, r > q := x:ℝ⊢ ∀ q ∈ x.toSet_Rat, ∃ r ∈ x.toSet_Rat, r > q All goals completed! 🐙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 nomax := x.toSet_Rat_nomax }namespace Chapter5abbrev DedekindCut.toSet_R (c: DedekindCut) : Set ℝ := (fun (q:ℚ) ↦ (q:ℝ)) '' c.Elemma declaration uses 'sorry'DedekindCut.toSet_R_nonempty (c: DedekindCut) : c.toSet_R.Nonempty := c:DedekindCut⊢ c.toSet_R.Nonempty All goals completed! 🐙lemma declaration uses 'sorry'DedekindCut.toSet_R_bounded (c: DedekindCut) : BddAbove c.toSet_R := c:DedekindCut⊢ BddAbove c.toSet_R All goals completed! 🐙noncomputable abbrev DedekindCut.toR (c: DedekindCut) : ℝ := sSup c.toSet_Rlemma DedekindCut.toR_isLUB (c: DedekindCut) : IsLUB c.toSet_R c.toR := isLUB_csSup c.toSet_R_nonempty c.toSet_R_boundedend Chapter5noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'Real.equivCut : ℝ ≃ Chapter5.DedekindCut where toFun := _root_.Real.toCut invFun := Chapter5.DedekindCut.toR left_inv x := x:ℝ⊢ x.toCut.toR = x All goals completed! 🐙 right_inv c := c:Chapter5.DedekindCut⊢ c.toR.toCut = c All goals completed! 🐙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 := x:Realy:ℝ⊢ y = equivR x ↔ y.toCut = x.toCut x:Realy:ℝ⊢ _root_.Real.equivCut y = equivCut x ↔ y.toCut = x.toCut All goals completed! 🐙

The isomorphism preserves order and ring operations

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Real.equivR_ordered_ring : Real ≃+*o ℝ where toEquiv := equivR map_add' := ⊢ ∀ (x y : Real), equivR.toFun (x + y) = equivR.toFun x + equivR.toFun y All goals completed! 🐙 map_mul' := ⊢ ∀ (x y : Real), equivR.toFun (x * y) = equivR.toFun x * equivR.toFun y All goals completed! 🐙 map_le_map_iff' := ⊢ ∀ {a b : Real}, equivR.toFun a ≤ equivR.toFun b ↔ a ≤ b All goals completed! 🐙
theorem declaration uses 'sorry'Real.pow_of_equivR (x:Real) (n:ℕ) : equivR (x^n) = (equivR x)^n := x:Realn:ℕ⊢ equivR (x ^ n) = equivR x ^ n All goals completed! 🐙theorem declaration uses 'sorry'Real.zpow_of_equivR (x:Real) (n:ℤ) : equivR (x^n) = (equivR x)^n := x:Realn:ℤ⊢ equivR (x ^ n) = equivR x ^ n All goals completed! 🐙theorem declaration uses 'sorry'Real.ratPow_of_equivR (x:Real) (q:ℚ) : equivR (x^q) = (equivR x)^(q:ℝ) := x:Realq:ℚ⊢ equivR (x ^ q) = equivR x ^ ↑q All goals completed! 🐙end Chapter5