4 The reals
We finally construct the real numbers starting from our rationals \(\mathrm{MyRat}\). As usual lean already has a type called \(\mathbb {R}\), so we define a new type called \(\mathrm{MyReal}\) that will be another definition of the real numbers.
The idea is the classical one: a real number is a Cauchy sequence of rationals, where two Cauchy sequences are identified when their difference tends to \(0\). We will use the absolute value \(|x|\) of an element \(x\) of \(\mathrm{MyRat}\), which lean already knows about: since \(\mathrm{MyRat}\) is ordered, \(|x|\) is defined as \(\max (x, -x)\).
4.1 Cauchy sequences
A sequence of rationals is just a function \(x \colon \mathrm{MyNat}\to \mathrm{MyRat}\), and we write \(x_n\) for its value at \(n\).
A sequence \(x \colon \mathrm{MyNat}\to \mathrm{MyRat}\) is a Cauchy sequence if
Every Cauchy sequence \(x\) is bounded: there exists \(B {\gt} 0\) such that \(|x_n| \leq B\) for all \(n\).
Apply the definition with \(\varepsilon = 1\) to get an \(N\), and take \(B\) to be the maximum of \(1 + |x_N|\) and the finitely many values \(|x_0|, \dots , |x_{N-1}|\).
\(\mathrm{MyReal}\) will be a quotient of a type called \(\mathrm{MyPrereal}\).
Let \(\mathrm{MyPrereal}\) be the type of Cauchy sequences, that is the subtype of \(x \colon \mathrm{MyNat}\to \mathrm{MyRat}\) such that \(x\) is a Cauchy sequence.
We define a relation \(R\) on \(\mathrm{MyPrereal}\) as follows: \(x\) and \(y\) are related if and only if
in other words if their difference tends to \(0\).
\(R\) is a reflexive relation.
Exercise.
\(R\) is a symmetric relation.
Exercise.
\(R\) is a transitive relation.
Exercise, using the triangle inequality and splitting \(\varepsilon \) into \(\varepsilon /2 + \varepsilon /2\).
We have that \(R\) is an equivalence relation. From now on, we will write \(x \approx y\) for \(x R y\).
For any rational \(x\), the constant sequence \(n \mapsto x\) is a Cauchy sequence.
Obvious, since \(|x - x| = 0 \leq \varepsilon \).
We now endow \(\mathrm{MyPrereal}\) with the algebraic operations, all defined termwise.
We define the zero of \(\mathrm{MyPrereal}\) as the constant sequence \(0\).
We define the one of \(\mathrm{MyPrereal}\) as the constant sequence \(1\).
If \(x\) is a Cauchy sequence, then \(-x\) (the termwise negation) is a Cauchy sequence. In particular negation is well defined on \(\mathrm{MyPrereal}\).
Exercise.
If \(x \approx x'\), then \(-x \approx -x'\).
Exercise.
If \(x\) and \(y\) are Cauchy sequences, then \(x + y\) (the termwise sum) is a Cauchy sequence. In particular addition is well defined on \(\mathrm{MyPrereal}\).
Exercise, splitting \(\varepsilon \) into \(\varepsilon /2 + \varepsilon /2\).
If \(x \approx x'\) and \(y \approx y'\), then \(x + y \approx x' + y'\).
Exercise.
If \(x\) and \(y\) are Cauchy sequences, then \(x * y\) (the termwise product) is a Cauchy sequence. In particular multiplication is well defined on \(\mathrm{MyPrereal}\).
Write \(x_p y_p - x_q y_q = x_p(y_p - y_q) + (x_p - x_q)y_q\) and use that Cauchy sequences are bounded (Lemma 126).
If \(x \approx x'\) and \(y \approx y'\), then \(x * y \approx x' * y'\).
Exercise, again using boundedness.
Inversion is more delicate: to invert a Cauchy sequence we first need to know that, if it does not tend to \(0\), then it is eventually bounded away from \(0\).
Let \(x\) be in \(\mathrm{MyPrereal}\) with \(x \not\approx 0\). Then there exist \(\delta {\gt} 0\) and \(N\) such that \(\delta {\lt} |x_n|\) for all \(n \geq N\).
Since \(x \not\approx 0\) there is some \(\varepsilon {\gt} 0\) for which the defining condition fails; combine this with the Cauchy property to make \(|x_n|\) eventually larger than \(\delta = \varepsilon /2\).
Let \(x\) be in \(\mathrm{MyPrereal}\) with \(x \not\approx 0\). Then the termwise inverse \(x^{-1}\) is a Cauchy sequence.
Using Lemma 142 the terms are eventually bounded away from \(0\), and then \(|x_p^{-1} - x_q^{-1}| = |x_p - x_q| / |x_p x_q|\) is controlled.
We define the inverse of \(x\) in \(\mathrm{MyPrereal}\) as the termwise inverse \(x^{-1}\) if \(x \not\approx 0\), and as \(0\) otherwise. Note that it is always defined.
If \(x \approx x'\), then \(x^{-1} \approx x'^{-1}\).
Exercise.
4.2 The reals
4.2.1 Definitions
We define our reals \(\mathrm{MyReal}\) as
We will write \(⟦ x ⟧\) for the class of the Cauchy sequence \(x\).
We define the zero of \(\mathrm{MyReal}\), denoted \(0\), as the class of the zero of \(\mathrm{MyPrereal}\).
We define the one of \(\mathrm{MyReal}\), denoted \(1\), as the class of the one of \(\mathrm{MyPrereal}\).
4.2.2 Field structure
We define the negation of \(⟦ x ⟧\) in \(\mathrm{MyReal}\) as \(⟦ -x ⟧\). Thanks to Lemma 137 this is well defined.
We define the addition of \(⟦ x ⟧\) and \(⟦ y ⟧\) in \(\mathrm{MyReal}\) as \(⟦ x + y ⟧\). Thanks to Lemma 139 this is well defined.
We define the multiplication of \(⟦ x ⟧\) and \(⟦ y ⟧\) in \(\mathrm{MyReal}\) as \(⟦ x * y ⟧\). Thanks to Lemma 141 this is well defined.
We define the inverse of \(⟦ x ⟧\) in \(\mathrm{MyReal}\) as \(⟦ x^{-1} ⟧\). Thanks to Lemma 145 this is well defined.
\(\mathrm{MyReal}\) with addition and multiplication is a commutative ring.
All the ring axioms are checked by reducing to representatives and using that the operations are termwise, so everything follows from the corresponding properties in \(\mathrm{MyRat}\).
In \(\mathrm{MyReal}\) we have \(0 \neq 1\).
If \(0 = 1\) then the constant sequences \(0\) and \(1\) would be related, which is false since \(|0 - 1| = 1\) does not become small.
Let \(x \neq 0\) be in \(\mathrm{MyReal}\). Then \(x * x^{-1} = 1\).
Let \(x = ⟦ a ⟧\) with \(a \not\approx 0\). By Lemma 142 the terms \(a_n\) are eventually nonzero, so \(a_n a_n^{-1} = 1\) eventually, and hence \(a * a^{-1} \approx 1\).
\(\mathrm{MyReal}\) with addition and multiplication is a field.
4.2.3 The inclusion \(k \colon \mathrm{MyRat}\to \mathrm{MyReal}\)
We define a map
sending a rational to the class of the corresponding constant sequence.
We have that \(k(0) = 0\).
Clear from the definition.
We have that \(k(1) = 1\).
Clear from the definition.
For all \(x\) in \(\mathrm{MyRat}\) we have that \(k(-x) = -k(x)\).
Clear from the definition.
For all \(x\) and \(y\) in \(\mathrm{MyRat}\) we have that \(k(x + y) = k(x) + k(y)\).
Clear from the definition.
For all \(x\) and \(y\) in \(\mathrm{MyRat}\) we have that \(k(x - y) = k(x) - k(y)\).
Clear from the definition.
For all \(x\) and \(y\) in \(\mathrm{MyRat}\) we have that \(k(x * y) = k(x) * k(y)\).
Clear from the definition.
For all \(x\) in \(\mathrm{MyRat}\) we have that \(k(x^{-1}) = k(x)^{-1}\).
Exercise.
We have that \(k\) is injective.
If \(k(x) = k(y)\) then the constant sequences \(x\) and \(y\) are related, so \(|x - y|\) is arbitrarily small and hence \(x = y\).
4.3 Positivity
To define the order on \(\mathrm{MyReal}\) we follow the same strategy as for \(\mathrm{MyRat}\): we first introduce a notion of positivity and nonnegativity at the level of \(\mathrm{MyPrereal}\).
4.3.1 Positive prereals
Given \(x\) in \(\mathrm{MyPrereal}\), we say that \(x\) is positive if there exist \(\delta {\gt} 0\) and \(N\) such that \(\delta \leq x_n\) for all \(n \geq N\), in other words if \(x\) is eventually bounded below by a positive rational.
If \(x\) is positive, then there exists \(N\) such that \(0 {\lt} x_n\) for all \(n \geq N\).
Immediate from the definition.
The one of \(\mathrm{MyPrereal}\) is positive.
Take \(\delta = 1\).
If \(x \approx 0\), then \(x\) is not positive.
If \(x\) were positive its terms would eventually be at least \(\delta {\gt} 0\), contradicting \(x \approx 0\).
If \(x\) is positive, then \(x \not\approx 0\).
Contrapositive of Lemma 169.
If \(x \approx x'\) and \(x\) is positive, then \(x'\) is positive.
Exercise.
Let \(x\) and \(y\) in \(\mathrm{MyPrereal}\) both positive. Then \(x + y\) is positive.
Exercise.
Let \(x\) and \(y\) in \(\mathrm{MyPrereal}\) both positive. Then \(x * y\) is positive.
Exercise.
4.3.2 Nonnegative prereals
Given \(x\) in \(\mathrm{MyPrereal}\), we say that \(x\) is nonnegative if either \(x\) is positive or \(x \approx 0\).
If \(x \approx 0\), then \(x\) is nonnegative.
Clear from the definition.
If there exists \(N\) such that \(0 \leq x_n\) for all \(n \geq N\), then \(x\) is nonnegative.
If \(x \not\approx 0\) then, by an argument similar to Lemma 142, \(x\) is eventually bounded below by a positive rational, hence positive.
The zero of \(\mathrm{MyPrereal}\) is nonnegative.
Clear, since \(0 \approx 0\).
The one of \(\mathrm{MyPrereal}\) is nonnegative.
Clear because of Lemma 168.
If \(x \approx x'\) and \(x\) is nonnegative, then \(x'\) is nonnegative.
Follows from Lemma 171.
Let \(x\) be in \(\mathrm{MyPrereal}\) such that both \(x\) and \(-x\) are nonnegative. Then \(x \approx 0\).
Suppose \(x \not\approx 0\). Since \(x\) is nonnegative, \(x\) is positive. Since \(-x\) is nonnegative, either \(-x \approx 0\) or \(-x\) is positive. The first case implies \(x \approx 0\), a contradiction. In the second case, \(x_n\) and \(-x_n\) are both eventually bounded below by positive rationals, which is impossible on a common tail. Hence \(x \approx 0\).
Let \(x\) be in \(\mathrm{MyPrereal}\) such that \(x\) is not nonnegative. Then \(-x\) is nonnegative.
If \(x\) is not nonnegative then it is in particular not eventually nonnegative, so \(-x\) is eventually bounded below by a positive rational.
4.3.3 Nonnegative reals
The notion of nonnegativity descends to \(\mathrm{MyReal}\).
We say that \(⟦ x ⟧\) in \(\mathrm{MyReal}\) is nonnegative if \(x\) is nonnegative. Thanks to Lemma 179 this does not depend on the representative.
The zero of \(\mathrm{MyReal}\) is nonnegative.
Clear because of Lemma 177.
Let \(x\) be in \(\mathrm{MyReal}\) such that both \(x\) and \(-x\) are nonnegative. Then \(x = 0\).
Follows from Lemma 180.
Let \(x\) and \(y\) in \(\mathrm{MyReal}\) both nonnegative. Then \(x + y\) is nonnegative.
Reduce to representatives and use Lemma 172 (treating the cases where one of them is \(\approx 0\) separately).
Let \(x\) and \(y\) in \(\mathrm{MyReal}\) both nonnegative. Then \(x * y\) is nonnegative.
Reduce to representatives and use Lemma 173.
4.4 The order
Let \(x\) and \(y\) in \(\mathrm{MyReal}\). We write \(x \leq y\) if \(y - x\) is nonnegative.
We have that \(0 \leq x\) if and only if \(x\) is nonnegative.
Clear.
In \(\mathrm{MyReal}\) we have that \(0 \leq 1\).
Clear because of Lemma 178.
The relation \(\leq \) on \(\mathrm{MyReal}\) is reflexive.
Clear because of Lemma 183.
The relation \(\leq \) on \(\mathrm{MyReal}\) is transitive.
It follows from Lemma 185, since \((z - y) + (y - x) = z - x\).
The relation \(\leq \) on \(\mathrm{MyReal}\) is antisymmetric.
It follows from Lemma 184.
It follows that \(\leq \) is an order relation.
4.4.1 Interaction between the order and the ring structure
Let \(x\), \(y\) and \(t\) in \(\mathrm{MyReal}\) be such that \(x \leq y\). Then \(x + t \leq y + t\).
Clear from the definitions, since \((y + t) - (x + t) = y - x\).
Let \(x\) and \(y\) in \(\mathrm{MyReal}\) be such that \(0 \leq x\) and \(0 \leq y\). Then \(0 \leq x * y\).
It follows from Lemma 186.
We have proved that \(\mathrm{MyReal}\) is an ordered ring.
4.4.2 Interaction between the order and the inclusion
Let \(x\) and \(y\) in \(\mathrm{MyRat}\). We have that \(k(x) \leq k(y)\) if and only if \(x \leq y\).
Exercise.
Let \(x\) and \(y\) in \(\mathrm{MyRat}\). We have that \(k(x) {\lt} k(y)\) if and only if \(x {\lt} y\).
4.4.3 The linear order structure
The order \(\leq \) on \(\mathrm{MyReal}\) is a total order.
This follows by Lemma 181.
We have that \(\mathrm{MyReal}\) with \(\leq \) is a linear order.
Clear from the lemmas above.
Let \(a\) and \(b\) in \(\mathrm{MyReal}\) be such that \(0 {\lt} a\) and \(0 {\lt} b\). Then \(0 {\lt} a * b\).
Exercise, using that a positive real is the class of a positive prereal and Lemma 173.
We now have that \(\mathrm{MyReal}\) is a strict ordered ring.
4.5 Density and completeness
The whole point of this construction is that \(\mathrm{MyReal}\) is complete: every Cauchy sequence of reals converges. We first record that \(\mathrm{MyRat}\) is dense in \(\mathrm{MyReal}\) (through \(k\)).
4.5.1 Density
Let \(x\) in \(\mathrm{MyReal}\) and let \(\varepsilon \) in \(\mathrm{MyRat}\) with \(0 {\lt} \varepsilon \). Then there exists \(r\) in \(\mathrm{MyRat}\) with \(|x - k(r)| {\lt} k(\varepsilon )\).
Pick a representative \(a\) of \(x\); by the Cauchy property the rational \(r = a_N\) for \(N\) large enough works.
Let \(x\) in \(\mathrm{MyReal}\) with \(0 {\lt} x\). Then there exists \(r\) in \(\mathrm{MyRat}\) with \(0 {\lt} r\) and \(k(r) {\lt} x\).
A positive real is the class of a positive prereal, which is eventually bounded below by a positive rational \(r\).
Let \(x\) in \(\mathrm{MyReal}\) and let \(\varepsilon \) in \(\mathrm{MyReal}\) with \(0 {\lt} \varepsilon \). Then there exists \(r\) in \(\mathrm{MyRat}\) with \(|x - k(r)| {\lt} \varepsilon \).
4.5.2 Limits and Cauchy sequences in \(\mathrm{MyReal}\)
A sequence \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\) tends to \(x\) in \(\mathrm{MyReal}\) if
A sequence \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\) is convergent if it tends to some \(x\) in \(\mathrm{MyReal}\).
A sequence \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\) is a Cauchy sequence if
Let \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\) and \(x\) in \(\mathrm{MyReal}\). If for every rational \(\varepsilon {\gt} 0\) there exists \(N\) such that \(|f_n - x| \leq k(\varepsilon )\) for all \(n \geq N\), then \(f\) tends to \(x\).
It is enough to check the condition for \(\varepsilon \) of the form \(k(\delta )\), which is possible by density (Lemma 201).
Let \(x\) in \(\mathrm{MyPrereal}\). Then the sequence \(n \mapsto k(x_n)\) tends to \(⟦ x ⟧\).
Immediate from the definition of \(\approx \) and Lemma 206: the Cauchy property of \(x\) is exactly what is needed.
4.5.3 Completeness
Let \(x\) in \(\mathrm{MyReal}\). Then there exists a natural number \(n\) such that \(x \leq k(i(n+1))\), where \(i \colon \mathrm{MyNat}\to \mathrm{MyRat}\) is the inclusion.
Apply density with \(\varepsilon = 1\) to find \(r\) with \(|x-k(r)|{\lt}1\), so \(x{\lt}k(r+1)\). Then use Lemma 124 to bound \(r+1\) by some \(i(m)\), enlarge this to a bound of the form \(i(n+1)\), and transfer the inequality through \(k\).
Let \(x\) in \(\mathrm{MyReal}\) with \(0 {\lt} x\). Then there exists a natural number \(n\) such that \(k(i(n+1)^{-1}) \leq x\).
Apply Lemma 208 to \(x^{-1}\) and take inverses.
Let \(x\) in \(\mathrm{MyReal}\) and \(n\) a natural number. Then there exists a rational \(r\) such that \(|x - k(r)| {\lt} k(i(n+1)^{-1})\).
Apply density (Lemma 200) with \(\varepsilon = i(n+1)^{-1}\).
Let \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\). Then there exists \(g \colon \mathrm{MyNat}\to \mathrm{MyRat}\) such that \(|f_n - k(g_n)| {\lt} k(i(n+1)^{-1})\) for all \(n\).
Apply Lemma 210 for each \(n\) and collect the choices.
Given \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\), we define \(\mathrm{approx}(f) \colon \mathrm{MyNat}\to \mathrm{MyRat}\) to be a choice of rational approximating sequence as in Lemma 211.
For all \(n\) we have \(|f_n - k(\mathrm{approx}(f)_n)| {\lt} k(i(n+1)^{-1})\).
This is the defining property of \(\mathrm{approx}(f)\).
If \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\) is a Cauchy sequence, then \(\mathrm{approx}(f)\) is a Cauchy sequence of rationals.
If \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\) is a Cauchy sequence, then \(\mathrm{approx}(f)\), being a Cauchy sequence of rationals, defines an element of \(\mathrm{MyPrereal}\).
\(\mathrm{MyReal}\) is complete: every Cauchy sequence \(f \colon \mathrm{MyNat}\to \mathrm{MyReal}\) is convergent.
Let \(a = \mathrm{approx}(f)\), seen as an element of \(\mathrm{MyPrereal}\) (Definition 215), and let \(x = ⟦ a ⟧\). By Lemma 207 the sequence \(n \mapsto k(a_n)\) tends to \(x\), and by Lemma 213 the sequence \(f\) stays close to \(n \mapsto k(a_n)\), so \(f\) tends to \(x\). Hence \(f\) is convergent.