The Field of Cauchy Sequences
In this chapter we will prove that whenever we start from an ordered field F, we can define a new ordered field of Cauchy sequences over F.
Let F be an ordered field.
Setoid Structure
R_Set is the setoid of Cauchy sequences over F; given two sequences x,y over F, we say that x is smaller than y if from some point onwards (y n) − (x n) is greater than some fixed, positive e. Apartness of two sequences means that one of them is smaller than the other, equality is the negation of the apartness.
Definition R_Set := CauchySeq F.
Section CSetoid_Structure.
Definition R_lt (x y : R_Set) := {N : N |
{e : F | 0 [<] e | forall n, N <= n -> e [<=] CS_seq _ y n[-]CS_seq _ x n}}.
Definition R_ap (x y : R_Set) := R_lt x y or R_lt y x.
Definition R_eq (x y : R_Set) := ~ (R_ap x y).
Lemma R_lt_cotrans : cotransitive R_lt.
Lemma R_ap_cotrans : cotransitive R_ap.
Lemma R_ap_symmetric : Csymmetric R_ap.
Lemma R_lt_irreflexive : irreflexive R_lt.
Lemma R_ap_irreflexive : irreflexive R_ap.
Lemma R_ap_eq_tight : tight_apart R_eq R_ap.
Definition R_CSetoid : CSetoid.
Defined.
End CSetoid_Structure.
Section Group_Structure.
Group Structure
The group structure is just the expected one; the lemmas which are specifically proved are just the necessary ones to get the group axioms.Definition R_plus (x y : R_CSetoid) : R_CSetoid :=
Build_CauchySeq _ _ (CS_seq_plus F _ _ (CS_proof _ x) (CS_proof _ y)).
Definition R_zero := Build_CauchySeq _ _ (CS_seq_const F 0).
Lemma R_plus_lft_ext : forall x y z, R_plus x z [#] R_plus y z -> x [#] y.
Lemma R_plus_assoc : associative R_plus.
Lemma R_zero_lft_unit : forall x, R_plus R_zero x [=] x.
Lemma R_plus_comm : forall x y, R_plus x y [=] R_plus y x.
Definition R_inv (x : R_CSetoid) : R_CSetoid :=
Build_CauchySeq _ _ (CS_seq_inv F _ (CS_proof _ x)).
Lemma R_inv_is_inv : forall x, R_plus x (R_inv x) [=] R_zero.
Lemma R_inv_ext : un_op_strext _ R_inv.
Definition Rinv : CSetoid_un_op R_CSetoid.
Defined.
Definition R_CAbGroup : CAbGroup.
Defined.
End Group_Structure.
Section Ring_Structure.
Definition R_mult (x y : R_CAbGroup) : R_CAbGroup :=
Build_CauchySeq _ _ (CS_seq_mult F _ _ (CS_proof _ x) (CS_proof _ y)).
Definition R_one : R_CAbGroup := Build_CauchySeq _ _ (CS_seq_const F 1).
Lemma R_one_ap_zero : R_one [#] 0.
Lemma R_mult_dist_plus : forall x y z, R_mult x (y[+]z) [=] R_mult x y[+]R_mult x z.
Lemma R_mult_dist_minus : forall x y z, R_mult x (y[-]z) [=] R_mult x y[-]R_mult x z.
Lemma R_one_rht_unit : forall x, R_mult x R_one [=] x.
Lemma R_mult_comm : forall x y, R_mult x y [=] R_mult y x.
Lemma R_mult_ap_zero' : forall x y, R_mult x y [#] 0 -> x [#] 0.
Lemma R_mult_lft_ext : forall x y z, R_mult x z [#] R_mult y z -> x [#] y.
Lemma R_mult_rht_ext : forall x y z, R_mult x y [#] R_mult x z -> y [#] z.
Lemma R_mult_strext : bin_op_strext _ R_mult.
Definition Rmult : CSetoid_bin_op R_CAbGroup.
Defined.
Lemma R_mult_assoc : associative Rmult.
Lemma R_one_lft_unit : forall x, R_mult R_one x [=] x.
Definition R_CRing : CRing.
Defined.
End Ring_Structure.
Section Field_Structure.
Field Structure
For the field structure, it is technically easier to first prove that our ring is actually an integral domain. The rest then follows quite straightforwardly.Lemma R_integral_domain :
forall x y : R_CRing, x [#] 0 -> y [#] 0 -> x[*]y [#] 0.
Definition R_recip : forall x : R_CRing, x [#] 0 -> R_CRing.
Defined.
Lemma R_recip_inverse : forall x x_, x[*]R_recip x x_ [=] 1.
Lemma R_recip_strext : forall x y x_ y_, R_recip x x_ [#] R_recip y y_ -> x [#] y.
Lemma R_recip_inverse' : forall x x_, R_recip x x_[*]x [=] 1.
Definition R_CField : CField.
Defined.
End Field_Structure.
Section Order.
Order Structure
Finally, we extend the field structure with the ordering we defined at the beginning.Lemma R_lt_strext : Crel_strext R_CSetoid R_lt.
Definition Rlt : CCSetoid_relation R_CField.
Defined.
Lemma Rlt_transitive : Ctransitive Rlt.
Lemma Rlt_strict : strictorder Rlt.
Lemma R_plus_resp_lt : forall x y, Rlt x y -> forall z, Rlt (x[+]z) (y[+]z).
Lemma R_mult_resp_lt : forall x y, Rlt 0 x -> Rlt 0 y -> Rlt 0 (x[*]y).
Definition R_COrdField : COrdField.
Defined.
End Order.
Section Auxiliary.
Lemma Rlt_alt_1 : forall x y : R_Set, {e : F | 0 [<] e |
{N : N | forall m, N <= m -> e [<=] CS_seq F y m[-]CS_seq F x m}} -> Rlt x y.
Lemma Rlt_alt_2 : forall x y : R_Set, Rlt x y -> {e : F | 0 [<] e |
{N : N | forall m, N <= m -> e [<=] CS_seq F y m[-]CS_seq F x m}}.
Lemma R_ap_alt_1 : forall x y : R_CSetoid, x [#] y -> {e : F | 0 [<] e |
{N : N | forall m, N <= m -> AbsBig e (CS_seq F x m[-]CS_seq F y m)}}.
Lemma Eq_alt_1 : forall (x y : R_Set) (e : F), 0 [<] e ->
~ {N : N | forall m, N <= m -> AbsBig (e [/]4) (CS_seq F x m[-]CS_seq F y m)} ->
{N : N | forall m, N <= m -> AbsSmall e (CS_seq F x m[-]CS_seq F y m)}.
Lemma R_ap_alt_2 : forall x y : R_CSetoid, {e : F | 0 [<] e |
{N : N | forall m, N <= m -> AbsBig e (CS_seq F x m[-]CS_seq F y m)}} -> x [#] y.
Lemma Eq_alt_2_1 : forall x y : R_Set, ~ (R_ap x y) -> forall e : F, 0 [<] e ->
{N : N | forall m, N <= m -> AbsSmall e (CS_seq F x m[-]CS_seq F y m)}.
Lemma Eq_alt_2_2 : forall x y : R_Set, (forall e : F, 0 [<] e ->
{N : N | forall m, N <= m -> AbsSmall e (CS_seq F x m[-]CS_seq F y m)}) -> ~ (R_ap x y).
End Auxiliary.
End Structure.