helm/software/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&gt;0 there exists N such that for all m&ge; N |seqm-seqN|&le; 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 &ge; N |seqm-seqN| &le; 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