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