helm/software/matita/contribs/procedural/CoRN/ftc/RefLemma.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: RefLemma.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *)
  20
  21 include "ftc/RefSeparating.ma".
  22
  23 include "ftc/RefSeparated.ma".
  24
  25 include "ftc/RefSepRef.ma".
  26
  27 (* UNEXPORTED
  28 Section Refinement_Lemma
  29 *)
  30
  31 (*#* *The Refinement Lemmas
  32
  33 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):
  34
  35 %\noindent\textbf{%#<b>#Theorem#</b>#%}% Let [f] be a continuous function on a
  36 compact interval [[a,b]] with modulus of continuity%\footnote{%# (#From our
  37 point of view, the modulus of continuity is simply the proof that [f] is
  38 continuous.#)#%}% [omega].
  39 Let [P] be a partition of [[a,b]] and [eps [>] Zero] be such that
  40 [mesh(P)  [<]  omega(eps)].
  41 Then
  42 %\[\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)#
  43 where [S(f,P)] denotes any sum of the function [f] respecting the partition
  44 [P] (as previously defined).
  45
  46 The proof of this theorem relies on the fact that for any two partitions [P]
  47 and [R] of [[a,b]] it is possible to define a partition [Q] which is
  48 ``almost'' a common refinement of [P] and [R]---that is, given [eps [>] Zero]
  49 it is possible to define [Q] such that for every point [x] of either [P] or
  50 [R] there is a point [y] of [Q] such that [|x[-]y|  [<]  eps].
  51 This requires three separate constructions (done in three separate files)
  52 which are then properly combined to give the final result.  We recommend the
  53 reader to ignore this technical constructions.
  54
  55 First we prove that if [P] and [R] are both
  56 separated (though not necessarily separated from each other) then we can
  57 define a partition [P'] arbitrarily close to [P] (that is, such that given
  58 [alpha [>] Zero] and [xi [>] Zero] [P'] satisfies both
  59 [mesh(P')  [<]  mesh(P) [+] xi] and for every choice of points [x_i] respecting
  60 [P] there is a choice of points [x'_i] respecting [P'] such that
  61 [|S(f,P)-S(f,P')|  [<]  alpha]) that is separated from [R].
  62
  63 Then we prove that given any partition [P]
  64 and assuming [a  [#]  b] we can define a partition [P'] arbitrarily close to
  65 [P] (in the same sense as above) which is separated.
  66
  67 Finally we prove that every two separated
  68 partitions [P] and [R] have a common refinement---as every two points in [P]
  69 and [R] are apart, we can decide which one is smaller.  We use here the
  70 technical results about ordering that we proved in the file [IntegralLemmas.v].
  71
  72 Using the results from these files, we prove our main lemma in several steps
  73 (and versions).
  74
  75 %\begin{convention}% Throughout this section:
  76  - [a,b:IR] and [I] denotes [[a,b]];
  77  - [F] is a partial function continuous in [I].
  78
  79 %\end{convention}%
  80 *)
  81
  82 (* UNEXPORTED
  83 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/a.var
  84 *)
  85
  86 (* UNEXPORTED
  87 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/b.var
  88 *)
  89
  90 (* UNEXPORTED
  91 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Hab.var
  92 *)
  93
  94 (* begin hide *)
  95
  96 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/I.con" "Refinement_Lemma__" as definition.
  97
  98 (* end hide *)
  99
 100 (* UNEXPORTED
 101 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/F.var
 102 *)
 103
 104 (* UNEXPORTED
 105 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF.var
 106 *)
 107
 108 (* UNEXPORTED
 109 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/incF.var
 110 *)
 111
 112 (* begin hide *)
 113
 114 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF'.con" "Refinement_Lemma__" as definition.
 115
 116 (* end hide *)
 117
 118 (* UNEXPORTED
 119 Section First_Refinement_Lemma
 120 *)
 121
 122 (*#*
 123 This is the first part of the proof of Theorem 2.9.
 124
 125 %\begin{convention}%
 126  - [P, Q] are partitions of [I] with, respectively, [n] and [m] points;
 127  - [Q] is a refinement of [P];
 128  - [e] is a positive real number;
 129  - [d] is the modulus of continuity of [F] for [e];
 130  - the mesh of [P] is less or equal to [d];
 131  - [fP] and [fQ] are choices of points respecting the partitions [P] and [Q],
 132 respectively.
 133
 134 %\end{convention}%
 135 *)
 136
 137 (* UNEXPORTED
 138 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/e.var
 139 *)
 140
 141 (* UNEXPORTED
 142 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/He.var
 143 *)
 144
 145 (* begin hide *)
 146
 147 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/d.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
 148
 149 (* end hide *)
 150
 151 (* UNEXPORTED
 152 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/m.var
 153 *)
 154
 155 (* UNEXPORTED
 156 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/n.var
 157 *)
 158
 159 (* UNEXPORTED
 160 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/P.var
 161 *)
 162
 163 (* UNEXPORTED
 164 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HMesh.var
 165 *)
 166
 167 (* UNEXPORTED
 168 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/Q.var
 169 *)
 170
 171 (* UNEXPORTED
 172 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/Href.var
 173 *)
 174
 175 (* UNEXPORTED
 176 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/fP.var
 177 *)
 178
 179 (* UNEXPORTED
 180 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfP.var
 181 *)
 182
 183 (* UNEXPORTED
 184 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfP'.var
 185 *)
 186
 187 (* UNEXPORTED
 188 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/fQ.var
 189 *)
 190
 191 (* UNEXPORTED
 192 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfQ.var
 193 *)
 194
 195 (* UNEXPORTED
 196 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfQ'.var
 197 *)
 198
 199 (* begin hide *)
 200
 201 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/sub.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
 202
 203 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_0.con" as lemma.
 204
 205 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_n.con" as lemma.
 206
 207 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_mon.con" as lemma.
 208
 209 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_mon'.con" as lemma.
 210
 211 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_hyp.con" as lemma.
 212
 213 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_S.con" as lemma.
 214
 215 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
 216
 217 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H'.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
 218
 219 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H0.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
 220
 221 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_SS.con" as lemma.
 222
 223 inline procedural "cic:/CoRN/ftc/RefLemma/RL_h.con" as definition.
 224
 225 inline procedural "cic:/CoRN/ftc/RefLemma/RL_g.con" as definition.
 226
 227 (* NOTATION
 228 Notation g := RL_g.
 229 *)
 230
 231 (* NOTATION
 232 Notation h := RL_h.
 233 *)
 234
 235 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc1.con" as lemma.
 236
 237 (* NOTATION
 238 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
 239 *)
 240
 241 (* NOTATION
 242 Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)).
 243 *)
 244
 245 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc2.con" as lemma.
 246
 247 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc3.con" as lemma.
 248
 249 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc4.con" as lemma.
 250
 251 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc5.con" as lemma.
 252
 253 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc6.con" as lemma.
 254
 255 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc7.con" as lemma.
 256
 257 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc8.con" as lemma.
 258
 259 (* end hide *)
 260
 261 inline procedural "cic:/CoRN/ftc/RefLemma/first_refinement_lemma.con" as lemma.
 262
 263 (* UNEXPORTED
 264 End First_Refinement_Lemma
 265 *)
 266
 267 (* UNEXPORTED
 268 Section Second_Refinement_Lemma
 269 *)
 270
 271 (*#*
 272 This is inequality (2.6.7).
 273
 274 %\begin{convention}%
 275  - [P, Q, R] are partitions of [I] with, respectively, [j, n] and [k] points;
 276  - [Q] is a common refinement of [P] and [R];
 277  - [e, e'] are positive real numbers;
 278  - [d, d'] are the moduli of continuity of [F] for [e, e'];
 279  - the Mesh of [P] is less or equal to [d];
 280  - the Mesh of [R] is less or equal to [d'];
 281  - [fP, fQ] and [fR] are choices of points respecting the partitions [P, Q]
 282 and [R], respectively.
 283
 284 %\end{convention}%
 285 *)
 286
 287 (* UNEXPORTED
 288 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/n.var
 289 *)
 290
 291 (* UNEXPORTED
 292 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/j.var
 293 *)
 294
 295 (* UNEXPORTED
 296 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/k.var
 297 *)
 298
 299 (* UNEXPORTED
 300 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/P.var
 301 *)
 302
 303 (* UNEXPORTED
 304 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/Q.var
 305 *)
 306
 307 (* UNEXPORTED
 308 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/R.var
 309 *)
 310
 311 (* UNEXPORTED
 312 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HrefP.var
 313 *)
 314
 315 (* UNEXPORTED
 316 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HrefR.var
 317 *)
 318
 319 (* UNEXPORTED
 320 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/e.var
 321 *)
 322
 323 (* UNEXPORTED
 324 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/e'.var
 325 *)
 326
 327 (* UNEXPORTED
 328 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/He.var
 329 *)
 330
 331 (* UNEXPORTED
 332 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/He'.var
 333 *)
 334
 335 (* begin hide *)
 336
 337 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d.con" "Refinement_Lemma__Second_Refinement_Lemma__" as definition.
 338
 339 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d'.con" "Refinement_Lemma__Second_Refinement_Lemma__" as definition.
 340
 341 (* end hide *)
 342
 343 (* UNEXPORTED
 344 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HMeshP.var
 345 *)
 346
 347 (* UNEXPORTED
 348 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HMeshR.var
 349 *)
 350
 351 (* UNEXPORTED
 352 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/fP.var
 353 *)
 354
 355 (* UNEXPORTED
 356 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfP.var
 357 *)
 358
 359 (* UNEXPORTED
 360 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfP'.var
 361 *)
 362
 363 (* UNEXPORTED
 364 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/fR.var
 365 *)
 366
 367 (* UNEXPORTED
 368 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfR.var
 369 *)
 370
 371 (* UNEXPORTED
 372 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfR'.var
 373 *)
 374
 375 inline procedural "cic:/CoRN/ftc/RefLemma/second_refinement_lemma.con" as lemma.
 376
 377 (* UNEXPORTED
 378 End Second_Refinement_Lemma
 379 *)
 380
 381 (* UNEXPORTED
 382 Section Third_Refinement_Lemma
 383 *)
 384
 385 (*#*
 386 This is an approximation of inequality (2.6.7), but without assuming the existence of a common refinement of [P] and [R].
 387
 388 %\begin{convention}%
 389  - [P, R] are partitions of [I] with, respectively, [n] and [m] points;
 390  - [e, e'] are positive real numbers;
 391  - [d, d'] are the moduli of continuity of [F] for [e, e'];
 392  - the Mesh of [P] is less than [d];
 393  - the Mesh of [R] is less than [d'];
 394  - [fP] and [fR] are choices of points respecting the partitions [P] and [R],
 395 respectively;
 396  - [beta] is a positive real number.
 397
 398 %\end{convention}%
 399 *)
 400
 401 (* UNEXPORTED
 402 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/n.var
 403 *)
 404
 405 (* UNEXPORTED
 406 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/m.var
 407 *)
 408
 409 (* UNEXPORTED
 410 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P.var
 411 *)
 412
 413 (* UNEXPORTED
 414 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R.var
 415 *)
 416
 417 (* UNEXPORTED
 418 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/e.var
 419 *)
 420
 421 (* UNEXPORTED
 422 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/e'.var
 423 *)
 424
 425 (* UNEXPORTED
 426 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/He.var
 427 *)
 428
 429 (* UNEXPORTED
 430 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/He'.var
 431 *)
 432
 433 (* begin hide *)
 434
 435 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 436
 437 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 438
 439 (* end hide *)
 440
 441 (* UNEXPORTED
 442 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HMeshP.var
 443 *)
 444
 445 (* UNEXPORTED
 446 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HMeshR.var
 447 *)
 448
 449 (* UNEXPORTED
 450 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP.var
 451 *)
 452
 453 (* UNEXPORTED
 454 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfP.var
 455 *)
 456
 457 (* UNEXPORTED
 458 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfP'.var
 459 *)
 460
 461 (* UNEXPORTED
 462 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR.var
 463 *)
 464
 465 (* UNEXPORTED
 466 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfR.var
 467 *)
 468
 469 (* UNEXPORTED
 470 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfR'.var
 471 *)
 472
 473 (* UNEXPORTED
 474 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Hab'.var
 475 *)
 476
 477 (* UNEXPORTED
 478 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/beta.var
 479 *)
 480
 481 (* UNEXPORTED
 482 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Hbeta.var
 483 *)
 484
 485 (* begin hide *)
 486
 487 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/alpha.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 488
 489 inline procedural "cic:/CoRN/ftc/RefLemma/RL_alpha.con" as lemma.
 490
 491 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi1.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 492
 493 inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi1.con" as lemma.
 494
 495 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta1.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 496
 497 inline procedural "cic:/CoRN/ftc/RefLemma/RL_delta1.con" as lemma.
 498
 499 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 500
 501 inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_sep.con" as lemma.
 502
 503 inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_Mesh.con" as lemma.
 504
 505 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 506
 507 inline procedural "cic:/CoRN/ftc/RefLemma/RL_fP'_in_P'.con" as lemma.
 508
 509 inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_P_sum.con" as lemma.
 510
 511 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi2.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 512
 513 inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi2.con" as lemma.
 514
 515 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta2.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 516
 517 inline procedural "cic:/CoRN/ftc/RefLemma/RL_delta2.con" as lemma.
 518
 519 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 520
 521 inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_sep.con" as lemma.
 522
 523 inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_Mesh.con" as lemma.
 524
 525 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 526
 527 inline procedural "cic:/CoRN/ftc/RefLemma/RL_fR'_in_R'.con" as lemma.
 528
 529 inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_R_sum.con" as lemma.
 530
 531 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi3.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 532
 533 inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi3.con" as lemma.
 534
 535 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Q.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 536
 537 inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_Mesh.con" as lemma.
 538
 539 inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_sep.con" as lemma.
 540
 541 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fQ.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
 542
 543 inline procedural "cic:/CoRN/ftc/RefLemma/RL_fQ_in_Q.con" as lemma.
 544
 545 inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_P'_sum.con" as lemma.
 546
 547 (* end hide *)
 548
 549 inline procedural "cic:/CoRN/ftc/RefLemma/third_refinement_lemma.con" as lemma.
 550
 551 (* UNEXPORTED
 552 End Third_Refinement_Lemma
 553 *)
 554
 555 (* UNEXPORTED
 556 Section Fourth_Refinement_Lemma
 557 *)
 558
 559 (* begin hide *)
 560
 561 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Fa.con" "Refinement_Lemma__Fourth_Refinement_Lemma__" as definition.
 562
 563 (* NOTATION
 564 Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)).
 565 *)
 566
 567 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sum_lemma_aux.con" as lemma.
 568
 569 (* end hide *)
 570
 571 (*#*
 572 Finally, this is inequality (2.6.7) exactly as stated (same conventions as
 573 above)
 574 *)
 575
 576 (* UNEXPORTED
 577 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/n.var
 578 *)
 579
 580 (* UNEXPORTED
 581 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/m.var
 582 *)
 583
 584 (* UNEXPORTED
 585 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/P.var
 586 *)
 587
 588 (* UNEXPORTED
 589 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/R.var
 590 *)
 591
 592 (* UNEXPORTED
 593 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/e.var
 594 *)
 595
 596 (* UNEXPORTED
 597 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/e'.var
 598 *)
 599
 600 (* UNEXPORTED
 601 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/He.var
 602 *)
 603
 604 (* UNEXPORTED
 605 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/He'.var
 606 *)
 607
 608 (* begin hide *)
 609
 610 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d.con" "Refinement_Lemma__Fourth_Refinement_Lemma__" as definition.
 611
 612 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d'.con" "Refinement_Lemma__Fourth_Refinement_Lemma__" as definition.
 613
 614 (* end hide *)
 615
 616 (* UNEXPORTED
 617 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HMeshP.var
 618 *)
 619
 620 (* UNEXPORTED
 621 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HMeshR.var
 622 *)
 623
 624 (* UNEXPORTED
 625 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/fP.var
 626 *)
 627
 628 (* UNEXPORTED
 629 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfP.var
 630 *)
 631
 632 (* UNEXPORTED
 633 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfP'.var
 634 *)
 635
 636 (* UNEXPORTED
 637 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/fR.var
 638 *)
 639
 640 (* UNEXPORTED
 641 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfR.var
 642 *)
 643
 644 (* UNEXPORTED
 645 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfR'.var
 646 *)
 647
 648 (* begin show *)
 649
 650 (* UNEXPORTED
 651 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Hab'.var
 652 *)
 653
 654 (* end show *)
 655
 656 inline procedural "cic:/CoRN/ftc/RefLemma/fourth_refinement_lemma.con" as lemma.
 657
 658 (* UNEXPORTED
 659 End Fourth_Refinement_Lemma
 660 *)
 661
 662 (* UNEXPORTED
 663 Section Main_Refinement_Lemma
 664 *)
 665
 666 (*#* We finish by presenting Theorem 9. *)
 667
 668 (* UNEXPORTED
 669 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/n.var
 670 *)
 671
 672 (* UNEXPORTED
 673 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/m.var
 674 *)
 675
 676 (* UNEXPORTED
 677 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/P.var
 678 *)
 679
 680 (* UNEXPORTED
 681 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/R.var
 682 *)
 683
 684 (* UNEXPORTED
 685 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/e.var
 686 *)
 687
 688 (* UNEXPORTED
 689 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/e'.var
 690 *)
 691
 692 (* UNEXPORTED
 693 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/He.var
 694 *)
 695
 696 (* UNEXPORTED
 697 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/He'.var
 698 *)
 699
 700 (* begin hide *)
 701
 702 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d.con" "Refinement_Lemma__Main_Refinement_Lemma__" as definition.
 703
 704 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d'.con" "Refinement_Lemma__Main_Refinement_Lemma__" as definition.
 705
 706 (* end hide *)
 707
 708 (* UNEXPORTED
 709 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HMeshP.var
 710 *)
 711
 712 (* UNEXPORTED
 713 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HMeshR.var
 714 *)
 715
 716 (* UNEXPORTED
 717 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/fP.var
 718 *)
 719
 720 (* UNEXPORTED
 721 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfP.var
 722 *)
 723
 724 (* UNEXPORTED
 725 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfP'.var
 726 *)
 727
 728 (* UNEXPORTED
 729 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/fR.var
 730 *)
 731
 732 (* UNEXPORTED
 733 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfR.var
 734 *)
 735
 736 (* UNEXPORTED
 737 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfR'.var
 738 *)
 739
 740 inline procedural "cic:/CoRN/ftc/RefLemma/refinement_lemma.con" as lemma.
 741
 742 (* UNEXPORTED
 743 End Main_Refinement_Lemma
 744 *)
 745
 746 (* UNEXPORTED
 747 End Refinement_Lemma
 748 *)
 749