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