helm/software/matita/contribs/CoRN-Decl/ftc/RefLemma.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/RefLemma".
  18
  19 (* $Id: RefLemma.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *)
  20
  21 (* INCLUDE
  22 RefSeparating
  23 *)
  24
  25 (* INCLUDE
  26 RefSeparated
  27 *)
  28
  29 (* INCLUDE
  30 RefSepRef
  31 *)
  32
  33 (* UNEXPORTED
  34 Section Refinement_Lemma.
  35 *)
  36
  37 (*#* *The Refinement Lemmas
  38
  39 Here we resume the results proved in four different files.  The aim is to prove the following result (last part of Theorem 2.9 of Bishop 1967):
  40
  41 %\noindent\textbf{%#<b>#Theorem#</b>#%}% Let [f] be a continuous function on a
  42 compact interval [[a,b]] with modulus of continuity%\footnote{%# (#From our
  43 point of view, the modulus of continuity is simply the proof that [f] is
  44 continuous.#)#%}% [omega].
  45 Let [P] be a partition of [[a,b]] and [eps [>] Zero] be such that
  46 [mesh(P)  [<]  omega(eps)].
  47 Then
  48 %\[\left|S(f,P)-\int_a^bf(x)dx\right|\leq\varepsilon(b-a),\]%#|S(f,P)-&int;f(x)dx|&le;&epsilon;(b-a)#
  49 where [S(f,P)] denotes any sum of the function [f] respecting the partition
  50 [P] (as previously defined).
  51
  52 The proof of this theorem relies on the fact that for any two partitions [P]
  53 and [R] of [[a,b]] it is possible to define a partition [Q] which is
  54 ``almost'' a common refinement of [P] and [R]---that is, given [eps [>] Zero]
  55 it is possible to define [Q] such that for every point [x] of either [P] or
  56 [R] there is a point [y] of [Q] such that [|x[-]y|  [<]  eps].
  57 This requires three separate constructions (done in three separate files)
  58 which are then properly combined to give the final result.  We recommend the
  59 reader to ignore this technical constructions.
  60
  61 First we prove that if [P] and [R] are both
  62 separated (though not necessarily separated from each other) then we can
  63 define a partition [P'] arbitrarily close to [P] (that is, such that given
  64 [alpha [>] Zero] and [xi [>] Zero] [P'] satisfies both
  65 [mesh(P')  [<]  mesh(P) [+] xi] and for every choice of points [x_i] respecting
  66 [P] there is a choice of points [x'_i] respecting [P'] such that
  67 [|S(f,P)-S(f,P')|  [<]  alpha]) that is separated from [R].
  68
  69 Then we prove that given any partition [P]
  70 and assuming [a  [#]  b] we can define a partition [P'] arbitrarily close to
  71 [P] (in the same sense as above) which is separated.
  72
  73 Finally we prove that every two separated
  74 partitions [P] and [R] have a common refinement---as every two points in [P]
  75 and [R] are apart, we can decide which one is smaller.  We use here the
  76 technical results about ordering that we proved in the file [IntegralLemmas.v].
  77
  78 Using the results from these files, we prove our main lemma in several steps
  79 (and versions).
  80
  81 %\begin{convention}% Throughout this section:
  82  - [a,b:IR] and [I] denotes [[a,b]];
  83  - [F] is a partial function continuous in [I].
  84
  85 %\end{convention}%
  86 *)
  87
  88 inline cic:/CoRN/ftc/RefLemma/a.var.
  89
  90 inline cic:/CoRN/ftc/RefLemma/b.var.
  91
  92 inline cic:/CoRN/ftc/RefLemma/Hab.var.
  93
  94 (* begin hide *)
  95
  96 inline cic:/CoRN/ftc/RefLemma/I.con.
  97
  98 (* end hide *)
  99
 100 inline cic:/CoRN/ftc/RefLemma/F.var.
 101
 102 inline cic:/CoRN/ftc/RefLemma/contF.var.
 103
 104 inline cic:/CoRN/ftc/RefLemma/incF.var.
 105
 106 (* begin hide *)
 107
 108 inline cic:/CoRN/ftc/RefLemma/contF'.con.
 109
 110 (* end hide *)
 111
 112 (* UNEXPORTED
 113 Section First_Refinement_Lemma.
 114 *)
 115
 116 (*#*
 117 This is the first part of the proof of Theorem 2.9.
 118
 119 %\begin{convention}%
 120  - [P, Q] are partitions of [I] with, respectively, [n] and [m] points;
 121  - [Q] is a refinement of [P];
 122  - [e] is a positive real number;
 123  - [d] is the modulus of continuity of [F] for [e];
 124  - the mesh of [P] is less or equal to [d];
 125  - [fP] and [fQ] are choices of points respecting the partitions [P] and [Q],
 126 respectively.
 127
 128 %\end{convention}%
 129 *)
 130
 131 inline cic:/CoRN/ftc/RefLemma/e.var.
 132
 133 inline cic:/CoRN/ftc/RefLemma/He.var.
 134
 135 (* begin hide *)
 136
 137 inline cic:/CoRN/ftc/RefLemma/d.con.
 138
 139 (* end hide *)
 140
 141 inline cic:/CoRN/ftc/RefLemma/m.var.
 142
 143 inline cic:/CoRN/ftc/RefLemma/n.var.
 144
 145 inline cic:/CoRN/ftc/RefLemma/P.var.
 146
 147 inline cic:/CoRN/ftc/RefLemma/HMesh.var.
 148
 149 inline cic:/CoRN/ftc/RefLemma/Q.var.
 150
 151 inline cic:/CoRN/ftc/RefLemma/Href.var.
 152
 153 inline cic:/CoRN/ftc/RefLemma/fP.var.
 154
 155 inline cic:/CoRN/ftc/RefLemma/HfP.var.
 156
 157 inline cic:/CoRN/ftc/RefLemma/HfP'.var.
 158
 159 inline cic:/CoRN/ftc/RefLemma/fQ.var.
 160
 161 inline cic:/CoRN/ftc/RefLemma/HfQ.var.
 162
 163 inline cic:/CoRN/ftc/RefLemma/HfQ'.var.
 164
 165 (* begin hide *)
 166
 167 inline cic:/CoRN/ftc/RefLemma/sub.con.
 168
 169 inline cic:/CoRN/ftc/RefLemma/RL_sub_0.con.
 170
 171 inline cic:/CoRN/ftc/RefLemma/RL_sub_n.con.
 172
 173 inline cic:/CoRN/ftc/RefLemma/RL_sub_mon.con.
 174
 175 inline cic:/CoRN/ftc/RefLemma/RL_sub_mon'.con.
 176
 177 inline cic:/CoRN/ftc/RefLemma/RL_sub_hyp.con.
 178
 179 inline cic:/CoRN/ftc/RefLemma/RL_sub_S.con.
 180
 181 inline cic:/CoRN/ftc/RefLemma/H.con.
 182
 183 inline cic:/CoRN/ftc/RefLemma/H'.con.
 184
 185 inline cic:/CoRN/ftc/RefLemma/H0.con.
 186
 187 inline cic:/CoRN/ftc/RefLemma/RL_sub_SS.con.
 188
 189 inline cic:/CoRN/ftc/RefLemma/RL_h.con.
 190
 191 inline cic:/CoRN/ftc/RefLemma/RL_g.con.
 192
 193 inline cic:/CoRN/ftc/RefLemma/ref_calc1.con.
 194
 195 inline cic:/CoRN/ftc/RefLemma/ref_calc2.con.
 196
 197 inline cic:/CoRN/ftc/RefLemma/ref_calc3.con.
 198
 199 inline cic:/CoRN/ftc/RefLemma/ref_calc4.con.
 200
 201 inline cic:/CoRN/ftc/RefLemma/ref_calc5.con.
 202
 203 inline cic:/CoRN/ftc/RefLemma/ref_calc6.con.
 204
 205 inline cic:/CoRN/ftc/RefLemma/ref_calc7.con.
 206
 207 inline cic:/CoRN/ftc/RefLemma/ref_calc8.con.
 208
 209 (* end hide *)
 210
 211 inline cic:/CoRN/ftc/RefLemma/first_refinement_lemma.con.
 212
 213 (* UNEXPORTED
 214 End First_Refinement_Lemma.
 215 *)
 216
 217 (* UNEXPORTED
 218 Section Second_Refinement_Lemma.
 219 *)
 220
 221 (*#*
 222 This is inequality (2.6.7).
 223
 224 %\begin{convention}%
 225  - [P, Q, R] are partitions of [I] with, respectively, [j, n] and [k] points;
 226  - [Q] is a common refinement of [P] and [R];
 227  - [e, e'] are positive real numbers;
 228  - [d, d'] are the moduli of continuity of [F] for [e, e'];
 229  - the Mesh of [P] is less or equal to [d];
 230  - the Mesh of [R] is less or equal to [d'];
 231  - [fP, fQ] and [fR] are choices of points respecting the partitions [P, Q]
 232 and [R], respectively.
 233
 234 %\end{convention}%
 235 *)
 236
 237 inline cic:/CoRN/ftc/RefLemma/n.var.
 238
 239 inline cic:/CoRN/ftc/RefLemma/j.var.
 240
 241 inline cic:/CoRN/ftc/RefLemma/k.var.
 242
 243 inline cic:/CoRN/ftc/RefLemma/P.var.
 244
 245 inline cic:/CoRN/ftc/RefLemma/Q.var.
 246
 247 inline cic:/CoRN/ftc/RefLemma/R.var.
 248
 249 inline cic:/CoRN/ftc/RefLemma/HrefP.var.
 250
 251 inline cic:/CoRN/ftc/RefLemma/HrefR.var.
 252
 253 inline cic:/CoRN/ftc/RefLemma/e.var.
 254
 255 inline cic:/CoRN/ftc/RefLemma/e'.var.
 256
 257 inline cic:/CoRN/ftc/RefLemma/He.var.
 258
 259 inline cic:/CoRN/ftc/RefLemma/He'.var.
 260
 261 (* begin hide *)
 262
 263 inline cic:/CoRN/ftc/RefLemma/d.con.
 264
 265 inline cic:/CoRN/ftc/RefLemma/d'.con.
 266
 267 (* end hide *)
 268
 269 inline cic:/CoRN/ftc/RefLemma/HMeshP.var.
 270
 271 inline cic:/CoRN/ftc/RefLemma/HMeshR.var.
 272
 273 inline cic:/CoRN/ftc/RefLemma/fP.var.
 274
 275 inline cic:/CoRN/ftc/RefLemma/HfP.var.
 276
 277 inline cic:/CoRN/ftc/RefLemma/HfP'.var.
 278
 279 inline cic:/CoRN/ftc/RefLemma/fR.var.
 280
 281 inline cic:/CoRN/ftc/RefLemma/HfR.var.
 282
 283 inline cic:/CoRN/ftc/RefLemma/HfR'.var.
 284
 285 inline cic:/CoRN/ftc/RefLemma/second_refinement_lemma.con.
 286
 287 (* UNEXPORTED
 288 End Second_Refinement_Lemma.
 289 *)
 290
 291 (* UNEXPORTED
 292 Section Third_Refinement_Lemma.
 293 *)
 294
 295 (*#*
 296 This is an approximation of inequality (2.6.7), but without assuming the existence of a common refinement of [P] and [R].
 297
 298 %\begin{convention}%
 299  - [P, R] are partitions of [I] with, respectively, [n] and [m] points;
 300  - [e, e'] are positive real numbers;
 301  - [d, d'] are the moduli of continuity of [F] for [e, e'];
 302  - the Mesh of [P] is less than [d];
 303  - the Mesh of [R] is less than [d'];
 304  - [fP] and [fR] are choices of points respecting the partitions [P] and [R],
 305 respectively;
 306  - [beta] is a positive real number.
 307
 308 %\end{convention}%
 309 *)
 310
 311 inline cic:/CoRN/ftc/RefLemma/n.var.
 312
 313 inline cic:/CoRN/ftc/RefLemma/m.var.
 314
 315 inline cic:/CoRN/ftc/RefLemma/P.var.
 316
 317 inline cic:/CoRN/ftc/RefLemma/R.var.
 318
 319 inline cic:/CoRN/ftc/RefLemma/e.var.
 320
 321 inline cic:/CoRN/ftc/RefLemma/e'.var.
 322
 323 inline cic:/CoRN/ftc/RefLemma/He.var.
 324
 325 inline cic:/CoRN/ftc/RefLemma/He'.var.
 326
 327 (* begin hide *)
 328
 329 inline cic:/CoRN/ftc/RefLemma/d.con.
 330
 331 inline cic:/CoRN/ftc/RefLemma/d'.con.
 332
 333 (* end hide *)
 334
 335 inline cic:/CoRN/ftc/RefLemma/HMeshP.var.
 336
 337 inline cic:/CoRN/ftc/RefLemma/HMeshR.var.
 338
 339 inline cic:/CoRN/ftc/RefLemma/fP.var.
 340
 341 inline cic:/CoRN/ftc/RefLemma/HfP.var.
 342
 343 inline cic:/CoRN/ftc/RefLemma/HfP'.var.
 344
 345 inline cic:/CoRN/ftc/RefLemma/fR.var.
 346
 347 inline cic:/CoRN/ftc/RefLemma/HfR.var.
 348
 349 inline cic:/CoRN/ftc/RefLemma/HfR'.var.
 350
 351 inline cic:/CoRN/ftc/RefLemma/Hab'.var.
 352
 353 inline cic:/CoRN/ftc/RefLemma/beta.var.
 354
 355 inline cic:/CoRN/ftc/RefLemma/Hbeta.var.
 356
 357 (* begin hide *)
 358
 359 inline cic:/CoRN/ftc/RefLemma/alpha.con.
 360
 361 inline cic:/CoRN/ftc/RefLemma/RL_alpha.con.
 362
 363 inline cic:/CoRN/ftc/RefLemma/csi1.con.
 364
 365 inline cic:/CoRN/ftc/RefLemma/RL_csi1.con.
 366
 367 inline cic:/CoRN/ftc/RefLemma/delta1.con.
 368
 369 inline cic:/CoRN/ftc/RefLemma/RL_delta1.con.
 370
 371 inline cic:/CoRN/ftc/RefLemma/P'.con.
 372
 373 inline cic:/CoRN/ftc/RefLemma/RL_P'_sep.con.
 374
 375 inline cic:/CoRN/ftc/RefLemma/RL_P'_Mesh.con.
 376
 377 inline cic:/CoRN/ftc/RefLemma/fP'.con.
 378
 379 inline cic:/CoRN/ftc/RefLemma/RL_fP'_in_P'.con.
 380
 381 inline cic:/CoRN/ftc/RefLemma/RL_P'_P_sum.con.
 382
 383 inline cic:/CoRN/ftc/RefLemma/csi2.con.
 384
 385 inline cic:/CoRN/ftc/RefLemma/RL_csi2.con.
 386
 387 inline cic:/CoRN/ftc/RefLemma/delta2.con.
 388
 389 inline cic:/CoRN/ftc/RefLemma/RL_delta2.con.
 390
 391 inline cic:/CoRN/ftc/RefLemma/R'.con.
 392
 393 inline cic:/CoRN/ftc/RefLemma/RL_R'_sep.con.
 394
 395 inline cic:/CoRN/ftc/RefLemma/RL_R'_Mesh.con.
 396
 397 inline cic:/CoRN/ftc/RefLemma/fR'.con.
 398
 399 inline cic:/CoRN/ftc/RefLemma/RL_fR'_in_R'.con.
 400
 401 inline cic:/CoRN/ftc/RefLemma/RL_R'_R_sum.con.
 402
 403 inline cic:/CoRN/ftc/RefLemma/csi3.con.
 404
 405 inline cic:/CoRN/ftc/RefLemma/RL_csi3.con.
 406
 407 inline cic:/CoRN/ftc/RefLemma/Q.con.
 408
 409 inline cic:/CoRN/ftc/RefLemma/RL_Q_Mesh.con.
 410
 411 inline cic:/CoRN/ftc/RefLemma/RL_Q_sep.con.
 412
 413 inline cic:/CoRN/ftc/RefLemma/fQ.con.
 414
 415 inline cic:/CoRN/ftc/RefLemma/RL_fQ_in_Q.con.
 416
 417 inline cic:/CoRN/ftc/RefLemma/RL_Q_P'_sum.con.
 418
 419 (* end hide *)
 420
 421 inline cic:/CoRN/ftc/RefLemma/third_refinement_lemma.con.
 422
 423 (* UNEXPORTED
 424 End Third_Refinement_Lemma.
 425 *)
 426
 427 (* UNEXPORTED
 428 Section Fourth_Refinement_Lemma.
 429 *)
 430
 431 (* begin hide *)
 432
 433 inline cic:/CoRN/ftc/RefLemma/Fa.con.
 434
 435 inline cic:/CoRN/ftc/RefLemma/RL_sum_lemma_aux.con.
 436
 437 (* end hide *)
 438
 439 (*#*
 440 Finally, this is inequality (2.6.7) exactly as stated (same conventions as
 441 above)
 442 *)
 443
 444 inline cic:/CoRN/ftc/RefLemma/n.var.
 445
 446 inline cic:/CoRN/ftc/RefLemma/m.var.
 447
 448 inline cic:/CoRN/ftc/RefLemma/P.var.
 449
 450 inline cic:/CoRN/ftc/RefLemma/R.var.
 451
 452 inline cic:/CoRN/ftc/RefLemma/e.var.
 453
 454 inline cic:/CoRN/ftc/RefLemma/e'.var.
 455
 456 inline cic:/CoRN/ftc/RefLemma/He.var.
 457
 458 inline cic:/CoRN/ftc/RefLemma/He'.var.
 459
 460 (* begin hide *)
 461
 462 inline cic:/CoRN/ftc/RefLemma/d.con.
 463
 464 inline cic:/CoRN/ftc/RefLemma/d'.con.
 465
 466 (* end hide *)
 467
 468 inline cic:/CoRN/ftc/RefLemma/HMeshP.var.
 469
 470 inline cic:/CoRN/ftc/RefLemma/HMeshR.var.
 471
 472 inline cic:/CoRN/ftc/RefLemma/fP.var.
 473
 474 inline cic:/CoRN/ftc/RefLemma/HfP.var.
 475
 476 inline cic:/CoRN/ftc/RefLemma/HfP'.var.
 477
 478 inline cic:/CoRN/ftc/RefLemma/fR.var.
 479
 480 inline cic:/CoRN/ftc/RefLemma/HfR.var.
 481
 482 inline cic:/CoRN/ftc/RefLemma/HfR'.var.
 483
 484 (* begin show *)
 485
 486 inline cic:/CoRN/ftc/RefLemma/Hab'.var.
 487
 488 (* end show *)
 489
 490 inline cic:/CoRN/ftc/RefLemma/fourth_refinement_lemma.con.
 491
 492 (* UNEXPORTED
 493 End Fourth_Refinement_Lemma.
 494 *)
 495
 496 (* UNEXPORTED
 497 Section Main_Refinement_Lemma.
 498 *)
 499
 500 (*#* We finish by presenting Theorem 9. *)
 501
 502 inline cic:/CoRN/ftc/RefLemma/n.var.
 503
 504 inline cic:/CoRN/ftc/RefLemma/m.var.
 505
 506 inline cic:/CoRN/ftc/RefLemma/P.var.
 507
 508 inline cic:/CoRN/ftc/RefLemma/R.var.
 509
 510 inline cic:/CoRN/ftc/RefLemma/e.var.
 511
 512 inline cic:/CoRN/ftc/RefLemma/e'.var.
 513
 514 inline cic:/CoRN/ftc/RefLemma/He.var.
 515
 516 inline cic:/CoRN/ftc/RefLemma/He'.var.
 517
 518 (* begin hide *)
 519
 520 inline cic:/CoRN/ftc/RefLemma/d.con.
 521
 522 inline cic:/CoRN/ftc/RefLemma/d'.con.
 523
 524 (* end hide *)
 525
 526 inline cic:/CoRN/ftc/RefLemma/HMeshP.var.
 527
 528 inline cic:/CoRN/ftc/RefLemma/HMeshR.var.
 529
 530 inline cic:/CoRN/ftc/RefLemma/fP.var.
 531
 532 inline cic:/CoRN/ftc/RefLemma/HfP.var.
 533
 534 inline cic:/CoRN/ftc/RefLemma/HfP'.var.
 535
 536 inline cic:/CoRN/ftc/RefLemma/fR.var.
 537
 538 inline cic:/CoRN/ftc/RefLemma/HfR.var.
 539
 540 inline cic:/CoRN/ftc/RefLemma/HfR'.var.
 541
 542 inline cic:/CoRN/ftc/RefLemma/refinement_lemma.con.
 543
 544 (* UNEXPORTED
 545 End Main_Refinement_Lemma.
 546 *)
 547
 548 (* UNEXPORTED
 549 End Refinement_Lemma.
 550 *)
 551