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 include "CoRN.ma".
  20
  21 (* $Id: Partitions.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *)
  22
  23 include "ftc/Continuity.ma".
  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 coercion cic:/matita/CoRN-Decl/ftc/Partitions/Pts.con 0 (* compounds *).
  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 "cic:/CoRN/ftc/Partitions/Partition_mon.con".
  62
  63 inline "cic:/CoRN/ftc/Partitions/Partition_in_compact.con".
  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 "cic:/CoRN/ftc/Partitions/part_pred_lemma.con".
  73
  74 inline "cic:/CoRN/ftc/Partitions/Partition_Dom.con".
  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 "cic:/CoRN/ftc/Partitions/Part_Mesh_List.con".
  89
  90 inline "cic:/CoRN/ftc/Partitions/Mesh.con".
  91
  92 inline "cic:/CoRN/ftc/Partitions/AntiMesh.con".
  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 "cic:/CoRN/ftc/Partitions/even_part_1.con".
 101
 102 inline "cic:/CoRN/ftc/Partitions/even_part_2.con".
 103
 104 inline "cic:/CoRN/ftc/Partitions/Even_Partition.con".
 105
 106 (* UNEXPORTED
 107 Section Refinements
 108 *)
 109
 110 alias id "a" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/a.var".
 111
 112 alias id "b" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/b.var".
 113
 114 alias id "Hab" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/Hab.var".
 115
 116 alias id "m" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/m.var".
 117
 118 alias id "n" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/n.var".
 119
 120 alias id "P" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/P.var".
 121
 122 alias id "Q" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/Q.var".
 123
 124 (*#*
 125 We now define what it means for a partition [Q] to be a refinement of
 126 [P] and prove the main property of refinements.
 127 *)
 128
 129 inline "cic:/CoRN/ftc/Partitions/Refinement.con".
 130
 131 inline "cic:/CoRN/ftc/Partitions/Refinement_prop.con".
 132
 133 (*#*
 134 We will also need to consider arbitrary sums %of the form
 135 \[\sum_{i=0}^{n-1}f(x_i)(a_{i+1}-a_i)\]%#of
 136 f(x<sub>i</sub>)(a<sub>i+1</sub>-a<sub>i</sub>)# where
 137 $x_i\in[a_i,a_{i+1}]$#x<sub>i</sub>&isin;[a<sub>i</sub>,a<sub>i+1</sub>]#.
 138 For this, we again need a choice function [x] which has to satisfy
 139 some condition.  We define the condition and the sum for a fixed [P]:
 140 *)
 141
 142 inline "cic:/CoRN/ftc/Partitions/Points_in_Partition.con".
 143
 144 inline "cic:/CoRN/ftc/Partitions/Pts_part_lemma.con".
 145
 146 inline "cic:/CoRN/ftc/Partitions/Partition_Sum.con".
 147
 148 (* UNEXPORTED
 149 End Refinements
 150 *)
 151
 152 (* UNEXPORTED
 153 Implicit Arguments Points_in_Partition [a b Hab n].
 154 *)
 155
 156 (* UNEXPORTED
 157 Implicit Arguments Partition_Sum [a b Hab n P g F].
 158 *)
 159
 160 (*#* **Constructions
 161
 162 We now formalize some trivial and helpful constructions.
 163
 164 %\begin{convention}% We will assume a fixed compact interval [[a,b]], denoted by [I].
 165 %\end{convention}%
 166 *)
 167
 168 alias id "a" = "cic:/CoRN/ftc/Partitions/Definitions/a.var".
 169
 170 alias id "b" = "cic:/CoRN/ftc/Partitions/Definitions/b.var".
 171
 172 alias id "Hab" = "cic:/CoRN/ftc/Partitions/Definitions/Hab.var".
 173
 174 (* begin hide *)
 175
 176 inline "cic:/CoRN/ftc/Partitions/Definitions/I.con" "Definitions__".
 177
 178 (* end hide *)
 179
 180 (* UNEXPORTED
 181 Section Getting_Points
 182 *)
 183
 184 (*#*
 185 From a partition we always have a canonical choice of points at which
 186 to evaluate a function: just take all but the last points of the
 187 partition.
 188
 189 %\begin{convention}% Let [Q] be a partition of [I] with [m] points.
 190 %\end{convention}%
 191 *)
 192
 193 alias id "m" = "cic:/CoRN/ftc/Partitions/Definitions/Getting_Points/m.var".
 194
 195 alias id "Q" = "cic:/CoRN/ftc/Partitions/Definitions/Getting_Points/Q.var".
 196
 197 inline "cic:/CoRN/ftc/Partitions/Partition_imp_points.con".
 198
 199 inline "cic:/CoRN/ftc/Partitions/Partition_imp_points_1.con".
 200
 201 inline "cic:/CoRN/ftc/Partitions/Partition_imp_points_2.con".
 202
 203 (* UNEXPORTED
 204 End Getting_Points
 205 *)
 206
 207 (*#*
 208 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]].
 209 *)
 210
 211 alias id "F" = "cic:/CoRN/ftc/Partitions/Definitions/F.var".
 212
 213 alias id "contF" = "cic:/CoRN/ftc/Partitions/Definitions/contF.var".
 214
 215 inline "cic:/CoRN/ftc/Partitions/Even_Partition_Sum.con".
 216
 217 (* UNEXPORTED
 218 End Definitions
 219 *)
 220
 221 (* UNEXPORTED
 222 Implicit Arguments Partition [a b].
 223 *)
 224
 225 (* UNEXPORTED
 226 Implicit Arguments Partition_Dom [a b Hab n].
 227 *)
 228
 229 (* UNEXPORTED
 230 Implicit Arguments Mesh [a b Hab n].
 231 *)
 232
 233 (* UNEXPORTED
 234 Implicit Arguments AntiMesh [a b Hab n].
 235 *)
 236
 237 (* UNEXPORTED
 238 Implicit Arguments Pts [a b Hab lng].
 239 *)
 240
 241 (* UNEXPORTED
 242 Implicit Arguments Part_Mesh_List [n a b Hab].
 243 *)
 244
 245 (* UNEXPORTED
 246 Implicit Arguments Points_in_Partition [a b Hab n].
 247 *)
 248
 249 (* UNEXPORTED
 250 Implicit Arguments Partition_Sum [a b Hab n P g F].
 251 *)
 252
 253 (* UNEXPORTED
 254 Implicit Arguments Even_Partition [a b].
 255 *)
 256
 257 (* UNEXPORTED
 258 Implicit Arguments Even_Partition_Sum [a b].
 259 *)
 260
 261 (* UNEXPORTED
 262 Implicit Arguments Refinement [a b Hab n m].
 263 *)
 264
 265 (* UNEXPORTED
 266 Hint Resolve start finish: algebra.
 267 *)
 268
 269 (* UNEXPORTED
 270 Section Lemmas
 271 *)
 272
 273 (*#* ** Properties of the mesh
 274
 275 If a partition has more than one point then its mesh list is nonempty.
 276 *)
 277
 278 inline "cic:/CoRN/ftc/Partitions/length_Part_Mesh_List.con".
 279
 280 (*#*
 281 Any element of the auxiliary list defined to calculate the mesh of a partition has a very specific form.
 282 *)
 283
 284 inline "cic:/CoRN/ftc/Partitions/Part_Mesh_List_lemma.con".
 285
 286 (*#*
 287 Mesh and antimesh are always nonnegative.
 288 *)
 289
 290 inline "cic:/CoRN/ftc/Partitions/Mesh_nonneg.con".
 291
 292 inline "cic:/CoRN/ftc/Partitions/AntiMesh_nonneg.con".
 293
 294 (*#*
 295 Most important, [AntiMesh] and [Mesh] provide lower and upper bounds
 296 for the distance between any two consecutive points in a partition.
 297
 298 %\begin{convention}% Let [I] be [[a,b]] and [P] be a partition of [I]
 299 with [n] points.
 300 %\end{convention}%
 301 *)
 302
 303 alias id "a" = "cic:/CoRN/ftc/Partitions/Lemmas/a.var".
 304
 305 alias id "b" = "cic:/CoRN/ftc/Partitions/Lemmas/b.var".
 306
 307 (* begin hide *)
 308
 309 inline "cic:/CoRN/ftc/Partitions/Lemmas/I.con" "Lemmas__".
 310
 311 (* end hide *)
 312
 313 alias id "Hab" = "cic:/CoRN/ftc/Partitions/Lemmas/Hab.var".
 314
 315 alias id "n" = "cic:/CoRN/ftc/Partitions/Lemmas/n.var".
 316
 317 alias id "P" = "cic:/CoRN/ftc/Partitions/Lemmas/P.var".
 318
 319 inline "cic:/CoRN/ftc/Partitions/Mesh_lemma.con".
 320
 321 inline "cic:/CoRN/ftc/Partitions/AntiMesh_lemma.con".
 322
 323 inline "cic:/CoRN/ftc/Partitions/Mesh_leEq.con".
 324
 325 (* UNEXPORTED
 326 End Lemmas
 327 *)
 328
 329 (* UNEXPORTED
 330 Section Even_Partitions
 331 *)
 332
 333 (*#* More technical stuff.  Two equal partitions have the same mesh.
 334 *)
 335
 336 inline "cic:/CoRN/ftc/Partitions/Mesh_wd.con".
 337
 338 inline "cic:/CoRN/ftc/Partitions/Mesh_wd'.con".
 339
 340 (*#*
 341 The mesh of an even partition is easily calculated.
 342 *)
 343
 344 inline "cic:/CoRN/ftc/Partitions/even_partition_Mesh.con".
 345
 346 (*#* ** Miscellaneous
 347 %\begin{convention}% Throughout this section, let [a,b:IR] and [I] be [[a,b]].
 348 %\end{convention}%
 349 *)
 350
 351 alias id "a" = "cic:/CoRN/ftc/Partitions/Even_Partitions/a.var".
 352
 353 alias id "b" = "cic:/CoRN/ftc/Partitions/Even_Partitions/b.var".
 354
 355 (* begin hide *)
 356
 357 inline "cic:/CoRN/ftc/Partitions/Even_Partitions/I.con" "Even_Partitions__".
 358
 359 (* end hide *)
 360
 361 alias id "Hab" = "cic:/CoRN/ftc/Partitions/Even_Partitions/Hab.var".
 362
 363 (*#*
 364 An interesting property: in a partition, if [ai [<] aj] then [i < j].
 365 *)
 366
 367 inline "cic:/CoRN/ftc/Partitions/Partition_Points_mon.con".
 368
 369 inline "cic:/CoRN/ftc/Partitions/refinement_resp_mult.con".
 370
 371 (*#*
 372 %\begin{convention}% Assume [m,n] are positive natural numbers and
 373 denote by [P] and [Q] the even partitions with, respectively, [m] and
 374 [n] points.
 375 %\end{convention}%
 376
 377 Even partitions always have a common refinement.
 378 *)
 379
 380 alias id "m" = "cic:/CoRN/ftc/Partitions/Even_Partitions/m.var".
 381
 382 alias id "n" = "cic:/CoRN/ftc/Partitions/Even_Partitions/n.var".
 383
 384 alias id "Hm" = "cic:/CoRN/ftc/Partitions/Even_Partitions/Hm.var".
 385
 386 alias id "Hn" = "cic:/CoRN/ftc/Partitions/Even_Partitions/Hn.var".
 387
 388 (* begin hide *)
 389
 390 inline "cic:/CoRN/ftc/Partitions/Even_Partitions/P.con" "Even_Partitions__".
 391
 392 inline "cic:/CoRN/ftc/Partitions/Even_Partitions/Q.con" "Even_Partitions__".
 393
 394 (* end hide *)
 395
 396 inline "cic:/CoRN/ftc/Partitions/even_partition_refinement.con".
 397
 398 (* UNEXPORTED
 399 End Even_Partitions
 400 *)
 401
 402 (* UNEXPORTED
 403 Section More_Definitions
 404 *)
 405
 406 (*#* ** Separation
 407
 408 Some auxiliary definitions.  A partition is said to be separated if all its points are distinct.
 409 *)
 410
 411 alias id "a" = "cic:/CoRN/ftc/Partitions/More_Definitions/a.var".
 412
 413 alias id "b" = "cic:/CoRN/ftc/Partitions/More_Definitions/b.var".
 414
 415 alias id "Hab" = "cic:/CoRN/ftc/Partitions/More_Definitions/Hab.var".
 416
 417 inline "cic:/CoRN/ftc/Partitions/_Separated.con".
 418
 419 (*#*
 420 Two partitions are said to be (mutually) separated if they are both
 421 separated and all their points are distinct (except for the
 422 endpoints).
 423
 424 %\begin{convention}% Let [P,Q] be partitions of [I] with,
 425 respectively, [n] and [m] points.
 426 %\end{convention}%
 427 *)
 428
 429 alias id "n" = "cic:/CoRN/ftc/Partitions/More_Definitions/n.var".
 430
 431 alias id "m" = "cic:/CoRN/ftc/Partitions/More_Definitions/m.var".
 432
 433 alias id "P" = "cic:/CoRN/ftc/Partitions/More_Definitions/P.var".
 434
 435 alias id "Q" = "cic:/CoRN/ftc/Partitions/More_Definitions/Q.var".
 436
 437 inline "cic:/CoRN/ftc/Partitions/Separated.con".
 438
 439 (* UNEXPORTED
 440 End More_Definitions
 441 *)
 442
 443 (* UNEXPORTED
 444 Implicit Arguments _Separated [a b Hab n].
 445 *)
 446
 447 (* UNEXPORTED
 448 Implicit Arguments Separated [a b Hab n m].
 449 *)
 450
 451 (* UNEXPORTED
 452 Section Sep_Partitions
 453 *)
 454
 455 alias id "a" = "cic:/CoRN/ftc/Partitions/Sep_Partitions/a.var".
 456
 457 alias id "b" = "cic:/CoRN/ftc/Partitions/Sep_Partitions/b.var".
 458
 459 (* begin hide *)
 460
 461 inline "cic:/CoRN/ftc/Partitions/Sep_Partitions/I.con" "Sep_Partitions__".
 462
 463 (* end hide *)
 464
 465 alias id "Hab" = "cic:/CoRN/ftc/Partitions/Sep_Partitions/Hab.var".
 466
 467 (*#*
 468 The antimesh of a separated partition is always positive.
 469 *)
 470
 471 inline "cic:/CoRN/ftc/Partitions/pos_AntiMesh.con".
 472
 473 (*#*
 474 A partition can have only one point iff the endpoints of the interval
 475 are the same; moreover, if the partition is separated and the
 476 endpoints of the interval are the same then it must have one point.
 477 *)
 478
 479 inline "cic:/CoRN/ftc/Partitions/partition_length_zero.con".
 480
 481 inline "cic:/CoRN/ftc/Partitions/_Separated_imp_length_zero.con".
 482
 483 inline "cic:/CoRN/ftc/Partitions/partition_less_imp_gt_zero.con".
 484
 485 (* UNEXPORTED
 486 End Sep_Partitions
 487 *)
 488