Real Number Structures

Let IR be a structure for real numbers.

CReals axioms

First properties which follow trivially from the axioms.

A stronger version, which often comes in useful.

Cauchy sequences

Alternative definitions

This section gives several definitions of Cauchy sequences. There are no lemmas in this section.

The current definition of Cauchy (Cauchy_prop) is:

for all e>0 there exists N such that for all m≥ N |seqm-seqN|≤ e

Variant 1 of Cauchy (Cauchy_prop1) is:

for all k there exists N such that for all m ≥ N |seqm-seqN| ≤ 1/(k+1)

In all of the following variants the limit occurs in the definition. Therefore it is useful to define an auxiliary predicate Cauchy_Lim_prop?, in terms of which Cauchy_prop? is defined.

Variant 2 of Cauchy (Cauchy_prop2) is exists y, (Cauchy_Lim_prop2 seq y) where
Cauchy_Lim_prop2 seq y := forall ε [>] 0, exists N, forall m >= N, (AbsIR seq m - y) [<=] ε

Note that Cauchy_Lim_prop2 equals seqLimit.

Variant 3 of Cauchy (Cauchy_prop3) reads exists y, (Cauchy_Lim_prop3 seq y) where
Cauchy_Lim_prop3 seq y := forall k, exists N, forall m >= N, (AbsIR seq m - y) [<=] 1[/] (k[+]1)

The following variant is more restricted.

Variant 4 of Cauchy (Cauchy_prop4): exists y, (Cauchy_Lim_prop4 seq y) where
Cauchy_Lim_prop4 seq y := forall k, (AbsIR seq m - y) [<=] 1[/] (k[+]1)

So
Cauchy_prop4 -> Cauchy_prop3 ⇔ Cauchy_prop2 ⇔ Cauchy_prop1 ⇔ Cauchy_prop

Note: we don't know which formulations are useful.

The inequalities are stated with ≤ rather than with < for the following reason: both formulations are equivalent, as is well known; and ≤ being a negative statement, this makes proofs sometimes easier and program extraction much more efficient.

Inequalities of Limits

The next lemma is equal to lemma Lim_Cauchy.

The next lemma follows from less_Lim_so_less_seq with y := (y+ (Lim seq)) /2.

Equivalence of formulations of Cauchy

Well definedness.

Properties of Cauchy sequences

Some of these lemmas are now obsolete, because they were reproved for arbitrary ordered fields...

We begin by defining the constant sequence and proving that it is Cauchy with the expected limit.