helm/software/matita/contribs/CoRN-Decl/reals/Intervals.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/Intervals".
  18
  19 (* $Id: Intervals.v,v 1.10 2004/04/23 10:01:04 lcf Exp $ *)
  20
  21 (* INCLUDE
  22 CSetoidInc
  23 *)
  24
  25 (* INCLUDE
  26 RealLists
  27 *)
  28
  29 (* UNEXPORTED
  30 Section Intervals.
  31 *)
  32
  33 (*#* * Intervals
  34 In this section we define (compact) intervals of the real line and
  35 some useful functions to work with them.
  36
  37 ** Definitions
  38
  39 We start by defining the compact interval [[a,b]] as being the set of
  40 points less or equal than [b] and greater or equal than [a].  We
  41 require [a [<=] b], as we want to work only in nonempty intervals.
  42 *)
  43
  44 inline cic:/CoRN/reals/Intervals/compact.con.
  45
  46 (*#*
  47 %\begin{convention}% Let [a,b : IR] and [Hab : a [<=] b].
  48 %\end{convention}%
  49
  50 As expected, both [a] and [b] are members of [[a,b]].  Also they are
  51 members of the interval [[Min(a,b),Max(a,b)]].
  52 *)
  53
  54 inline cic:/CoRN/reals/Intervals/a.var.
  55
  56 inline cic:/CoRN/reals/Intervals/b.var.
  57
  58 inline cic:/CoRN/reals/Intervals/Hab.var.
  59
  60 inline cic:/CoRN/reals/Intervals/compact_inc_lft.con.
  61
  62 inline cic:/CoRN/reals/Intervals/compact_inc_rht.con.
  63
  64 inline cic:/CoRN/reals/Intervals/compact_Min_lft.con.
  65
  66 inline cic:/CoRN/reals/Intervals/compact_Min_rht.con.
  67
  68 (*#*
  69 As we will be interested in taking functions with domain in a compact
  70 interval, we want this predicate to be well defined.
  71 *)
  72
  73 inline cic:/CoRN/reals/Intervals/compact_wd.con.
  74
  75 (*#*
  76 Also, it will sometimes be necessary to rewrite the endpoints of an interval.
  77 *)
  78
  79 inline cic:/CoRN/reals/Intervals/compact_wd'.con.
  80
  81 (*#*
  82 As we identify subsets with predicates, inclusion is simply implication.
  83 *)
  84
  85 (*#*
  86 Finally, we define a restriction operator that takes a function [F]
  87 and a well defined predicate [P] included in the domain of [F] and
  88 returns the restriction $F|_P$# of F to P#.
  89 *)
  90
  91 inline cic:/CoRN/reals/Intervals/Frestr.con.
  92
  93 (* UNEXPORTED
  94 End Intervals.
  95 *)
  96
  97 (* UNEXPORTED
  98 Implicit Arguments Frestr [F P].
  99 *)
 100
 101 (* UNEXPORTED
 102 Section More_Intervals.
 103 *)
 104
 105 inline cic:/CoRN/reals/Intervals/included_refl'.con.
 106
 107 (*#* We prove some inclusions of compact intervals.  *)
 108
 109 inline cic:/CoRN/reals/Intervals/compact_map1.con.
 110
 111 inline cic:/CoRN/reals/Intervals/compact_map2.con.
 112
 113 inline cic:/CoRN/reals/Intervals/compact_map3.con.
 114
 115 (* UNEXPORTED
 116 End More_Intervals.
 117 *)
 118
 119 (* UNEXPORTED
 120 Hint Resolve included_refl' compact_map1 compact_map2 compact_map3 : included.
 121 *)
 122
 123 (* UNEXPORTED
 124 Section Totally_Bounded.
 125 *)
 126
 127 (*#* ** Totally Bounded
 128
 129 Totally bounded sets will play an important role in what is
 130 to come.  The definition (equivalent to the classical one) states that
 131 [P] is totally bounded iff
 132 %\[\forall_{\varepsilon>0}\exists_{x_1,\ldots,x_n}\forall_{y\in P}
 133 \exists_{1\leq i\leq n}|y-x_i|<\varepsilon\]%#&forall;e&gt;0
 134 &exist;x<sub>1</sub>,...,x<sub>n</sub>&forall;y&isin;P&exist;
 135 1&le;i&le;n.|y-x<sub>i</sub>|&lt;e#.
 136
 137 Notice the use of lists for quantification.
 138 *)
 139
 140 inline cic:/CoRN/reals/Intervals/totally_bounded.con.
 141
 142 (*#*
 143 This definition is classically, but not constructively, equivalent to
 144 the definition of compact (if completeness is assumed); the next
 145 result, classically equivalent to the Heine-Borel theorem, justifies
 146 that we take the definition of totally bounded to be the relevant one
 147 and that we defined compacts as we did.
 148 *)
 149
 150 inline cic:/CoRN/reals/Intervals/compact_is_totally_bounded.con.
 151
 152 (*#*
 153 Suprema and infima will be needed throughout; we define them here both
 154 for arbitrary subsets of [IR] and for images of functions.
 155 *)
 156
 157 inline cic:/CoRN/reals/Intervals/set_glb_IR.con.
 158
 159 inline cic:/CoRN/reals/Intervals/set_lub_IR.con.
 160
 161 inline cic:/CoRN/reals/Intervals/fun_image.con.
 162
 163 inline cic:/CoRN/reals/Intervals/fun_glb_IR.con.
 164
 165 inline cic:/CoRN/reals/Intervals/fun_lub_IR.con.
 166
 167 (* begin hide *)
 168
 169 inline cic:/CoRN/reals/Intervals/aux_seq_lub.con.
 170
 171 inline cic:/CoRN/reals/Intervals/aux_seq_lub_prop.con.
 172
 173 (* end hide *)
 174
 175 (*#*
 176 The following are probably the most important results in this section.
 177 *)
 178
 179 inline cic:/CoRN/reals/Intervals/totally_bounded_has_lub.con.
 180
 181 (* begin hide *)
 182
 183 inline cic:/CoRN/reals/Intervals/aux_seq_glb.con.
 184
 185 inline cic:/CoRN/reals/Intervals/aux_seq_glb_prop.con.
 186
 187 (* end hide *)
 188
 189 inline cic:/CoRN/reals/Intervals/totally_bounded_has_glb.con.
 190
 191 (* UNEXPORTED
 192 End Totally_Bounded.
 193 *)
 194
 195 (* UNEXPORTED
 196 Section Compact.
 197 *)
 198
 199 (*#* ** Compact sets
 200
 201 In this section we dwell a bit farther into the definition of compactness
 202 and explore some of its properties.
 203
 204 The following characterization of inclusion can be very useful:
 205 *)
 206
 207 inline cic:/CoRN/reals/Intervals/included_compact.con.
 208
 209 (*#*
 210 At several points in our future development of a theory we will need
 211 to partition a compact interval in subintervals of length smaller than
 212 some predefined value [eps]. Although this seems a
 213 consequence of every compact interval being totally bounded, it is in
 214 fact a stronger property.  In this section we perform that
 215 construction (requiring the endpoints of the interval to be distinct)
 216 and prove some of its good properties.
 217
 218 %\begin{convention}% Let [a,b : IR], [Hab : (a [<=] b)] and denote by [I]
 219 the compact interval [[a,b]].  Also assume that [a [<] b], and let [e] be
 220 a positive real number.
 221 %\end{convention}%
 222 *)
 223
 224 inline cic:/CoRN/reals/Intervals/a.var.
 225
 226 inline cic:/CoRN/reals/Intervals/b.var.
 227
 228 inline cic:/CoRN/reals/Intervals/Hab.var.
 229
 230 (* begin hide *)
 231
 232 inline cic:/CoRN/reals/Intervals/I.con.
 233
 234 (* end hide *)
 235
 236 inline cic:/CoRN/reals/Intervals/Hab'.var.
 237
 238 inline cic:/CoRN/reals/Intervals/e.var.
 239
 240 inline cic:/CoRN/reals/Intervals/He.var.
 241
 242 (*#*
 243 We start by finding a natural number [n] such that [(b[-]a) [/] n [<] e].
 244 *)
 245
 246 inline cic:/CoRN/reals/Intervals/compact_nat.con.
 247
 248 (*#* Obviously such an [n] must be greater than zero.*)
 249
 250 inline cic:/CoRN/reals/Intervals/pos_compact_nat.con.
 251
 252 (*#*
 253 We now define a sequence on [n] points in [[a,b]] by
 254 [x_i [=] Min(a,b) [+]i[*] (b[-]a) [/]n] and
 255 prove that all of its points are really in that interval.
 256 *)
 257
 258 inline cic:/CoRN/reals/Intervals/compact_part.con.
 259
 260 inline cic:/CoRN/reals/Intervals/compact_part_hyp.con.
 261
 262 (*#*
 263 This sequence is strictly increasing and each two consecutive points
 264 are apart by less than [e].*)
 265
 266 inline cic:/CoRN/reals/Intervals/compact_less.con.
 267
 268 inline cic:/CoRN/reals/Intervals/compact_leEq.con.
 269
 270 (*#* When we proceed to integration, this lemma will also be useful: *)
 271
 272 inline cic:/CoRN/reals/Intervals/compact_partition_lemma.con.
 273
 274 (*#* The next lemma provides an upper bound for the distance between two points in an interval: *)
 275
 276 inline cic:/CoRN/reals/Intervals/compact_elements.con.
 277
 278 (* UNEXPORTED
 279 Opaque Min Max.
 280 *)
 281
 282 (*#* The following is a variation on the previous lemma: *)
 283
 284 inline cic:/CoRN/reals/Intervals/compact_elements'.con.
 285
 286 (*#* The following lemma is a bit more specific: it shows that we can
 287 also estimate the distance from the center of a compact interval to
 288 any of its points. *)
 289
 290 inline cic:/CoRN/reals/Intervals/compact_bnd_AbsIR.con.
 291
 292 (*#* Finally, two more useful lemmas to prove inclusion of compact
 293 intervals.  They will be necessary for the definition and proof of the
 294 elementary properties of the integral.  *)
 295
 296 inline cic:/CoRN/reals/Intervals/included2_compact.con.
 297
 298 inline cic:/CoRN/reals/Intervals/included3_compact.con.
 299
 300 (* UNEXPORTED
 301 End Compact.
 302 *)
 303
 304 (* UNEXPORTED
 305 Hint Resolve included_compact included2_compact included3_compact : included.
 306 *)
 307