helm/software/matita/contribs/CoRN-Procedural/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 alias id "a" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/a.var".
  83
  84 alias id "b" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/b.var".
  85
  86 alias id "Hab" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Hab.var".
  87
  88 (* begin hide *)
  89
  90 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/I.con" "Refinement_Lemma__".
  91
  92 (* end hide *)
  93
  94 alias id "F" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/F.var".
  95
  96 alias id "contF" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF.var".
  97
  98 alias id "incF" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/incF.var".
  99
 100 (* begin hide *)
 101
 102 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF'.con" "Refinement_Lemma__".
 103
 104 (* end hide *)
 105
 106 (* UNEXPORTED
 107 Section First_Refinement_Lemma
 108 *)
 109
 110 (*#*
 111 This is the first part of the proof of Theorem 2.9.
 112
 113 %\begin{convention}%
 114  - [P, Q] are partitions of [I] with, respectively, [n] and [m] points;
 115  - [Q] is a refinement of [P];
 116  - [e] is a positive real number;
 117  - [d] is the modulus of continuity of [F] for [e];
 118  - the mesh of [P] is less or equal to [d];
 119  - [fP] and [fQ] are choices of points respecting the partitions [P] and [Q],
 120 respectively.
 121
 122 %\end{convention}%
 123 *)
 124
 125 alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/e.var".
 126
 127 alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/He.var".
 128
 129 (* begin hide *)
 130
 131 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/d.con" "Refinement_Lemma__First_Refinement_Lemma__".
 132
 133 (* end hide *)
 134
 135 alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/m.var".
 136
 137 alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/n.var".
 138
 139 alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/P.var".
 140
 141 alias id "HMesh" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HMesh.var".
 142
 143 alias id "Q" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/Q.var".
 144
 145 alias id "Href" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/Href.var".
 146
 147 alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/fP.var".
 148
 149 alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfP.var".
 150
 151 alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfP'.var".
 152
 153 alias id "fQ" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/fQ.var".
 154
 155 alias id "HfQ" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfQ.var".
 156
 157 alias id "HfQ'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfQ'.var".
 158
 159 (* begin hide *)
 160
 161 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/sub.con" "Refinement_Lemma__First_Refinement_Lemma__".
 162
 163 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_0.con".
 164
 165 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_n.con".
 166
 167 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_mon.con".
 168
 169 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_mon'.con".
 170
 171 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_hyp.con".
 172
 173 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_S.con".
 174
 175 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H.con" "Refinement_Lemma__First_Refinement_Lemma__".
 176
 177 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H'.con" "Refinement_Lemma__First_Refinement_Lemma__".
 178
 179 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H0.con" "Refinement_Lemma__First_Refinement_Lemma__".
 180
 181 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_SS.con".
 182
 183 inline procedural "cic:/CoRN/ftc/RefLemma/RL_h.con".
 184
 185 inline procedural "cic:/CoRN/ftc/RefLemma/RL_g.con".
 186
 187 (* NOTATION
 188 Notation g := RL_g.
 189 *)
 190
 191 (* NOTATION
 192 Notation h := RL_h.
 193 *)
 194
 195 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc1.con".
 196
 197 (* NOTATION
 198 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
 199 *)
 200
 201 (* NOTATION
 202 Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)).
 203 *)
 204
 205 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc2.con".
 206
 207 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc3.con".
 208
 209 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc4.con".
 210
 211 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc5.con".
 212
 213 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc6.con".
 214
 215 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc7.con".
 216
 217 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc8.con".
 218
 219 (* end hide *)
 220
 221 inline procedural "cic:/CoRN/ftc/RefLemma/first_refinement_lemma.con".
 222
 223 (* UNEXPORTED
 224 End First_Refinement_Lemma
 225 *)
 226
 227 (* UNEXPORTED
 228 Section Second_Refinement_Lemma
 229 *)
 230
 231 (*#*
 232 This is inequality (2.6.7).
 233
 234 %\begin{convention}%
 235  - [P, Q, R] are partitions of [I] with, respectively, [j, n] and [k] points;
 236  - [Q] is a common refinement of [P] and [R];
 237  - [e, e'] are positive real numbers;
 238  - [d, d'] are the moduli of continuity of [F] for [e, e'];
 239  - the Mesh of [P] is less or equal to [d];
 240  - the Mesh of [R] is less or equal to [d'];
 241  - [fP, fQ] and [fR] are choices of points respecting the partitions [P, Q]
 242 and [R], respectively.
 243
 244 %\end{convention}%
 245 *)
 246
 247 alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/n.var".
 248
 249 alias id "j" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/j.var".
 250
 251 alias id "k" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/k.var".
 252
 253 alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/P.var".
 254
 255 alias id "Q" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/Q.var".
 256
 257 alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/R.var".
 258
 259 alias id "HrefP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HrefP.var".
 260
 261 alias id "HrefR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HrefR.var".
 262
 263 alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/e.var".
 264
 265 alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/e'.var".
 266
 267 alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/He.var".
 268
 269 alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/He'.var".
 270
 271 (* begin hide *)
 272
 273 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d.con" "Refinement_Lemma__Second_Refinement_Lemma__".
 274
 275 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d'.con" "Refinement_Lemma__Second_Refinement_Lemma__".
 276
 277 (* end hide *)
 278
 279 alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HMeshP.var".
 280
 281 alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HMeshR.var".
 282
 283 alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/fP.var".
 284
 285 alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfP.var".
 286
 287 alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfP'.var".
 288
 289 alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/fR.var".
 290
 291 alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfR.var".
 292
 293 alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfR'.var".
 294
 295 inline procedural "cic:/CoRN/ftc/RefLemma/second_refinement_lemma.con".
 296
 297 (* UNEXPORTED
 298 End Second_Refinement_Lemma
 299 *)
 300
 301 (* UNEXPORTED
 302 Section Third_Refinement_Lemma
 303 *)
 304
 305 (*#*
 306 This is an approximation of inequality (2.6.7), but without assuming the existence of a common refinement of [P] and [R].
 307
 308 %\begin{convention}%
 309  - [P, R] are partitions of [I] with, respectively, [n] and [m] points;
 310  - [e, e'] are positive real numbers;
 311  - [d, d'] are the moduli of continuity of [F] for [e, e'];
 312  - the Mesh of [P] is less than [d];
 313  - the Mesh of [R] is less than [d'];
 314  - [fP] and [fR] are choices of points respecting the partitions [P] and [R],
 315 respectively;
 316  - [beta] is a positive real number.
 317
 318 %\end{convention}%
 319 *)
 320
 321 alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/n.var".
 322
 323 alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/m.var".
 324
 325 alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P.var".
 326
 327 alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R.var".
 328
 329 alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/e.var".
 330
 331 alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/e'.var".
 332
 333 alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/He.var".
 334
 335 alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/He'.var".
 336
 337 (* begin hide *)
 338
 339 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 340
 341 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 342
 343 (* end hide *)
 344
 345 alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HMeshP.var".
 346
 347 alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HMeshR.var".
 348
 349 alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP.var".
 350
 351 alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfP.var".
 352
 353 alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfP'.var".
 354
 355 alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR.var".
 356
 357 alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfR.var".
 358
 359 alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfR'.var".
 360
 361 alias id "Hab'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Hab'.var".
 362
 363 alias id "beta" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/beta.var".
 364
 365 alias id "Hbeta" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Hbeta.var".
 366
 367 (* begin hide *)
 368
 369 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/alpha.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 370
 371 inline procedural "cic:/CoRN/ftc/RefLemma/RL_alpha.con".
 372
 373 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi1.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 374
 375 inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi1.con".
 376
 377 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta1.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 378
 379 inline procedural "cic:/CoRN/ftc/RefLemma/RL_delta1.con".
 380
 381 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 382
 383 inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_sep.con".
 384
 385 inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_Mesh.con".
 386
 387 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 388
 389 inline procedural "cic:/CoRN/ftc/RefLemma/RL_fP'_in_P'.con".
 390
 391 inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_P_sum.con".
 392
 393 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi2.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 394
 395 inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi2.con".
 396
 397 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta2.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 398
 399 inline procedural "cic:/CoRN/ftc/RefLemma/RL_delta2.con".
 400
 401 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 402
 403 inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_sep.con".
 404
 405 inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_Mesh.con".
 406
 407 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 408
 409 inline procedural "cic:/CoRN/ftc/RefLemma/RL_fR'_in_R'.con".
 410
 411 inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_R_sum.con".
 412
 413 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi3.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 414
 415 inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi3.con".
 416
 417 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Q.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 418
 419 inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_Mesh.con".
 420
 421 inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_sep.con".
 422
 423 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fQ.con" "Refinement_Lemma__Third_Refinement_Lemma__".
 424
 425 inline procedural "cic:/CoRN/ftc/RefLemma/RL_fQ_in_Q.con".
 426
 427 inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_P'_sum.con".
 428
 429 (* end hide *)
 430
 431 inline procedural "cic:/CoRN/ftc/RefLemma/third_refinement_lemma.con".
 432
 433 (* UNEXPORTED
 434 End Third_Refinement_Lemma
 435 *)
 436
 437 (* UNEXPORTED
 438 Section Fourth_Refinement_Lemma
 439 *)
 440
 441 (* begin hide *)
 442
 443 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Fa.con" "Refinement_Lemma__Fourth_Refinement_Lemma__".
 444
 445 (* NOTATION
 446 Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)).
 447 *)
 448
 449 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sum_lemma_aux.con".
 450
 451 (* end hide *)
 452
 453 (*#*
 454 Finally, this is inequality (2.6.7) exactly as stated (same conventions as
 455 above)
 456 *)
 457
 458 alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/n.var".
 459
 460 alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/m.var".
 461
 462 alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/P.var".
 463
 464 alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/R.var".
 465
 466 alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/e.var".
 467
 468 alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/e'.var".
 469
 470 alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/He.var".
 471
 472 alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/He'.var".
 473
 474 (* begin hide *)
 475
 476 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d.con" "Refinement_Lemma__Fourth_Refinement_Lemma__".
 477
 478 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d'.con" "Refinement_Lemma__Fourth_Refinement_Lemma__".
 479
 480 (* end hide *)
 481
 482 alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HMeshP.var".
 483
 484 alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HMeshR.var".
 485
 486 alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/fP.var".
 487
 488 alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfP.var".
 489
 490 alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfP'.var".
 491
 492 alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/fR.var".
 493
 494 alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfR.var".
 495
 496 alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfR'.var".
 497
 498 (* begin show *)
 499
 500 alias id "Hab'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Hab'.var".
 501
 502 (* end show *)
 503
 504 inline procedural "cic:/CoRN/ftc/RefLemma/fourth_refinement_lemma.con".
 505
 506 (* UNEXPORTED
 507 End Fourth_Refinement_Lemma
 508 *)
 509
 510 (* UNEXPORTED
 511 Section Main_Refinement_Lemma
 512 *)
 513
 514 (*#* We finish by presenting Theorem 9. *)
 515
 516 alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/n.var".
 517
 518 alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/m.var".
 519
 520 alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/P.var".
 521
 522 alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/R.var".
 523
 524 alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/e.var".
 525
 526 alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/e'.var".
 527
 528 alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/He.var".
 529
 530 alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/He'.var".
 531
 532 (* begin hide *)
 533
 534 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d.con" "Refinement_Lemma__Main_Refinement_Lemma__".
 535
 536 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d'.con" "Refinement_Lemma__Main_Refinement_Lemma__".
 537
 538 (* end hide *)
 539
 540 alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HMeshP.var".
 541
 542 alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HMeshR.var".
 543
 544 alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/fP.var".
 545
 546 alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfP.var".
 547
 548 alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfP'.var".
 549
 550 alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/fR.var".
 551
 552 alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfR.var".
 553
 554 alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfR'.var".
 555
 556 inline procedural "cic:/CoRN/ftc/RefLemma/refinement_lemma.con".
 557
 558 (* UNEXPORTED
 559 End Main_Refinement_Lemma
 560 *)
 561
 562 (* UNEXPORTED
 563 End Refinement_Lemma
 564 *)
 565