The Real Number Structure
We will now apply our Cauchy sequence construction to an archimedean ordered field in order to obtain a model of the real numbers.
Injection of Q
We start by showing how to inject the rational numbers in the field of Cauchy sequences; this embedding preserves the algebraic operations.
Let F be an ordered field.
Variable F : COrdField.
Notation "'R_COrdField''" := (R_COrdField F).
Definition inject_Q (x : F) : R_COrdField' := Build_CauchySeq _ _ (CS_seq_const _ x).
Lemma ing_eq : forall x y : F, x [=] y -> inject_Q x [=] inject_Q y.
Lemma ing_plus : forall x y : F, inject_Q (x[+]y) [=] inject_Q x[+]inject_Q y.
Lemma ing_min : forall x : F, inject_Q [--]x [=] [--] (inject_Q x).
Lemma ing_lt : forall x y : F, x [<] y -> inject_Q x [<] inject_Q y.
Lemma ing_ap : forall x y : F, x [#] y -> inject_Q x [#] inject_Q y.
Lemma ing_cancel_eq : forall x y : F, inject_Q x [=] inject_Q y -> x [=] y.
Lemma ing_cancel_less : forall x y : F, inject_Q x [<] inject_Q y -> x [<] y.
Lemma ing_le : forall x y : F, x [<=] y -> inject_Q x [<=] inject_Q y.
Lemma ing_cancel_leEq : forall x y : F, inject_Q x [<=] inject_Q y -> x [<=] y.
Lemma ing_cancel_AbsSmall : forall e x y : F,
AbsSmall (inject_Q e) (inject_Q x[-]inject_Q y) -> AbsSmall e (x[-]y).
Lemma ing_One : inject_Q (1:F) [=] 1.
Lemma ing_nring' : forall m n : N,
CS_seq _ (nring (R:=R_COrdField') n) m [=] CS_seq _ (inject_Q (nring n)) m.
Lemma ing_nring : forall n : N, nring n [=] inject_Q (nring n).
Lemma ing_mult : forall x y : F, inject_Q (x[*]y) [=] inject_Q x[*]inject_Q y.
Lemma ing_div_three : forall x, inject_Q x [/]3 [=] inject_Q (x [/]3).
Lemma ing_n : forall x n H1 H2,
(inject_Q x[/] nring n[//]H2) [=] inject_Q (x[/] nring n[//]H1).
Theorem expand_Q_R : forall (x : R_COrdField') e, 0 [<] e -> forall N,
(forall m, N <= m -> AbsSmall (e [/]4) (CS_seq F x m[-]CS_seq F x N)) ->
forall m, N <= m -> AbsSmall (inject_Q e) (inject_Q (CS_seq F x m) [-]x).
Lemma conv_modulus : forall (x : R_COrdField') M, {N : N | forall m,
N <= m -> AbsSmall (one_div_succ M) (CS_seq F x m[-]CS_seq F x N)}.
Let T (x : R_COrdField') (m : N) := let (N, _) := conv_modulus x m in N.
We now assume our original field is archimedean and prove that the
resulting one is, too.
Hypothesis F_is_archemaedian : forall x : F, {n : N | x [<] nring n}.
Theorem R_is_archemaedian : forall x : R_COrdField', {n : N | x [<=] nring n}.
Lemma modulus_property : forall x M m0 m1, T x M <= m0 -> T x M <= m1 ->
AbsSmall (2[*]one_div_succ M) (CS_seq F x m0[-]CS_seq F x m1).
Lemma modulus_property_2 : forall x M m, T x M <= m ->
AbsSmall (one_div_succ M) (CS_seq F x m[-]CS_seq F x (T x M)).
Lemma expand_Q_R_2 : forall x e N, 0 [<] e ->
(forall m, N <= m -> AbsSmall (e [/]4) (CS_seq F x m[-]CS_seq F x N)) ->
AbsSmall (inject_Q e) (inject_Q (CS_seq F x N) [-]x).
Lemma CS_seq_diagonal : forall a : CauchySeq R_COrdField',
Cauchy_prop (fun m => let b := (CS_seq _ a m) in CS_seq F b (T b m)).
Lemma Q_dense_in_R : forall x, 0 [<] x -> {q : F | 0 [<] q | inject_Q q [<] x}.
Definition LimR_CauchySeq (a : CauchySeq R_COrdField') :=
Build_CauchySeq _ _ (CS_seq_diagonal a).
Theorem R_is_complete : forall a : CauchySeq R_COrdField',
SeqLimit (R:=R_COrdField') a (LimR_CauchySeq a).
Definition R_is_CReals := Build_is_CReals _
LimR_CauchySeq R_is_complete R_is_archemaedian.
Definition R_as_CReals := Build_CReals _ _ R_is_CReals.
End R_CReals.