]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/CoRN/reals/CauchySeq.mma
Stuff moved from old Matita.
[helm.git] / matita / matita / contribs / procedural / CoRN / reals / CauchySeq.mma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "CoRN.ma".
18
19 (* $Id: CauchySeq.v,v 1.8 2004/04/23 10:01:04 lcf Exp $ *)
20
21 (*#* printing IR %\ensuremath{\mathbb R}% *)
22
23 (*#* printing PartIR %\ensuremath{\mathbb R\!\not\rightarrow\!\mathbb R}% *)
24
25 (*#* printing ZeroR %\ensuremath{\mathbf0}% #0# *)
26
27 (*#* printing OneR %\ensuremath{\mathbf1}% #1# *)
28
29 (*#* printing AbsIR %\ensuremath{|\cdot|_{\mathbb R}}% *)
30
31 include "reals/CReals.ma".
32
33 (*#* *Real Number Structures
34 %\begin{convention}% Let [IR] be a structure for real numbers.
35 %\end{convention}%
36 *)
37
38 (*
39 Require Export R_CReals.
40 Definition IR : CReals := Concrete_R.
41 Opaque IR.
42 *)
43
44 inline procedural "cic:/CoRN/reals/CauchySeq/IR.con".
45
46 (* NOTATION
47 Notation PartIR := (PartFunct IR).
48 *)
49
50 (* NOTATION
51 Notation ProjIR1 := (prj1 IR _ _ _).
52 *)
53
54 (* NOTATION
55 Notation ProjIR2 := (prj2 IR _ _ _).
56 *)
57
58 include "tactics/Transparent_algebra.ma".
59
60 (* begin hide *)
61
62 (* NOTATION
63 Notation ZeroR := (Zero:IR).
64 *)
65
66 (* NOTATION
67 Notation OneR := (One:IR).
68 *)
69
70 (* end hide *)
71
72 (* UNEXPORTED
73 Section CReals_axioms
74 *)
75
76 (*#* ** [CReals] axioms *)
77
78 inline procedural "cic:/CoRN/reals/CauchySeq/CReals_is_CReals.con" as lemma.
79
80 (*#* First properties which follow trivially from the axioms.  *)
81
82 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_Cauchy.con" as lemma.
83
84 inline procedural "cic:/CoRN/reals/CauchySeq/Archimedes.con" as lemma.
85
86 inline procedural "cic:/CoRN/reals/CauchySeq/Archimedes'.con" as lemma.
87
88 (*#* A stronger version, which often comes in useful.  *)
89
90 inline procedural "cic:/CoRN/reals/CauchySeq/str_Archimedes.con" as lemma.
91
92 inline procedural "cic:/CoRN/reals/CauchySeq/CauchySeqR.con" as definition.
93
94 (* UNEXPORTED
95 End CReals_axioms
96 *)
97
98 (* UNEXPORTED
99 Section Cauchy_Defs
100 *)
101
102 (*#* ** Cauchy sequences
103 *** Alternative definitions
104 This section gives several definitions of Cauchy sequences. There
105 are no lemmas in this section.
106
107 The current definition of Cauchy ([Cauchy_prop]) is:
108
109 %\[\forall \epsilon>0. \exists N. \forall m\geq N. |seq_m - seq_N|\leq\varepsilon\]%
110 #for all e>0 there exists N such that for all m≥ N |seqm-seqN|≤ e#
111
112 Variant 1 of Cauchy ([Cauchy_prop1]) is:
113
114 %\[\forall k. \exists N. \forall m \geq N. |seq_m - seq_N|\leq1/(k+1)\]%
115 #for all k there exists N such that for all m ≥ N |seqm-seqN| ≤ 1/(k+1)#
116
117 In all of the following variants the limit occurs in the definition.
118 Therefore it is useful to define an auxiliary predicate
119 [Cauchy_Lim_prop?], in terms of which [Cauchy_prop?] is defined.
120
121 Variant 2 of Cauchy ([Cauchy_prop2]) is [exists y, (Cauchy_Lim_prop2 seq y)]
122 where
123 [[
124 Cauchy_Lim_prop2 seq y := forall eps [>] Zero, exists N, forall m >= N, (AbsIR seq m - y) [<=] eps
125 ]]
126
127 Note that [Cauchy_Lim_prop2] equals [seqLimit].
128
129 Variant 3 of Cauchy ([Cauchy_prop3]) reads [exists y, (Cauchy_Lim_prop3 seq y)]
130 where
131 [[
132 Cauchy_Lim_prop3 seq y := forall k, exists N, forall m >= N, (AbsIR seq m - y) [<=] One[/] (k[+]1)
133 ]]
134
135 The following variant is more restricted.
136
137 Variant 4 of Cauchy ([Cauchy_prop4]): [exists y, (Cauchy_Lim_prop4 seq y)]
138 where
139 [[
140 Cauchy_Lim_prop4 seq y := forall k, (AbsIR seq m - y) [<=] One[/] (k[+]1)
141 ]]
142
143 So
144 [[
145 Cauchy_prop4 -> Cauchy_prop3 Iff Cauchy_prop2 Iff Cauchy_prop1 Iff Cauchy_prop
146 ]]
147 Note: we don't know which formulations are useful.
148
149 The inequalities are stated with [[<=]] rather than with [<] for the
150 following reason: both formulations are equivalent, as is well known;
151 and [[<=]] being a negative statement, this makes proofs
152 sometimes easier and program extraction much more efficient.
153 *)
154
155 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop1.con" as definition.
156
157 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2.con" as definition.
158
159 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop2.con" as definition.
160
161 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3.con" as definition.
162
163 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop3.con" as definition.
164
165 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4.con" as definition.
166
167 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop4.con" as definition.
168
169 (* UNEXPORTED
170 End Cauchy_Defs
171 *)
172
173 (* UNEXPORTED
174 Section Inequalities
175 *)
176
177 (*#* *** Inequalities of Limits
178
179 The next lemma is equal to lemma [Lim_Cauchy].  *)
180
181 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_complete.con" as lemma.
182
183 inline procedural "cic:/CoRN/reals/CauchySeq/less_Lim_so_less_seq.con" as lemma.
184
185 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_less_so_seq_less.con" as lemma.
186
187 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_less_Lim_so_seq_less_seq.con" as lemma.
188
189 (*#* The next lemma follows from [less_Lim_so_less_seq] with [y := (y[+] (Lim seq)) [/]TwoNZ].  *)
190
191 inline procedural "cic:/CoRN/reals/CauchySeq/less_Lim_so.con" as lemma.
192
193 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_less_so.con" as lemma.
194
195 inline procedural "cic:/CoRN/reals/CauchySeq/leEq_seq_so_leEq_Lim.con" as lemma.
196
197 inline procedural "cic:/CoRN/reals/CauchySeq/str_leEq_seq_so_leEq_Lim.con" as lemma.
198
199 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_leEq_Lim.con" as lemma.
200
201 inline procedural "cic:/CoRN/reals/CauchySeq/seq_leEq_so_Lim_leEq.con" as lemma.
202
203 inline procedural "cic:/CoRN/reals/CauchySeq/str_seq_leEq_so_Lim_leEq.con" as lemma.
204
205 inline procedural "cic:/CoRN/reals/CauchySeq/Limits_unique.con" as lemma.
206
207 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_wd.con" as lemma.
208
209 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_strext.con" as lemma.
210
211 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap.con" as lemma.
212
213 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap'.con" as lemma.
214
215 (* UNEXPORTED
216 End Inequalities
217 *)
218
219 (* UNEXPORTED
220 Section Equiv_Cauchy
221 *)
222
223 (*#* *** Equivalence of formulations of Cauchy *)
224
225 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop1_prop.con" as lemma.
226
227 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop2_prop.con" as lemma.
228
229 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3_prop2.con" as lemma.
230
231 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop2.con" as lemma.
232
233 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop.con" as lemma.
234
235 inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq1.con" as definition.
236
237 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop3.con" as lemma.
238
239 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop2.con" as lemma.
240
241 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop3.con" as lemma.
242
243 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop.con" as lemma.
244
245 inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq4.con" as definition.
246
247 inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq4_y.con" as definition.
248
249 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_CauchySeq4.con" as lemma.
250
251 inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq2.con" as definition.
252
253 inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq2_y.con" as definition.
254
255 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_CauchySeq2.con" as lemma.
256
257 (*#* Well definedness. *)
258
259 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop_wd.con" as lemma.
260
261 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2_wd.con" as lemma.
262
263 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_wd'.con" as lemma.
264
265 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_unique.con" as lemma.
266
267 (* UNEXPORTED
268 End Equiv_Cauchy
269 *)
270
271 (* UNEXPORTED
272 Section Cauchy_props
273 *)
274
275 (*#* *** Properties of Cauchy sequences
276
277 Some of these lemmas are now obsolete, because they were reproved for arbitrary ordered fields$\ldots$#...#
278
279 We begin by defining the constant sequence and proving that it is Cauchy with the expected limit.
280 *)
281
282 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_const.con" as definition.
283
284 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_const.con" as lemma.
285
286 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_plus.con" as lemma.
287
288 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_plus.con" as lemma.
289
290 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_plus.con" as lemma.
291
292 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_inv.con" as lemma.
293
294 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_inv.con" as lemma.
295
296 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_inv.con" as lemma.
297
298 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_minus.con" as lemma.
299
300 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_minus.con" as lemma.
301
302 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_minus.con" as lemma.
303
304 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_mult.con" as lemma.
305
306 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_mult.con" as lemma.
307
308 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_mult.con" as lemma.
309
310 (* UNEXPORTED
311 End Cauchy_props
312 *)
313