Chapter 5 epilogue: isomorphism with the Mathlib real number

Stream: Analysis I

[Louis Cabarion]

Has anyone managed to make Section_5_epilogue.lean build sorry free?

[Louis Cabarion]

Some context: in the chapter 5 epilogue it is shown that there is an isomorphism between the Chapter 5 reals and the Mathlib reals.

[Louis Cabarion]

Could it be that this level (the section 5 epilogue) hasn’t been "play tested" by anyone yet?

[Aaron Liu]

Honestly I don't see why we have to go through dedekind cuts

[Aaron Liu]

Both constructions satisfy the property "(conditionally) complete linear ordered field" and so must be uniquely isomorphic as ordered fields

[Aaron Liu]

Since they must be Archimedean and any Archimedean linear ordered field embeds uniquely in any conditionally complete linearly ordered field

[Louis Cabarion]

@Aaron Liu I'm not sure I follow. Are you suggesting that the Cauchy sequence construction should have been used instead, or that an axiomatic approach would be more appropriate? I thought the intention was to follow the book, which uses the Dedekind construction. If I understand correctly, the Dedekind approach is typically used in introductory real analysis texts (such as Analysis I and Baby Rudin) because it's conceptually simpler than the Cauchy construction.

[Aaron Liu]

I mean for showing that Chapter5.Real is uniquely isomorphic to _root_.Real you really don't need to know the details of either of them, just that they're both conditionally complete linearly ordered fields, and you also don't have to define dedekind cuts. Uniqueness is a lot easier than existence ehre.

[Louis Cabarion]

@Aaron Liu Now I think I follow. The goal should be to show noncomputable instance : ConditionallyCompleteLinearOrderedField Chapter5.Real := …?

(We already know that noncomputable instance : ConditionallyCompleteLinearOrderedField ℝ := { }.)

Context:

* `ConditionallyCompleteLinearOrderedField`: A field satisfying the standard axiomatization of
  the real numbers, being a Dedekind complete and linear ordered field.

[Aaron Liu]

There is docs#LinearOrderedField.uniqueOrderRingIso in mathlib, I'm saying you can just replicate this argument with Chapter5.Real and _root_.Real, without having to go through dedekind cuts.

[Aaron Liu]

The problem with textbook dedekind cuts is that they duplicate all the rational numbers and you have to explicitly exclude some of them

[Li Xuanji]

Could it be that this level (the section 5 epilogue) hasn’t been "play tested" by anyone yet?

FWIW I'm doing the exercises roughly in order, but I find the epilogues and Chapter 3 pretty boring so I am planning to skip them until after chapter 11 :slight_smile:

[Terence Tao]

I have not playtested this epilogue either, but my intent was to avoid too heavy a reliance on existing Mathlib theorems such as docs#LinearOrderedField.uniqueOrderRingIso and use the opportunity to teach some further mathematics, in particular introducing the alternate Dedekind cut approach to the reals without having to set up the full construction. No doubt there are more efficient ways to achieve the specific goal of showing existence and uniqueness of the reals, but that was not quite my primary objective.

[Rado Kirov]

Ok, I am finally at this section. I got the set isomorphism working and I am stuck on proving the homomorphism for the various operations - see https://github.com/rkirov/analysis

I think I should make use of https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.html#csSup_add but haven't figure out how to.

[Rado Kirov]

ok, I have solutions for addition and le homomorphisms.

First I define addition, multiplication and le on Dedekind cuts. Then prove OrderedRing isos between Real ~ DedekindCuts and R ~ DedekindCuts (the second one is basically copy paste of the first). Finally mathlib already knows that OrderedRing isos compose. Not sure if this is defeating the original intent of the exercises, but it does require me to learn more about Dedekind cuts (to define their + and * ops). In fact, I haven't finished the mul part as there is some trickery involved, but will read Rubin tomorrow and figure it out.

see https://github.com/rkirov/analysis/commit/1a7741d2297b10f1a58a8711c111bd54a59b4e77

[Rado Kirov]

Made some more progress here - finished all pow iso proofs, started defining DedekindCut mul following Rudin, but ran into a blocker - termination checker is not happy with my definition. I have never worked with it, so will need to do some more poking around tomorrow to figure out how to convince it that the recursive call will always reach the positive-positive branch with at most one recusive call.

https://github.com/rkirov/analysis/commit/b0dfdf71d32c161e20ef10ecfc9374bd4142c58a#diff-aba545776da0ad4df868df9bba8a9b120c1aae75bf23cce41c21cab506bdecd0R360-R369

[Terence Tao]

It occurs to me that an alternate way to proceed is to show that the embedding of the rationals in both the Chapter 5 reals and the Mathlib reals are compatible with the isomorphism between the two, i.e.,

