helm/software/matita/contribs/CoRN-Decl/ftc/Partitions.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/ftc/Partitions".
  18
  19 (* $Id: Partitions.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *)
  20
  21 (* INCLUDE
  22 Continuity
  23 *)
  24
  25 (*#* printing Partition_Sum %\ensuremath{\sum_P}% #&sum;<sub>P</sub># *)
  26
  27 (* UNEXPORTED
  28 Section Definitions.
  29 *)
  30
  31 (*#* *Partitions
  32
  33 We now begin to lay the way for the definition of Riemann integral.  This will
  34 be done through the definition of a sequence of
  35 sums that is proved to be convergent; in order to do that, we first
  36 need to do a bit of work on partitions.
  37
  38 **Definitions
  39
  40 A partition is defined as a record type.  For each compact interval [[a,b]]
  41 and each natural number [n], a partition of [[a,b]] with [n+1] points is a
  42 choice of real numbers [a [=] a0 [<=] a1 [<=] an [=] b]; the following
  43 specification works as follows:
  44  - [Pts] is the function that chooses the points (it is declared as a
  45 coercion);
  46  - [prf1] states that [Pts] is a setoid function;
  47  - [prf2] states that the points are ordered;
  48  - [start] requires that [a0 [=] a] and
  49  - [finish] requires that [an [=] b].
  50
  51 *)
  52
  53 inline cic:/CoRN/ftc/Partitions/Partition.ind.
  54
  55 (*#* Two immediate consequences of this are that [ai [<=] aj] whenever
  56 [i < j] and that [ai] is in [[a,b]] for all [i].
  57 *)
  58
  59 inline cic:/CoRN/ftc/Partitions/Partition_mon.con.
  60
  61 inline cic:/CoRN/ftc/Partitions/Partition_in_compact.con.
  62
  63 (*#*
  64 Each partition of [[a,b]] implies a partition of the interval
  65 $[a,a_{n-1}]$#[a,a<sub>n-1</sub>]#.  This partition will play an
  66 important role in much of our future work, so we take some care to
  67 define it.
  68 *)
  69
  70 inline cic:/CoRN/ftc/Partitions/part_pred_lemma.con.
  71
  72 inline cic:/CoRN/ftc/Partitions/Partition_Dom.con.
  73
  74 (*#*
  75 The mesh of a partition is the greatest distance between two
  76 consecutive points.  For convenience's sake we also define the dual
  77 concept, which is very helpful in some situations.  In order to do
  78 this, we begin by building a list with all the distances between
  79 consecutive points; next we only need to extract the maximum and the
  80 minimum of this list. Notice that this list is nonempty except in the
  81 case when [a [=] b] and [n = 0]; this means that the convention we took
  82 of defining the minimum and maximum of the empty list to be [0] actually
  83 helps us in this case.
  84 *)
  85
  86 inline cic:/CoRN/ftc/Partitions/Part_Mesh_List.con.
  87
  88 inline cic:/CoRN/ftc/Partitions/Mesh.con.
  89
  90 inline cic:/CoRN/ftc/Partitions/AntiMesh.con.
  91
  92 (*#*
  93 Even partitions (partitions where all the points are evenly spaced)
  94 will also play a central role in our work; the first two lemmas are
  95 presented simply to make the definition of even partition lighter.
  96 *)
  97
  98 inline cic:/CoRN/ftc/Partitions/even_part_1.con.
  99
 100 inline cic:/CoRN/ftc/Partitions/even_part_2.con.
 101
 102 inline cic:/CoRN/ftc/Partitions/Even_Partition.con.
 103
 104 (* UNEXPORTED
 105 Section Refinements.
 106 *)
 107
 108 inline cic:/CoRN/ftc/Partitions/a.var.
 109
 110 inline cic:/CoRN/ftc/Partitions/b.var.
 111
 112 inline cic:/CoRN/ftc/Partitions/Hab.var.
 113
 114 inline cic:/CoRN/ftc/Partitions/m.var.
 115
 116 inline cic:/CoRN/ftc/Partitions/n.var.
 117
 118 inline cic:/CoRN/ftc/Partitions/P.var.
 119
 120 inline cic:/CoRN/ftc/Partitions/Q.var.
 121
 122 (*#*
 123 We now define what it means for a partition [Q] to be a refinement of
 124 [P] and prove the main property of refinements.
 125 *)
 126
 127 inline cic:/CoRN/ftc/Partitions/Refinement.con.
 128
 129 inline cic:/CoRN/ftc/Partitions/Refinement_prop.con.
 130
 131 (*#*
 132 We will also need to consider arbitrary sums %of the form
 133 \[\sum_{i=0}^{n-1}f(x_i)(a_{i+1}-a_i)\]%#of
 134 f(x<sub>i</sub>)(a<sub>i+1</sub>-a<sub>i</sub>)# where
 135 $x_i\in[a_i,a_{i+1}]$#x<sub>i</sub>&isin;[a<sub>i</sub>,a<sub>i+1</sub>]#.
 136 For this, we again need a choice function [x] which has to satisfy
 137 some condition.  We define the condition and the sum for a fixed [P]:
 138 *)
 139
 140 inline cic:/CoRN/ftc/Partitions/Points_in_Partition.con.
 141
 142 inline cic:/CoRN/ftc/Partitions/Pts_part_lemma.con.
 143
 144 inline cic:/CoRN/ftc/Partitions/Partition_Sum.con.
 145
 146 (* UNEXPORTED
 147 End Refinements.
 148 *)
 149
 150 (* UNEXPORTED
 151 Implicit Arguments Points_in_Partition [a b Hab n].
 152 *)
 153
 154 (* UNEXPORTED
 155 Implicit Arguments Partition_Sum [a b Hab n P g F].
 156 *)
 157
 158 (*#* **Constructions
 159
 160 We now formalize some trivial and helpful constructions.
 161
 162 %\begin{convention}% We will assume a fixed compact interval [[a,b]], denoted by [I].
 163 %\end{convention}%
 164 *)
 165
 166 inline cic:/CoRN/ftc/Partitions/a.var.
 167
 168 inline cic:/CoRN/ftc/Partitions/b.var.
 169
 170 inline cic:/CoRN/ftc/Partitions/Hab.var.
 171
 172 (* begin hide *)
 173
 174 inline cic:/CoRN/ftc/Partitions/I.con.
 175
 176 (* end hide *)
 177
 178 (* UNEXPORTED
 179 Section Getting_Points.
 180 *)
 181
 182 (*#*
 183 From a partition we always have a canonical choice of points at which
 184 to evaluate a function: just take all but the last points of the
 185 partition.
 186
 187 %\begin{convention}% Let [Q] be a partition of [I] with [m] points.
 188 %\end{convention}%
 189 *)
 190
 191 inline cic:/CoRN/ftc/Partitions/m.var.
 192
 193 inline cic:/CoRN/ftc/Partitions/Q.var.
 194
 195 inline cic:/CoRN/ftc/Partitions/Partition_imp_points.con.
 196
 197 inline cic:/CoRN/ftc/Partitions/Partition_imp_points_1.con.
 198
 199 inline cic:/CoRN/ftc/Partitions/Partition_imp_points_2.con.
 200
 201 (* UNEXPORTED
 202 End Getting_Points.
 203 *)
 204
 205 (*#*
 206 As a corollary, given any continuous function [F] and a natural number we have an immediate choice of a sum of [F] in [[a,b]].
 207 *)
 208
 209 inline cic:/CoRN/ftc/Partitions/F.var.
 210
 211 inline cic:/CoRN/ftc/Partitions/contF.var.
 212
 213 inline cic:/CoRN/ftc/Partitions/Even_Partition_Sum.con.
 214
 215 (* UNEXPORTED
 216 End Definitions.
 217 *)
 218
 219 (* UNEXPORTED
 220 Implicit Arguments Partition [a b].
 221 *)
 222
 223 (* UNEXPORTED
 224 Implicit Arguments Partition_Dom [a b Hab n].
 225 *)
 226
 227 (* UNEXPORTED
 228 Implicit Arguments Mesh [a b Hab n].
 229 *)
 230
 231 (* UNEXPORTED
 232 Implicit Arguments AntiMesh [a b Hab n].
 233 *)
 234
 235 (* UNEXPORTED
 236 Implicit Arguments Pts [a b Hab lng].
 237 *)
 238
 239 (* UNEXPORTED
 240 Implicit Arguments Part_Mesh_List [n a b Hab].
 241 *)
 242
 243 (* UNEXPORTED
 244 Implicit Arguments Points_in_Partition [a b Hab n].
 245 *)
 246
 247 (* UNEXPORTED
 248 Implicit Arguments Partition_Sum [a b Hab n P g F].
 249 *)
 250
 251 (* UNEXPORTED
 252 Implicit Arguments Even_Partition [a b].
 253 *)
 254
 255 (* UNEXPORTED
 256 Implicit Arguments Even_Partition_Sum [a b].
 257 *)
 258
 259 (* UNEXPORTED
 260 Implicit Arguments Refinement [a b Hab n m].
 261 *)
 262
 263 (* UNEXPORTED
 264 Hint Resolve start finish: algebra.
 265 *)
 266
 267 (* UNEXPORTED
 268 Section Lemmas.
 269 *)
 270
 271 (*#* ** Properties of the mesh
 272
 273 If a partition has more than one point then its mesh list is nonempty.
 274 *)
 275
 276 inline cic:/CoRN/ftc/Partitions/length_Part_Mesh_List.con.
 277
 278 (*#*
 279 Any element of the auxiliary list defined to calculate the mesh of a partition has a very specific form.
 280 *)
 281
 282 inline cic:/CoRN/ftc/Partitions/Part_Mesh_List_lemma.con.
 283
 284 (*#*
 285 Mesh and antimesh are always nonnegative.
 286 *)
 287
 288 inline cic:/CoRN/ftc/Partitions/Mesh_nonneg.con.
 289
 290 inline cic:/CoRN/ftc/Partitions/AntiMesh_nonneg.con.
 291
 292 (*#*
 293 Most important, [AntiMesh] and [Mesh] provide lower and upper bounds
 294 for the distance between any two consecutive points in a partition.
 295
 296 %\begin{convention}% Let [I] be [[a,b]] and [P] be a partition of [I]
 297 with [n] points.
 298 %\end{convention}%
 299 *)
 300
 301 inline cic:/CoRN/ftc/Partitions/a.var.
 302
 303 inline cic:/CoRN/ftc/Partitions/b.var.
 304
 305 (* begin hide *)
 306
 307 inline cic:/CoRN/ftc/Partitions/I.con.
 308
 309 (* end hide *)
 310
 311 inline cic:/CoRN/ftc/Partitions/Hab.var.
 312
 313 inline cic:/CoRN/ftc/Partitions/n.var.
 314
 315 inline cic:/CoRN/ftc/Partitions/P.var.
 316
 317 inline cic:/CoRN/ftc/Partitions/Mesh_lemma.con.
 318
 319 inline cic:/CoRN/ftc/Partitions/AntiMesh_lemma.con.
 320
 321 inline cic:/CoRN/ftc/Partitions/Mesh_leEq.con.
 322
 323 (* UNEXPORTED
 324 End Lemmas.
 325 *)
 326
 327 (* UNEXPORTED
 328 Section Even_Partitions.
 329 *)
 330
 331 (*#* More technical stuff.  Two equal partitions have the same mesh.
 332 *)
 333
 334 inline cic:/CoRN/ftc/Partitions/Mesh_wd.con.
 335
 336 inline cic:/CoRN/ftc/Partitions/Mesh_wd'.con.
 337
 338 (*#*
 339 The mesh of an even partition is easily calculated.
 340 *)
 341
 342 inline cic:/CoRN/ftc/Partitions/even_partition_Mesh.con.
 343
 344 (*#* ** Miscellaneous
 345 %\begin{convention}% Throughout this section, let [a,b:IR] and [I] be [[a,b]].
 346 %\end{convention}%
 347 *)
 348
 349 inline cic:/CoRN/ftc/Partitions/a.var.
 350
 351 inline cic:/CoRN/ftc/Partitions/b.var.
 352
 353 (* begin hide *)
 354
 355 inline cic:/CoRN/ftc/Partitions/I.con.
 356
 357 (* end hide *)
 358
 359 inline cic:/CoRN/ftc/Partitions/Hab.var.
 360
 361 (*#*
 362 An interesting property: in a partition, if [ai [<] aj] then [i < j].
 363 *)
 364
 365 inline cic:/CoRN/ftc/Partitions/Partition_Points_mon.con.
 366
 367 inline cic:/CoRN/ftc/Partitions/refinement_resp_mult.con.
 368
 369 (*#*
 370 %\begin{convention}% Assume [m,n] are positive natural numbers and
 371 denote by [P] and [Q] the even partitions with, respectively, [m] and
 372 [n] points.
 373 %\end{convention}%
 374
 375 Even partitions always have a common refinement.
 376 *)
 377
 378 inline cic:/CoRN/ftc/Partitions/m.var.
 379
 380 inline cic:/CoRN/ftc/Partitions/n.var.
 381
 382 inline cic:/CoRN/ftc/Partitions/Hm.var.
 383
 384 inline cic:/CoRN/ftc/Partitions/Hn.var.
 385
 386 (* begin hide *)
 387
 388 inline cic:/CoRN/ftc/Partitions/P.con.
 389
 390 inline cic:/CoRN/ftc/Partitions/Q.con.
 391
 392 (* end hide *)
 393
 394 inline cic:/CoRN/ftc/Partitions/even_partition_refinement.con.
 395
 396 (* UNEXPORTED
 397 End Even_Partitions.
 398 *)
 399
 400 (* UNEXPORTED
 401 Section More_Definitions.
 402 *)
 403
 404 (*#* ** Separation
 405
 406 Some auxiliary definitions.  A partition is said to be separated if all its points are distinct.
 407 *)
 408
 409 inline cic:/CoRN/ftc/Partitions/a.var.
 410
 411 inline cic:/CoRN/ftc/Partitions/b.var.
 412
 413 inline cic:/CoRN/ftc/Partitions/Hab.var.
 414
 415 inline cic:/CoRN/ftc/Partitions/_Separated.con.
 416
 417 (*#*
 418 Two partitions are said to be (mutually) separated if they are both
 419 separated and all their points are distinct (except for the
 420 endpoints).
 421
 422 %\begin{convention}% Let [P,Q] be partitions of [I] with,
 423 respectively, [n] and [m] points.
 424 %\end{convention}%
 425 *)
 426
 427 inline cic:/CoRN/ftc/Partitions/n.var.
 428
 429 inline cic:/CoRN/ftc/Partitions/m.var.
 430
 431 inline cic:/CoRN/ftc/Partitions/P.var.
 432
 433 inline cic:/CoRN/ftc/Partitions/Q.var.
 434
 435 inline cic:/CoRN/ftc/Partitions/Separated.con.
 436
 437 (* UNEXPORTED
 438 End More_Definitions.
 439 *)
 440
 441 (* UNEXPORTED
 442 Implicit Arguments _Separated [a b Hab n].
 443 *)
 444
 445 (* UNEXPORTED
 446 Implicit Arguments Separated [a b Hab n m].
 447 *)
 448
 449 (* UNEXPORTED
 450 Section Sep_Partitions.
 451 *)
 452
 453 inline cic:/CoRN/ftc/Partitions/a.var.
 454
 455 inline cic:/CoRN/ftc/Partitions/b.var.
 456
 457 (* begin hide *)
 458
 459 inline cic:/CoRN/ftc/Partitions/I.con.
 460
 461 (* end hide *)
 462
 463 inline cic:/CoRN/ftc/Partitions/Hab.var.
 464
 465 (*#*
 466 The antimesh of a separated partition is always positive.
 467 *)
 468
 469 inline cic:/CoRN/ftc/Partitions/pos_AntiMesh.con.
 470
 471 (*#*
 472 A partition can have only one point iff the endpoints of the interval
 473 are the same; moreover, if the partition is separated and the
 474 endpoints of the interval are the same then it must have one point.
 475 *)
 476
 477 inline cic:/CoRN/ftc/Partitions/partition_length_zero.con.
 478
 479 inline cic:/CoRN/ftc/Partitions/_Separated_imp_length_zero.con.
 480
 481 inline cic:/CoRN/ftc/Partitions/partition_less_imp_gt_zero.con.
 482
 483 (* UNEXPORTED
 484 End Sep_Partitions.
 485 *)
 486