1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/reals/CauchySeq".
19 (* $Id: CauchySeq.v,v 1.8 2004/04/23 10:01:04 lcf Exp $ *)
21 (*#* printing IR %\ensuremath{\mathbb R}% *)
23 (*#* printing PartIR %\ensuremath{\mathbb R\!\not\rightarrow\!\mathbb R}% *)
25 (*#* printing ZeroR %\ensuremath{\mathbf0}% #0# *)
27 (*#* printing OneR %\ensuremath{\mathbf1}% #1# *)
29 (*#* printing AbsIR %\ensuremath{|\cdot|_{\mathbb R}}% *)
35 (*#* *Real Number Structures
36 %\begin{convention}% Let [IR] be a structure for real numbers.
41 Require Export R_CReals.
42 Definition IR : CReals := Concrete_R.
46 inline cic:/CoRN/reals/CauchySeq/IR.var.
57 Section CReals_axioms.
60 (*#* ** [CReals] axioms *)
62 inline cic:/CoRN/reals/CauchySeq/CReals_is_CReals.con.
64 (*#* First properties which follow trivially from the axioms. *)
66 inline cic:/CoRN/reals/CauchySeq/Lim_Cauchy.con.
68 inline cic:/CoRN/reals/CauchySeq/Archimedes.con.
70 inline cic:/CoRN/reals/CauchySeq/Archimedes'.con.
72 (*#* A stronger version, which often comes in useful. *)
74 inline cic:/CoRN/reals/CauchySeq/str_Archimedes.con.
76 inline cic:/CoRN/reals/CauchySeq/CauchySeqR.con.
86 (*#* ** Cauchy sequences
87 *** Alternative definitions
88 This section gives several definitions of Cauchy sequences. There
89 are no lemmas in this section.
91 The current definition of Cauchy ([Cauchy_prop]) is:
93 %\[\forall \epsilon>0. \exists N. \forall m\geq N. |seq_m - seq_N|\leq\varepsilon\]%
94 #for all e>0 there exists N such that for all m≥ N |seqm-seqN|≤ e#
96 Variant 1 of Cauchy ([Cauchy_prop1]) is:
98 %\[\forall k. \exists N. \forall m \geq N. |seq_m - seq_N|\leq1/(k+1)\]%
99 #for all k there exists N such that for all m ≥ N |seqm-seqN| ≤ 1/(k+1)#
101 In all of the following variants the limit occurs in the definition.
102 Therefore it is useful to define an auxiliary predicate
103 [Cauchy_Lim_prop?], in terms of which [Cauchy_prop?] is defined.
105 Variant 2 of Cauchy ([Cauchy_prop2]) is [exists y, (Cauchy_Lim_prop2 seq y)]
108 Cauchy_Lim_prop2 seq y := forall eps [>] Zero, exists N, forall m >= N, (AbsIR seq m - y) [<=] eps
111 Note that [Cauchy_Lim_prop2] equals [seqLimit].
113 Variant 3 of Cauchy ([Cauchy_prop3]) reads [exists y, (Cauchy_Lim_prop3 seq y)]
116 Cauchy_Lim_prop3 seq y := forall k, exists N, forall m >= N, (AbsIR seq m - y) [<=] One[/] (k[+]1)
119 The following variant is more restricted.
121 Variant 4 of Cauchy ([Cauchy_prop4]): [exists y, (Cauchy_Lim_prop4 seq y)]
124 Cauchy_Lim_prop4 seq y := forall k, (AbsIR seq m - y) [<=] One[/] (k[+]1)
129 Cauchy_prop4 -> Cauchy_prop3 Iff Cauchy_prop2 Iff Cauchy_prop1 Iff Cauchy_prop
131 Note: we don't know which formulations are useful.
133 The inequalities are stated with [[<=]] rather than with [<] for the
134 following reason: both formulations are equivalent, as is well known;
135 and [[<=]] being a negative statement, this makes proofs
136 sometimes easier and program extraction much more efficient.
139 inline cic:/CoRN/reals/CauchySeq/Cauchy_prop1.con.
141 inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2.con.
143 inline cic:/CoRN/reals/CauchySeq/Cauchy_prop2.con.
145 inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3.con.
147 inline cic:/CoRN/reals/CauchySeq/Cauchy_prop3.con.
149 inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4.con.
151 inline cic:/CoRN/reals/CauchySeq/Cauchy_prop4.con.
158 Section Inequalities.
161 (*#* *** Inequalities of Limits
163 The next lemma is equal to lemma [Lim_Cauchy]. *)
165 inline cic:/CoRN/reals/CauchySeq/Cauchy_complete.con.
167 inline cic:/CoRN/reals/CauchySeq/less_Lim_so_less_seq.con.
169 inline cic:/CoRN/reals/CauchySeq/Lim_less_so_seq_less.con.
171 inline cic:/CoRN/reals/CauchySeq/Lim_less_Lim_so_seq_less_seq.con.
173 (*#* The next lemma follows from [less_Lim_so_less_seq] with [y := (y[+] (Lim seq)) [/]TwoNZ]. *)
175 inline cic:/CoRN/reals/CauchySeq/less_Lim_so.con.
177 inline cic:/CoRN/reals/CauchySeq/Lim_less_so.con.
179 inline cic:/CoRN/reals/CauchySeq/leEq_seq_so_leEq_Lim.con.
181 inline cic:/CoRN/reals/CauchySeq/str_leEq_seq_so_leEq_Lim.con.
183 inline cic:/CoRN/reals/CauchySeq/Lim_leEq_Lim.con.
185 inline cic:/CoRN/reals/CauchySeq/seq_leEq_so_Lim_leEq.con.
187 inline cic:/CoRN/reals/CauchySeq/str_seq_leEq_so_Lim_leEq.con.
189 inline cic:/CoRN/reals/CauchySeq/Limits_unique.con.
191 inline cic:/CoRN/reals/CauchySeq/Lim_wd.con.
193 inline cic:/CoRN/reals/CauchySeq/Lim_strext.con.
195 inline cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap.con.
197 inline cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap'.con.
204 Section Equiv_Cauchy.
207 (*#* *** Equivalence of formulations of Cauchy *)
209 inline cic:/CoRN/reals/CauchySeq/Cauchy_prop1_prop.con.
211 inline cic:/CoRN/reals/CauchySeq/Cauchy_prop2_prop.con.
213 inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3_prop2.con.
215 inline cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop2.con.
217 inline cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop.con.
219 inline cic:/CoRN/reals/CauchySeq/Build_CauchySeq1.con.
221 inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop3.con.
223 inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop2.con.
225 inline cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop3.con.
227 inline cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop.con.
229 inline cic:/CoRN/reals/CauchySeq/Build_CauchySeq4.con.
231 inline cic:/CoRN/reals/CauchySeq/Build_CauchySeq4_y.con.
233 inline cic:/CoRN/reals/CauchySeq/Lim_CauchySeq4.con.
235 inline cic:/CoRN/reals/CauchySeq/Build_CauchySeq2.con.
237 inline cic:/CoRN/reals/CauchySeq/Build_CauchySeq2_y.con.
239 inline cic:/CoRN/reals/CauchySeq/Lim_CauchySeq2.con.
241 (*#* Well definedness. *)
243 inline cic:/CoRN/reals/CauchySeq/Cauchy_prop_wd.con.
245 inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2_wd.con.
247 inline cic:/CoRN/reals/CauchySeq/Lim_wd'.con.
249 inline cic:/CoRN/reals/CauchySeq/Lim_unique.con.
256 Section Cauchy_props.
259 (*#* *** Properties of Cauchy sequences
261 Some of these lemmas are now obsolete, because they were reproved for arbitrary ordered fields$\ldots$#...#
263 We begin by defining the constant sequence and proving that it is Cauchy with the expected limit.
266 inline cic:/CoRN/reals/CauchySeq/Cauchy_const.con.
268 inline cic:/CoRN/reals/CauchySeq/Lim_const.con.
270 inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_plus.con.
272 inline cic:/CoRN/reals/CauchySeq/Cauchy_plus.con.
274 inline cic:/CoRN/reals/CauchySeq/Lim_plus.con.
276 inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_inv.con.
278 inline cic:/CoRN/reals/CauchySeq/Cauchy_inv.con.
280 inline cic:/CoRN/reals/CauchySeq/Lim_inv.con.
282 inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_minus.con.
284 inline cic:/CoRN/reals/CauchySeq/Cauchy_minus.con.
286 inline cic:/CoRN/reals/CauchySeq/Lim_minus.con.
288 inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_mult.con.
290 inline cic:/CoRN/reals/CauchySeq/Cauchy_mult.con.
292 inline cic:/CoRN/reals/CauchySeq/Lim_mult.con.