theorem Real.coe_equiv_coe (q:ℚ) : equivR (q:Real) = (q:ℝ) := by sorry

which is probably a lemma that should have gone in the epilogue anyway. From this lemma one can show homomorphism properties on the rationals first, and then take limits to conclude the corresponding homomorphism properties for general reals.

p.s. Please feel free to record any tips for future users as pull requests to these sections!

[Rado Kirov]

That's a great idea and looks much simpler than defining the whole theory of ring operations on Dedekind cuts.

So I have the following

theorem Real.equivR_eq (x:Real) (y: ℝ) : Real.equivR x = y ↔ x.toCut = y.toCut := by ???

theorem Real.coe_equiv_coe (q:ℚ) : equivR (q:Real) = (q:ℝ) :=  -- proved

theorem Real.equivR_add_q (x y : ℚ) : equivR ((x: Real) + (y: Real)) = equivR (x:Real) + equivR (y: Real) -- proved

theorem Real.equivR_LIM (a: ℕ -> ℚ) : equivR (LIM a) = LIM_IN_R fun (n: ℕ) ↦ equivR (a n)  -- ???

theorem Real.equivR_add (x y : Real) : equivR (x + y) = equivR x + equivR y :=  -- can be proved

What I am missing:
1) somehow can't finish the basic Real.equivR_eq . It should be just EquivLike.inv_apply_eq but I have a .symm instead of .inv and can't find a way to transform between them :'(
2) I don't know what's the equivalent of LIM in mathlib's R but I need it for some sort of equivR_LIM theorem to finish the proof.

[Rado Kirov]

p.s. Please feel free to record any tips for future users as pull requests to these sections!

Definitely, I plan so step back at the end of Chapter 5 (feels like a good point with all of Z,N,R built) and go through previous chapter and clean up stuff (also using @Dan Abramov solutions for Ch2 and Ch3 that was recently finished), and write up the tips sections. I am two sorries away from finishing all of ch5, so a hopefully will be done with this by this weekend.

[Rado Kirov]

Ok, ignore problem 1) above, you had that in the original scaffold - https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_5_epilogue.lean#L129-L131 I just removed when going after the DedekindCut OrderRingIso approach. Adding it back works perfectly (though I continue to find working with Equiv and EquivLike surprisingly tricky due to .symm vs .inv or .toFun of direct eval).

[Terence Tao]

As for problem 2: docs#CauSeq.lim might work for you. There is a more general limit notion docs#limUnder but it is a little unintuitive to use; the limit of a convergent sequence a:ℕ → ℝ, for instance, is I believe limUnder Filter.atTop a if I am not mistaken. The assertion that a sequence a converges to a limit L is Filter.atTop.Tendsto a (nhds L), which is a little clunky, although one gets used to it (and filters do eventually make mathematical sense, I promise!)

[Rado Kirov]

Using CauSeq worked reasonably well (I will eventually learn filters, but rather solve this more traditionally first).

The leftover parts of the proof now boils down to transforming inequalities for limits in Reals and R into statements purely in Q and then showing they are equivalent. The theorems I have left to prove are (statements could be a bit off):

theorem Real.LIM_lt_LIM {a b : ℕ → ℚ} (ha : Sequence.IsCauchy a) (hb : Sequence.IsCauchy b):
    LIM a < LIM b ↔ ∃ ε:ℚ, ε > 0 ∧ ∃ N, ∀ n ≥ N, a n < b n - ε := by
  sorry

theorem Real.LIM_le_LIM {a b : ℕ → ℚ} (ha : Sequence.IsCauchy a) (hb : Sequence.IsCauchy b):
    LIM a ≤ LIM b ↔ ∃ ε:ℚ, ε > 0 ∧ ∃ N, ∀ n ≥ N, a n < b n - ε ∨
    ∀ ε:ℚ, ε > 0 → ∃ N, ∀ n ≥ N, |a n - b n| ≤ ε := by
  sorry

theorem R.lim_lt_lim {a b : ℕ → ℝ} (ha : IsCauSeq abs a) (hb : IsCauSeq abs b):
    CauSeq.lim ⟨a, ha⟩ < CauSeq.lim ⟨b, hb⟩ ↔ ∃ ε:ℚ, ε > 0 ∧ ∃ N, ∀ n ≥ N, a n < b n - ε := by
  sorry

theorem R.lim_le_lim {a b : ℕ → ℝ} (ha : IsCauSeq abs a) (hb : IsCauSeq abs b):
    CauSeq.lim ⟨a, ha⟩ ≤ CauSeq.lim ⟨b, hb⟩ ↔ ∃ ε:ℚ, ε > 0 ∧ ∃ N, ∀ n ≥ N, a n < b n - ε
      ∨ ∀ ε:ℚ, ε > 0 → ∃ N, ∀ n ≥ N, |a n - b n| ≤ ε
     := by
  sorry

