# Lecture 4.3: Mathematics — Rational and Real Numbers

Today we will go through the construction of `ℚ` and `ℝ` as quotient types

A similar construction will be shown in the next lecture for the _p_-adic integers


## Rational numbers

Rational numbers can be expressed as `n / d` where `n`, `d : ℤ`, representing the unique solution of `x` in the equation `x * d = n` for `d ≠ 0`

We use the following general idea to construct new types with specific properties:

 1. Create a new type to "syntactically" represent all elements

 2. Quotient this representation, equating syntactic elements that should be considered equal

 3. Define functions by lifting functions from the syntactic representation and prove that they respect the quotient relation

For `ℚ`:

 1. We simply introduce a dependent triple `(n : ℤ, d : ℤ, hd : d ≠ 0)` to represent `n / d`

 2. As quotient relation, we use `n / d ≈ n' / d' := n * d' = n' * d`

 3. Define `0 := 0 / 1`, `1 := 1 / 1`, and addition, multiplication, and order:

        n / d + n' / d'      :=  (n * d' + n' * d) / (d * d')
        (n / d) * (n' / d')  :=  (n * n') / (d * d')
        n / d ≤ n' / d'      :=  n * d' ≤ n' * d

    and show that they respect the relation `≈`

    Since these functions respect `≈`, we can `lift` them into functions on `ℚ`

Now we can prove that `ℚ` forms a `linear_orderd_field`

Alternative (extreme) definitions of `ℚ`:

* Use `(n : ℤ, d : ℤ, hd : 0 < d, h : coprime n d)`, where `coprime n d` says that `n` and `d` do not have a common divisor (except `1` and `-1`)

  This is the definition used in `mathlib`

  Advantages: no quotient required; more efficient computation; more theorems are definitional equalities

  Disadvantage: more complicated function definitions

* Define all elements syntactically, including the desired operations:

      inductive pre_ℚ : Type
      | zero, one : pre_ℚ
      | add, sub, mul, div : pre_ℚ → pre_ℚ → pre_ℚ

  Define `≈` to include congruence rules and to follow the `field` equations:

      inductive ≈ : pre_ℚ → pre_ℚ → Prop
      | add_congr {a b c d : pre_ℚ} : a ≈ b → c ≈ d → add a c ≈ add b d 
      | add_comm {a b : pre_ℚ}      : add a b ≈ add b a
      | add_assoc {a b c : pre_ℚ}   : add a (add b c) ≈ add (add a b) c
      ...

  Advantages: does not require `ℤ`; easy to prove the `field` equations; general recipe reusable for other algebraic constructions (e.g. [free monoids](https://en.wikipedia.org/wiki/Free_monoid), [free groups](https://en.wikipedia.org/wiki/Free_group))

  Disadvantage: the definition of orders and lemmas about them are more complicated


## Real numbers

`ℚ` is **incomplete**: the sets `{x ∈ ℚ | x² < 2}` and `{x ∈ ℚ | x² > 2}`  partition `ℚ`, but the supremum or infimum is not in `ℚ`

The sequence of rationals

    1, 1.4, 1.41, 1.414, 1.4142, 1.41421, 1.414213, 1.4142135, 1.41421356, ...

does not converge to a rational number

There are different ways to construct the real numbers:

* Cauchy sequences

* Dedekind cuts: `r : ℝ` is represented essentially as `{x : ℚ | x < r}`, i.e. as values of type `set ℚ` corresponding to sets that are nonempty, bounded to the right, and downwards closed

* Binary sequences `ℕ → bool` for the interval [0, 1]

Cauchy sequences are the easiest approach, especially if `ℚ` is already available

We follow the general recipe described above, using Cauchy sequence as the "syntactic" concept


## Cauchy sequences

`ℚ` cannot represent √2, but it can approximate it:

    1
    1.4
    1.41
    1.414
    1.4142
    1.41421
    1.414213
    1.4142135
    1.41421356
    ...

One way to approximate the missing numbers is to use _Cauchy_ sequences

A sequence `f : ℕ → α` is _Cauchy_ if the distance between two elements gets arbitrarily small:

    cauchy f  :=  ∀ε > 0, ∃N, ∀n ≥ N, |f N - f n| < ε

where `α` is equipped with an "absolute value" operator `| | : α → ℚ`

To construct `ℝ`, `α` will be `ℚ`

It is easy to define the operations on Cauchy sequences:

    0      :=  λn, 0
    1      :=  λn, 1
    f + g  :=  λn, f n + g n
    f * g  :=  λn, f n * g n

The definitions requires us to prove that when `f` and `g` form a Cauchy sequence, then `f + g` and `f * g` form Cauchy sequences

However, two different Cauchy sequences can approximate the same point:

    1                2
    1.4              1.5
    1.41             1.42
    1.414            1.415
    1.4142           1.4143
    1.41421          1.41422
    1.414213         1.414214
    1.4142135        1.4142136
    1.41421356       1.41421357
    ...               ...

Both converge towards √2

Two sequences are _equivalent_ if they approximate the same point:

    equiv f g  :=  ∀ε > 0, ∃N, ∀m ≥ N, ∀n ≥ N, |f m - g n| < ε

Cauchy sequences also have a order:

    0 < f := ∃ε > 0, ∃N, ∀m ≥ N, ε < f m

This is all we need since `f < g ↔ 0 < g - f`


## Constructing `ℝ`

`ℝ` is defined as the quotient of Cauchy sequences on `ℚ` with respect to the relation `equiv`

To define the ordered field structure on `ℝ`, all operations are lifted from Cauchy sequences

Unlike `ℚ`, `ℝ` is _complete_—i.e. all Cauchy sequence on `ℝ` have a limit:

    ∀f : ℕ → ℝ, cauchy f → ∃x, ∀ε > 0, ∃N, ∀m ≥ N, |f m - x| < ε


## Analysis

Analysis does not stop with introducing `ℝ`

`mathlib` has more material on analysis:

  * topological and metric spaces

  * linear algebra with modules and vector spaces

  * normed vector spaces

  * measures and simple integrals

But one of the more important concepts, derivatives, is still missing

In the next lecture, we will hear from Robert Y. Lewis about a related topic from number theory: _p_-adic numbers
