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