helm/software/matita/contribs/CoRN-Decl/algebra/COrdCauchy.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/algebra/COrdCauchy".
  18
  19 include "CoRN_notation.ma".
  20
  21 include "algebra/COrdAbs.ma".
  22
  23 (* Begin_SpecReals *)
  24
  25 (* UNEXPORTED
  26 Section OrdField_Cauchy.
  27 *)
  28
  29 (*#* **Cauchy sequences
  30 %\begin{convention}% Let [R] be an ordered field.
  31 %\end{convention}%
  32 *)
  33
  34 inline "cic:/CoRN/algebra/COrdCauchy/R.var".
  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 "cic:/CoRN/algebra/COrdCauchy/Cauchy_prop.con".
  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 "cic:/CoRN/algebra/COrdCauchy/CauchySeq.ind".
  72
  73 coercion "cic:/matita/CoRN-Decl/algebra/COrdCauchy/CS_seq.con" 0 (* compounds *).
  74
  75 inline "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 "cic:/CoRN/algebra/COrdCauchy/CS_seq_bounded.con".
  90
  91 inline "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 inline "cic:/CoRN/algebra/COrdCauchy/f.var".
  99
 100 inline "cic:/CoRN/algebra/COrdCauchy/g.var".
 101
 102 inline "cic:/CoRN/algebra/COrdCauchy/Hf.var".
 103
 104 inline "cic:/CoRN/algebra/COrdCauchy/Hg.var".
 105
 106 inline "cic:/CoRN/algebra/COrdCauchy/CS_seq_plus.con".
 107
 108 inline "cic:/CoRN/algebra/COrdCauchy/CS_seq_inv.con".
 109
 110 inline "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 inline "cic:/CoRN/algebra/COrdCauchy/e.var".
 125
 126 inline "cic:/CoRN/algebra/COrdCauchy/He.var".
 127
 128 inline "cic:/CoRN/algebra/COrdCauchy/N.var".
 129
 130 inline "cic:/CoRN/algebra/COrdCauchy/f_bnd.var".
 131
 132 inline "cic:/CoRN/algebra/COrdCauchy/CS_seq_recip_def.con".
 133
 134 inline "cic:/CoRN/algebra/COrdCauchy/CS_seq_recip_seq.con".
 135
 136 inline "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 "cic:/CoRN/algebra/COrdCauchy/maj_upto_eps.con".
 152
 153 (* UNEXPORTED
 154 Section Mult_AbsSmall.
 155 *)
 156
 157 inline "cic:/CoRN/algebra/COrdCauchy/R.var".
 158
 159 (*#*
 160 ** [AbsSmall] revisited
 161 %\begin{convention}% Let [R] be an ordered field.
 162 %\end{convention}%
 163 *)
 164
 165 inline "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall'_rht.con".
 166
 167 inline "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall_rht.con".
 168
 169 inline "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall_lft.con".
 170
 171 inline "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 inline "cic:/CoRN/algebra/COrdCauchy/R.var".
 182
 183 (*#*
 184 ** Multiplication is continuous
 185 %\begin{convention}% Let [R] be an ordered field.
 186 %\end{convention}%
 187 *)
 188
 189 inline "cic:/CoRN/algebra/COrdCauchy/smaller.con".
 190
 191 inline "cic:/CoRN/algebra/COrdCauchy/estimate_abs.con".
 192
 193 inline "cic:/CoRN/algebra/COrdCauchy/mult_contin.con".
 194
 195 (*#* Addition is also continuous. *)
 196
 197 inline "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 inline "cic:/CoRN/algebra/COrdCauchy/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 "cic:/CoRN/algebra/COrdCauchy/resp_less_char'.con".
 225
 226 inline "cic:/CoRN/algebra/COrdCauchy/resp_less_char.con".
 227
 228 inline "cic:/CoRN/algebra/COrdCauchy/resp_leEq_char'.con".
 229
 230 inline "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 "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon.con".
 242
 243 inline "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'.con".
 244
 245 inline "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'.con".
 246
 247 inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'.con".
 248
 249 inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_inj.con".
 250
 251 inline "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon_lt.con".
 252
 253 inline "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'_lt.con".
 254
 255 inline "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'_lt.con".
 256
 257 inline "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'2_lt.con".
 258
 259 inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'_lt.con".
 260
 261 inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_inj_lt.con".
 262
 263 inline "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon_le.con".
 264
 265 inline "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'_le.con".
 266
 267 inline "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'_le.con".
 268
 269 inline "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'2_le.con".
 270
 271 inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'_le.con".
 272
 273 inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_inj_le.con".
 274
 275 (*#*
 276 A similar result for %{\em %partial%}% functions.
 277 *)
 278
 279 inline "cic:/CoRN/algebra/COrdCauchy/part_mon_imp_mon'.con".
 280
 281 (* UNEXPORTED
 282 End Monotonous_functions.
 283 *)
 284