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 Chapter5@[ext] structure 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! 🐙-- In order to use this definition, we need some machinery ----- -- We start by showing it works for ratCasts theorem declaration uses 'sorry'Real.equivR_ratCast {q: ℚ} : equivR q = (q: ℝ) := q:ℚ⊢ equivR ↑q = ↑q All goals completed! 🐙lemma Real.equivR_nat {n: ℕ} : equivR n = (n: ℝ) := equivR_ratCastlemma Real.equivR_int {n: ℤ} : equivR n = (n: ℝ) := equivR_ratCast---- -- We then want to set up a way to convert from the Real `LIM` to the ℝ `Real.mk` -- To do this we need a few things: -- Convertion between the notions of Cauchy Sequences theorem declaration uses 'sorry'Sequence.IsCauchy.to_IsCauSeq {a: ℕ → ℚ} (ha: IsCauchy a) : IsCauSeq _root_.abs a := a:ℕ → ℚha:(↑a).IsCauchy⊢ IsCauSeq _root_.abs a All goals completed! 🐙-- Convertion of an `IsCauchy` to a `CauSeq` abbrev Sequence.IsCauchy.CauSeq {a: ℕ → ℚ} : (ha: IsCauchy a) → CauSeq ℚ _root_.abs := (⟨a, ·.to_IsCauSeq⟩)-- We then set up the conversion from Sequence.Equiv to CauSeq.LimZero because -- it is the equivalence relation example {a b: CauSeq ℚ abs} : a ≈ b ↔ CauSeq.LimZero (a - b) := a:CauSeq ℚ absb:CauSeq ℚ abs⊢ a ≈ b ↔ (a - b).LimZero All goals completed! 🐙theorem declaration uses 'sorry'Sequence.Equiv.LimZero {a b: ℕ → ℚ} (ha: IsCauchy a) (hb: IsCauchy b) (h:Equiv a b) : CauSeq.LimZero (ha.CauSeq - hb.CauSeq) := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyh:Equiv a b⊢ (ha.CauSeq - hb.CauSeq).LimZero All goals completed! 🐙-- We can now use it to convert between different functions in Real.mk theorem Real.mk_eq_mk {a b: ℕ → ℚ} (ha : Sequence.IsCauchy a) (hb : Sequence.IsCauchy b) (hab: Sequence.Equiv a b) : Real.mk ha.CauSeq = Real.mk hb.CauSeq := Real.mk_eq.mpr (hab.LimZero ha hb)-- Both directions of the equivalence theorem declaration uses 'sorry'Sequence.Equiv_iff_LimZero {a b: ℕ → ℚ} (ha: IsCauchy a) (hb: IsCauchy b) : Equiv a b ↔ CauSeq.LimZero (ha.CauSeq - hb.CauSeq) := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ Equiv a b ↔ (ha.CauSeq - hb.CauSeq).LimZero a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ (ha.CauSeq - hb.CauSeq).LimZero → Equiv a b All goals completed! 🐙---- -- We create some cauchy sequences with useful properties -- We show that for any sequence, it will eventually be arbitrarily close to its LIM open Real in theorem declaration uses 'sorry'Sequence.difference_approaches_zero {a: ℕ → ℚ} (ha: Sequence.IsCauchy a) : ∀ε > 0, ∃N, ∀n ≥ N, |LIM a - a n| ≤ (ε: ℚ) := a:ℕ → ℚha:(↑a).IsCauchy⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, |LIM a - ↑(a n)| ≤ ↑ε All goals completed! 🐙-- There exists a Cauchy sequence entirely above the LIM theorem declaration uses 'sorry'Real.exists_equiv_above {a: ℕ → ℚ} (ha: Sequence.IsCauchy a) : ∃(b: ℕ → ℚ), Sequence.IsCauchy b ∧ Sequence.Equiv a b ∧ ∀n, LIM a ≤ b n := a:ℕ → ℚha:(↑a).IsCauchy⊢ ∃ b, (↑b).IsCauchy ∧ Sequence.Equiv a b ∧ ∀ (n : ℕ), LIM a ≤ ↑(b n) All goals completed! 🐙-- There exists a Cauchy sequence entirely below the LIM theorem declaration uses 'sorry'Real.exists_equiv_below {a: ℕ → ℚ} (ha: Sequence.IsCauchy a) : ∃(b: ℕ → ℚ), Sequence.IsCauchy b ∧ Sequence.Equiv a b ∧ ∀n, b n ≤ LIM a := a:ℕ → ℚha:(↑a).IsCauchy⊢ ∃ b, (↑b).IsCauchy ∧ Sequence.Equiv a b ∧ ∀ (n : ℕ), ↑(b n) ≤ LIM a All goals completed! 🐙
Real.mk_le {f g : CauSeq ℚ abs} : Real.mk f ≤ Real.mk g ↔ f ≤ g
Real.mk_le_of_forall_le {f : CauSeq ℚ abs} {x : ℝ} (h : ∃ i, ∀ j ≥ i, ↑(↑f j) ≤ x) : Real.mk f ≤ x
Real.mk_const {x : ℚ} : Real.mk (CauSeq.const abs x) = ↑x
-- Transform a `Real` to an `ℝ` by going through Cauchy Sequences -- we can use the conversion of Real.mk_eq to use different sequences to show different parts theorem declaration uses 'sorry'Real.equivR_eq' {a: ℕ → ℚ} (ha: Sequence.IsCauchy a) : (LIM a).equivR = Real.mk ha.CauSeq := a:ℕ → ℚha:(↑a).IsCauchy⊢ equivR (LIM a) = Real.mk ha.CauSeq a:ℕ → ℚha:(↑a).IsCauchyhq:∃ q, ↑q = LIM a⊢ equivR (LIM a) = Real.mk ha.CauSeqa:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM a⊢ equivR (LIM a) = Real.mk ha.CauSeq a:ℕ → ℚha:(↑a).IsCauchyhq:∃ q, ↑q = LIM a⊢ equivR (LIM a) = Real.mk ha.CauSeq All goals completed! 🐙 a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM a⊢ sSup (Rat.cast '' (LIM a).toSet_Rat) = Real.mk ha.CauSeq a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM a⊢ Real.mk ha.CauSeq ∈ upperBounds (Rat.cast '' (LIM a).toSet_Rat)a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM a⊢ Real.mk ha.CauSeq ∈ lowerBounds (upperBounds (Rat.cast '' (LIM a).toSet_Rat)) a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM a⊢ Real.mk ha.CauSeq ∈ upperBounds (Rat.cast '' (LIM a).toSet_Rat) -- show that `Real.mk ha.CauSeq` is an upper bound a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM aa✝:ℝhy:a✝ ∈ Rat.cast '' (LIM a).toSet_Rat⊢ a✝ ≤ Real.mk ha.CauSeq a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM aa✝:ℝhy✝:a✝ ∈ Rat.cast '' (LIM a).toSet_Raty:ℚhy:y ∈ (LIM a).toSet_Rath:↑y = a✝⊢ a✝ ≤ Real.mk ha.CauSeq a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM aa✝:ℝhy✝:a✝ ∈ Rat.cast '' (LIM a).toSet_Raty:ℚhy:y ∈ (LIM a).toSet_Rath:↑y = a✝⊢ Real.mk (CauSeq.const _root_.abs y) ≤ Real.mk ha.CauSeq All goals completed! 🐙 -- show that for any other upper bound, `Real.mk ha.CauSeq` is smaller a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM aM:ℝhM:M ∈ upperBounds (Rat.cast '' (LIM a).toSet_Rat)⊢ Real.mk ha.CauSeq ≤ M All goals completed! 🐙lemma Real.equivR_eq (x: Real) : ∃(a : ℕ → ℚ) (ha: Sequence.IsCauchy a), x = LIM a ∧ x.equivR = Real.mk ha.CauSeq := x:Real⊢ ∃ a, ∃ (ha : (↑a).IsCauchy), x = LIM a ∧ equivR x = Real.mk ha.CauSeq a:ℕ → ℚha:(↑a).IsCauchy⊢ ∃ a_1, ∃ (ha : (↑a_1).IsCauchy), LIM a = LIM a_1 ∧ equivR (LIM a) = Real.mk ha.CauSeq 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! 🐙
-- helpers for converting properties between Real and ℝ lemma Real.equivR_map_mul {x y : Real} : equivR (x * y) = equivR x * equivR y := equivR_ordered_ring.map_mul _ _lemma Real.equivR_map_inv {x: Real} : equivR (x⁻¹) = (equivR x)⁻¹ := map_inv₀ equivR_ordered_ring _theorem declaration uses 'sorry'Real.equivR_map_pos {x: Real} : 0 < x ↔ 0 < equivR x := x:Real⊢ 0 < x ↔ 0 < equivR x All goals completed! 🐙theorem declaration uses 'sorry'Real.equivR_map_nonneg {x: Real} : 0 ≤ x ↔ 0 ≤ equivR x := x:Real⊢ 0 ≤ x ↔ 0 ≤ equivR x All goals completed! 🐙-- Showing equivalence of the different pows 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