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