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