helm/software/matita/contribs/procedural/CoRN/algebra/COrdCauchy.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 include "algebra/COrdAbs.ma".
  20
  21 (* Begin_SpecReals *)
  22
  23 (* UNEXPORTED
  24 Section OrdField_Cauchy
  25 *)
  26
  27 (*#* **Cauchy sequences
  28 %\begin{convention}% Let [R] be an ordered field.
  29 %\end{convention}%
  30 *)
  31
  32 (* UNEXPORTED
  33 cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/R.var
  34 *)
  35
  36 (* begin hide *)
  37
  38 (* UNEXPORTED
  39 Set Implicit Arguments.
  40 *)
  41
  42 (* UNEXPORTED
  43 Unset Strict Implicit.
  44 *)
  45
  46 (* end hide *)
  47
  48 inline procedural "cic:/CoRN/algebra/COrdCauchy/Cauchy_prop.con" as definition.
  49
  50 (* begin hide *)
  51
  52 (* UNEXPORTED
  53 Set Strict Implicit.
  54 *)
  55
  56 (* UNEXPORTED
  57 Unset Implicit Arguments.
  58 *)
  59
  60 (* end hide *)
  61
  62 (* Def. CauchyP, Build_CauchyP *)
  63
  64 (* Should be defined in terms of CauchyP *)
  65
  66 (*#*
  67 Implicit arguments turned off, because Coq makes a mess of it in combination
  68 with the coercions
  69 *)
  70
  71 inline procedural "cic:/CoRN/algebra/COrdCauchy/CauchySeq.ind".
  72
  73 (* COERCION
  74 cic:/matita/CoRN-Procedural/algebra/COrdCauchy/CS_seq.con
  75 *)
  76
  77 inline procedural "cic:/CoRN/algebra/COrdCauchy/SeqLimit.con" as definition.
  78
  79 (* End_SpecReals *)
  80
  81 (*#*
  82 We now prove that the property of being a Cauchy sequence is preserved
  83 through the usual algebraic operations (addition, subtraction and
  84 multiplication -- and division, provided some additional conditions
  85 hold).
  86
  87 %\begin{convention}% Let [R] be an ordered field.
  88 %\end{convention}%
  89 *)
  90
  91 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_bounded.con" as theorem.
  92
  93 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_const.con" as lemma.
  94
  95 (*#*
  96 %\begin{convention}% Assume [f] and [g] are Cauchy sequences on [R].
  97 %\end{convention}%
  98 *)
  99
 100 (* UNEXPORTED
 101 cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/f.var
 102 *)
 103
 104 (* UNEXPORTED
 105 cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/g.var
 106 *)
 107
 108 (* UNEXPORTED
 109 cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/Hf.var
 110 *)
 111
 112 (* UNEXPORTED
 113 cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/Hg.var
 114 *)
 115
 116 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_plus.con" as lemma.
 117
 118 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_inv.con" as lemma.
 119
 120 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_mult.con" as lemma.
 121
 122 (*#*
 123 We now assume that [f] is, from some point onwards, greater than
 124 some positive number.  The sequence of reciprocals is defined as
 125 being constantly one up to that point, and the sequence of
 126 reciprocals from then onwards.
 127
 128 %\begin{convention}%
 129 Let [e] be a postive element of [R] and let [N:nat] be such that from
 130 [N] onwards, [(f n) [#] Zero]
 131 %\end{convention}%
 132 *)
 133
 134 (* UNEXPORTED
 135 cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/e.var
 136 *)
 137
 138 (* UNEXPORTED
 139 cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/He.var
 140 *)
 141
 142 (* UNEXPORTED
 143 cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/N.var
 144 *)
 145
 146 (* UNEXPORTED
 147 cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/f_bnd.var
 148 *)
 149
 150 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_recip_def.con" as lemma.
 151
 152 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_recip_seq.con" as definition.
 153
 154 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_recip.con" as lemma.
 155
 156 (* UNEXPORTED
 157 End OrdField_Cauchy
 158 *)
 159
 160 (* UNEXPORTED
 161 Implicit Arguments SeqLimit [R].
 162 *)
 163
 164 (*#*
 165 The following lemma does not require the sequence to be Cauchy, but it fits
 166 well here anyway.
 167 *)
 168
 169 inline procedural "cic:/CoRN/algebra/COrdCauchy/maj_upto_eps.con" as lemma.
 170
 171 (* UNEXPORTED
 172 Section Mult_AbsSmall
 173 *)
 174
 175 (* UNEXPORTED
 176 cic:/CoRN/algebra/COrdCauchy/Mult_AbsSmall/R.var
 177 *)
 178
 179 (*#*
 180 ** [AbsSmall] revisited
 181 %\begin{convention}% Let [R] be an ordered field.
 182 %\end{convention}%
 183 *)
 184
 185 inline procedural "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall'_rht.con" as lemma.
 186
 187 inline procedural "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall_rht.con" as lemma.
 188
 189 inline procedural "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall_lft.con" as lemma.
 190
 191 inline procedural "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall.con" as lemma.
 192
 193 (* UNEXPORTED
 194 End Mult_AbsSmall
 195 *)
 196
 197 (* UNEXPORTED
 198 Section Mult_Continuous
 199 *)
 200
 201 (* UNEXPORTED
 202 cic:/CoRN/algebra/COrdCauchy/Mult_Continuous/R.var
 203 *)
 204
 205 (*#*
 206 ** Multiplication is continuous
 207 %\begin{convention}% Let [R] be an ordered field.
 208 %\end{convention}%
 209 *)
 210
 211 inline procedural "cic:/CoRN/algebra/COrdCauchy/smaller.con" as lemma.
 212
 213 inline procedural "cic:/CoRN/algebra/COrdCauchy/estimate_abs.con" as lemma.
 214
 215 inline procedural "cic:/CoRN/algebra/COrdCauchy/mult_contin.con" as lemma.
 216
 217 (*#* Addition is also continuous. *)
 218
 219 inline procedural "cic:/CoRN/algebra/COrdCauchy/plus_contin.con" as lemma.
 220
 221 (* UNEXPORTED
 222 End Mult_Continuous
 223 *)
 224
 225 (* UNEXPORTED
 226 Section Monotonous_functions
 227 *)
 228
 229 (*#*
 230 ** Monotonous Functions
 231
 232 Finally, we study several properties of monotonous functions and
 233 characterize them in some way.
 234
 235 %\begin{convention}% Let [R] be an ordered field.
 236 %\end{convention}%
 237 *)
 238
 239 (* UNEXPORTED
 240 cic:/CoRN/algebra/COrdCauchy/Monotonous_functions/R.var
 241 *)
 242
 243 (*#*
 244 We begin by characterizing the preservation of less (less or equal)
 245 in terms of preservation of less or equal (less).
 246 *)
 247
 248 inline procedural "cic:/CoRN/algebra/COrdCauchy/resp_less_char'.con" as lemma.
 249
 250 inline procedural "cic:/CoRN/algebra/COrdCauchy/resp_less_char.con" as lemma.
 251
 252 inline procedural "cic:/CoRN/algebra/COrdCauchy/resp_leEq_char'.con" as lemma.
 253
 254 inline procedural "cic:/CoRN/algebra/COrdCauchy/resp_leEq_char.con" as lemma.
 255
 256 (*#*
 257 Next, we see different characterizations of monotonous functions from
 258 some subset of the natural numbers into [R].  Mainly, these
 259 amount (for different types of functions) to proving that a function
 260 is monotonous iff [f(i) [<] f(i+1)] for every [i].
 261
 262 Also, strictly monotonous functions are injective.
 263 *)
 264
 265 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon.con" as lemma.
 266
 267 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'.con" as lemma.
 268
 269 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'.con" as lemma.
 270
 271 inline procedural "cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'.con" as lemma.
 272
 273 inline procedural "cic:/CoRN/algebra/COrdCauchy/mon_imp_inj.con" as lemma.
 274
 275 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon_lt.con" as lemma.
 276
 277 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'_lt.con" as lemma.
 278
 279 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'_lt.con" as lemma.
 280
 281 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'2_lt.con" as lemma.
 282
 283 inline procedural "cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'_lt.con" as lemma.
 284
 285 inline procedural "cic:/CoRN/algebra/COrdCauchy/mon_imp_inj_lt.con" as lemma.
 286
 287 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon_le.con" as lemma.
 288
 289 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'_le.con" as lemma.
 290
 291 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'_le.con" as lemma.
 292
 293 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'2_le.con" as lemma.
 294
 295 inline procedural "cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'_le.con" as lemma.
 296
 297 inline procedural "cic:/CoRN/algebra/COrdCauchy/mon_imp_inj_le.con" as lemma.
 298
 299 (*#*
 300 A similar result for %{\em %partial%}% functions.
 301 *)
 302
 303 inline procedural "cic:/CoRN/algebra/COrdCauchy/part_mon_imp_mon'.con" as lemma.
 304
 305 (* UNEXPORTED
 306 End Monotonous_functions
 307 *)
 308