For custom Reals, it feels like something we would have proved (at least with epsilon real, and we can translate to epsilon in Q using exists_rat_between), but I can't seem to find it now.

For the versions in mathlib R, I am very stumped and can't seem to find anything like that.

[Kevin Buzzard]

As I type, Real.LIM_le_LIM is a statement about < not <=. I assume there is a slip somewhere? (edit: fixed)

[Terence Tao]

On looking a bit more at the CauSeq API it seems that there is only a light amount of API for lim itself, but a lot more on LimZero, the const Cauchy sequences, and the ordering on CauSeq, so one may have to first invoke things like docs#CauSeq.equiv_lim to translate things to a setting where there is more API.

[Rado Kirov]

As I type, Real.LIM_le_LIM is a statement about < not <=. I assume there is a slip somewhere?

Ah, typo, fixed it.

[Rado Kirov]

Made some more progress here. First I realized that some of the machinary in chapter 5 is just for \N -> \Q, so can be used directly. The theorems I had above can be restated as (and doing < and = version to derive <= easily):

Custom Real versions

theorem Real.LIM_lt_LIM {a b : ℕ → ℚ} (ha : Sequence.IsCauchy a) (hb : Sequence.IsCauchy b):
    LIM a < LIM b ↔ ∃ c: ℕ → ℚ, Sequence.IsCauchy c ∧ (BoundedAwayPos c) ∧ Sequence.Equiv (b - a) c

theorem Real.LIM_eq_LIM' {a b : ℕ → ℚ} (ha : Sequence.IsCauchy a) (hb : Sequence.IsCauchy b):
    LIM a = LIM b ↔ Sequence.Equiv (b - a) 0 := by

and mathlib versions

theorem R.lim_lt_lim {a b : ℕ → ℚ}
    (ha : IsCauSeq abs fun (n: ℕ) ↦ (a n : ℝ)) (hb : IsCauSeq abs fun (n: ℕ) ↦ (b n : ℝ)):
    CauSeq.lim ⟨fun (n: ℕ) ↦ (a n : ℝ), ha⟩ < CauSeq.lim ⟨fun (n: ℕ) ↦ (b n : ℝ), hb⟩ ↔
       ∃ c: ℕ → ℚ, Sequence.IsCauchy c ∧ BoundedAwayPos c ∧ Sequence.Equiv (b - a) c

theorem R.lim_eq_lim {a b : ℕ → ℚ}
    (ha : IsCauSeq abs fun (n: ℕ) ↦ (a n : ℝ)) (hb : IsCauSeq abs fun (n: ℕ) ↦ (b n : ℝ)):
    CauSeq.lim ⟨fun (n: ℕ) ↦ (a n : ℝ), ha⟩ = CauSeq.lim ⟨fun (n: ℕ) ↦ (b n : ℝ), hb⟩ ↔
      Sequence.Equiv a b := by

I proved the custom Reals version, and also R.lim_eq_lim using the tip from @Terence Tao to translate to LimZero and use https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/CauSeq/Completion.html#CauSeq.lim_eq_zero_iff. I think the same approach would work for R.lim_lt_lim but there is no lim_lt_zero_iff, so I need to understand a bit more how to use the other APIs.

Btw, noticed there is no CauSeq.lim_sub, so wrote my own - https://github.com/rkirov/analysis/blob/main/analysis/Analysis/Section_5_epilogue.lean#L439-L442. Should I be upstreaming that to mathlib? Or given how overwhelmed the review queue is not bother.

[Rado Kirov]

Found a number of other useful APIs (there were two files containing them in mathlib) and with some unfolding ( :shrug: I know I am not supposed to but there is no algorithm to know whether the right API wasn't build and unfolding is required, or I just haven't found it) managed to complete the final sorry - https://github.com/rkirov/analysis/commit/56babb2f9558a3d6f0e9be1b3c9f76c65ba04846.

One other purely CauSeq theorem I needed and proved :

theorem CauSeq.pos_equiv_pos (f g : CauSeq ℝ abs) (h: f ≈ g): f.Pos ↔ g.Pos := by

might be a good candidate for upstreaming too.

Chapter 5 is fully complete now! Will take the next few days to write up a retro and go back to fill in the tips.

[Terence Tao]

I'm not familiar with the Mathlib upstreaming process, but I would imagine that small commits that just add a few simple and uncontroversial lemmas should be easy to process.

I have a tools directory in the repository for lemmas that could potentially be useful outside of the analysis text, one could also temporarily put those lemmas there until the Mathlib process resolves, and import them in the Chapter 5 epilogue.

[Ruben Van de Velde]

There's documentation at https://leanprover-community.github.io/contribute/index.html , but yes, straightforward lemmas usually go through pretty quickly. (Definitions can be harder)