matita/contribs/CoRN-Decl/reals/CauchySeq.ma

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