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 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.

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)

structure Chapter5.DedekindCut : Type

• E : Set ℚ
• nonempty : self.E.Nonempty
• bounded : BddAbove self.E
• lower : IsLowerSet self.E
• nomax (q : ℚ) : q ∈ self.E → ∃ r ∈ self.E, r > q

theorem Chapter5.isLowerSet_iff (E : Set ℚ) : IsLowerSet E ↔ ∀ (q r : ℚ), r < q → q ∈ E → r ∈ E

@[reducible, inline]

abbrev Chapter5.Real.toSet_Rat (x : Real) : Set ℚ

Equations

• x.toSet_Rat = {q : ℚ | ↑q < x}

theorem Chapter5.Real.toSet_Rat_nonempty (x : Real) : x.toSet_Rat.Nonempty

theorem Chapter5.Real.toSet_Rat_bounded (x : Real) : BddAbove x.toSet_Rat

theorem Chapter5.Real.toSet_Rat_lower (x : Real) : IsLowerSet x.toSet_Rat

theorem Chapter5.Real.toSet_Rat_nomax {x : Real} (q : ℚ) : q ∈ x.toSet_Rat → ∃ r ∈ x.toSet_Rat, r > q

@[reducible, inline]

abbrev Chapter5.Real.toCut (x : Real) : DedekindCut

Equations

• x.toCut = { E := x.toSet_Rat, nonempty := ⋯, bounded := ⋯, lower := ⋯, nomax := ⋯ }

@[reducible, inline]

abbrev Chapter5.DedekindCut.toSet_Real (c : DedekindCut) : Set Real

Equations

• c.toSet_Real = (fun (q : ℚ) => ↑q) '' c.E

theorem Chapter5.DedekindCut.toSet_Real_nonempty (c : DedekindCut) : c.toSet_Real.Nonempty

theorem Chapter5.DedekindCut.toSet_Real_bounded (c : DedekindCut) : BddAbove c.toSet_Real

@[reducible, inline]

noncomputable abbrev Chapter5.DedekindCut.toReal (c : DedekindCut) : Real

Equations

• c.toReal = sSup c.toSet_Real

theorem Chapter5.DedekindCut.toReal_isLUB (c : DedekindCut) : IsLUB c.toSet_Real c.toReal

@[reducible, inline]

noncomputable abbrev Chapter5.Real.equivCut : Real ≃ DedekindCut

Equations

• Chapter5.Real.equivCut = { toFun := Chapter5.Real.toCut, invFun := Chapter5.DedekindCut.toReal, left_inv := Chapter5.Real.equivCut._proof_1, right_inv := Chapter5.Real.equivCut._proof_2 }

@[reducible, inline]

abbrev Real.toSet_Rat (x : ℝ) : Set ℚ

Now to develop analogous results for the Mathlib reals.

Equations

• x.toSet_Rat = {q : ℚ | ↑q < x}

theorem Real.toSet_Rat_nonempty (x : ℝ) : x.toSet_Rat.Nonempty

theorem Real.toSet_Rat_bounded (x : ℝ) : BddAbove x.toSet_Rat

theorem Real.toSet_Rat_lower (x : ℝ) : IsLowerSet x.toSet_Rat

theorem Real.toSet_Rat_nomax (x : ℝ) (q : ℚ) : q ∈ x.toSet_Rat → ∃ r ∈ x.toSet_Rat, r > q

@[reducible, inline]

abbrev Real.toCut (x : ℝ) : Chapter5.DedekindCut

Equations

• x.toCut = { E := x.toSet_Rat, nonempty := ⋯, bounded := ⋯, lower := ⋯, nomax := ⋯ }

@[reducible, inline]

abbrev Chapter5.DedekindCut.toSet_R (c : DedekindCut) : Set ℝ

Equations

• c.toSet_R = (fun (q : ℚ) => ↑q) '' c.E

theorem Chapter5.DedekindCut.toSet_R_nonempty (c : DedekindCut) : c.toSet_R.Nonempty

theorem Chapter5.DedekindCut.toSet_R_bounded (c : DedekindCut) : BddAbove c.toSet_R

@[reducible, inline]

noncomputable abbrev Chapter5.DedekindCut.toR (c : DedekindCut) : ℝ

Equations

• c.toR = sSup c.toSet_R

theorem Chapter5.DedekindCut.toR_isLUB (c : DedekindCut) : IsLUB c.toSet_R c.toR

@[reducible, inline]

noncomputable abbrev Real.equivCut : ℝ ≃ Chapter5.DedekindCut

Equations

• Real.equivCut = { toFun := Real.toCut, invFun := Chapter5.DedekindCut.toR, left_inv := Real.equivCut._proof_1, right_inv := Real.equivCut._proof_2 }

@[reducible, inline]

noncomputable abbrev Chapter5.Real.equivR : Real ≃ ℝ

The isomorphism between the Chapter 5 reals and the Mathlib reals.

Equations

• Chapter5.Real.equivR = Chapter5.Real.equivCut.trans Real.equivCut.symm

theorem Chapter5.Real.equivR_iff (x : Real) (y : ℝ) : y = equivR x ↔ y.toCut = x.toCut

@[reducible, inline]

noncomputable abbrev Chapter5.Real.equivR_ordered_ring : Real ≃+*o ℝ

The isomorphism preserves order and ring operations

Equations

• One or more equations did not get rendered due to their size.

theorem Chapter5.Real.pow_of_equivR (x : Real) (n : ℕ) : equivR (x ^ n) = equivR x ^ n

theorem Chapter5.Real.zpow_of_equivR (x : Real) (n : ℤ) : equivR (x ^ n) = equivR x ^ n

theorem Chapter5.Real.ratPow_of_equivR (x : Real) (q : ℚ) : equivR (x ^ q) = equivR x ^ ↑q