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