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