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