1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/RefLemma".
21 (* $Id: RefLemma.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *)
23 include "ftc/RefSeparating.ma".
25 include "ftc/RefSeparated.ma".
27 include "ftc/RefSepRef.ma".
30 Section Refinement_Lemma.
33 (*#* *The Refinement Lemmas
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):
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)].
44 %\[\left|S(f,P)-\int_a^bf(x)dx\right|\leq\varepsilon(b-a),\]%#|S(f,P)-∫f(x)dx|≤ε(b-a)#
45 where [S(f,P)] denotes any sum of the function [f] respecting the partition
46 [P] (as previously defined).
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.
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].
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.
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].
74 Using the results from these files, we prove our main lemma in several steps
77 %\begin{convention}% Throughout this section:
78 - [a,b:IR] and [I] denotes [[a,b]];
79 - [F] is a partial function continuous in [I].
84 inline "cic:/CoRN/ftc/RefLemma/a.var".
86 inline "cic:/CoRN/ftc/RefLemma/b.var".
88 inline "cic:/CoRN/ftc/RefLemma/Hab.var".
92 inline "cic:/CoRN/ftc/RefLemma/I.con".
96 inline "cic:/CoRN/ftc/RefLemma/F.var".
98 inline "cic:/CoRN/ftc/RefLemma/contF.var".
100 inline "cic:/CoRN/ftc/RefLemma/incF.var".
104 inline "cic:/CoRN/ftc/RefLemma/contF'.con".
109 Section First_Refinement_Lemma.
113 This is the first part of the proof of Theorem 2.9.
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],
127 inline "cic:/CoRN/ftc/RefLemma/e.var".
129 inline "cic:/CoRN/ftc/RefLemma/He.var".
133 inline "cic:/CoRN/ftc/RefLemma/d.con".
137 inline "cic:/CoRN/ftc/RefLemma/m.var".
139 inline "cic:/CoRN/ftc/RefLemma/n.var".
141 inline "cic:/CoRN/ftc/RefLemma/P.var".
143 inline "cic:/CoRN/ftc/RefLemma/HMesh.var".
145 inline "cic:/CoRN/ftc/RefLemma/Q.var".
147 inline "cic:/CoRN/ftc/RefLemma/Href.var".
149 inline "cic:/CoRN/ftc/RefLemma/fP.var".
151 inline "cic:/CoRN/ftc/RefLemma/HfP.var".
153 inline "cic:/CoRN/ftc/RefLemma/HfP'.var".
155 inline "cic:/CoRN/ftc/RefLemma/fQ.var".
157 inline "cic:/CoRN/ftc/RefLemma/HfQ.var".
159 inline "cic:/CoRN/ftc/RefLemma/HfQ'.var".
163 inline "cic:/CoRN/ftc/RefLemma/sub.con".
165 inline "cic:/CoRN/ftc/RefLemma/RL_sub_0.con".
167 inline "cic:/CoRN/ftc/RefLemma/RL_sub_n.con".
169 inline "cic:/CoRN/ftc/RefLemma/RL_sub_mon.con".
171 inline "cic:/CoRN/ftc/RefLemma/RL_sub_mon'.con".
173 inline "cic:/CoRN/ftc/RefLemma/RL_sub_hyp.con".
175 inline "cic:/CoRN/ftc/RefLemma/RL_sub_S.con".
177 inline "cic:/CoRN/ftc/RefLemma/H.con".
179 inline "cic:/CoRN/ftc/RefLemma/H'.con".
181 inline "cic:/CoRN/ftc/RefLemma/H0.con".
183 inline "cic:/CoRN/ftc/RefLemma/RL_sub_SS.con".
185 inline "cic:/CoRN/ftc/RefLemma/RL_h.con".
187 inline "cic:/CoRN/ftc/RefLemma/RL_g.con".
189 inline "cic:/CoRN/ftc/RefLemma/ref_calc1.con".
191 inline "cic:/CoRN/ftc/RefLemma/ref_calc2.con".
193 inline "cic:/CoRN/ftc/RefLemma/ref_calc3.con".
195 inline "cic:/CoRN/ftc/RefLemma/ref_calc4.con".
197 inline "cic:/CoRN/ftc/RefLemma/ref_calc5.con".
199 inline "cic:/CoRN/ftc/RefLemma/ref_calc6.con".
201 inline "cic:/CoRN/ftc/RefLemma/ref_calc7.con".
203 inline "cic:/CoRN/ftc/RefLemma/ref_calc8.con".
207 inline "cic:/CoRN/ftc/RefLemma/first_refinement_lemma.con".
210 End First_Refinement_Lemma.
214 Section Second_Refinement_Lemma.
218 This is inequality (2.6.7).
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.
233 inline "cic:/CoRN/ftc/RefLemma/n.var".
235 inline "cic:/CoRN/ftc/RefLemma/j.var".
237 inline "cic:/CoRN/ftc/RefLemma/k.var".
239 inline "cic:/CoRN/ftc/RefLemma/P.var".
241 inline "cic:/CoRN/ftc/RefLemma/Q.var".
243 inline "cic:/CoRN/ftc/RefLemma/R.var".
245 inline "cic:/CoRN/ftc/RefLemma/HrefP.var".
247 inline "cic:/CoRN/ftc/RefLemma/HrefR.var".
249 inline "cic:/CoRN/ftc/RefLemma/e.var".
251 inline "cic:/CoRN/ftc/RefLemma/e'.var".
253 inline "cic:/CoRN/ftc/RefLemma/He.var".
255 inline "cic:/CoRN/ftc/RefLemma/He'.var".
259 inline "cic:/CoRN/ftc/RefLemma/d.con".
261 inline "cic:/CoRN/ftc/RefLemma/d'.con".
265 inline "cic:/CoRN/ftc/RefLemma/HMeshP.var".
267 inline "cic:/CoRN/ftc/RefLemma/HMeshR.var".
269 inline "cic:/CoRN/ftc/RefLemma/fP.var".
271 inline "cic:/CoRN/ftc/RefLemma/HfP.var".
273 inline "cic:/CoRN/ftc/RefLemma/HfP'.var".
275 inline "cic:/CoRN/ftc/RefLemma/fR.var".
277 inline "cic:/CoRN/ftc/RefLemma/HfR.var".
279 inline "cic:/CoRN/ftc/RefLemma/HfR'.var".
281 inline "cic:/CoRN/ftc/RefLemma/second_refinement_lemma.con".
284 End Second_Refinement_Lemma.
288 Section Third_Refinement_Lemma.
292 This is an approximation of inequality (2.6.7), but without assuming the existence of a common refinement of [P] and [R].
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],
302 - [beta] is a positive real number.
307 inline "cic:/CoRN/ftc/RefLemma/n.var".
309 inline "cic:/CoRN/ftc/RefLemma/m.var".
311 inline "cic:/CoRN/ftc/RefLemma/P.var".
313 inline "cic:/CoRN/ftc/RefLemma/R.var".
315 inline "cic:/CoRN/ftc/RefLemma/e.var".
317 inline "cic:/CoRN/ftc/RefLemma/e'.var".
319 inline "cic:/CoRN/ftc/RefLemma/He.var".
321 inline "cic:/CoRN/ftc/RefLemma/He'.var".
325 inline "cic:/CoRN/ftc/RefLemma/d.con".
327 inline "cic:/CoRN/ftc/RefLemma/d'.con".
331 inline "cic:/CoRN/ftc/RefLemma/HMeshP.var".
333 inline "cic:/CoRN/ftc/RefLemma/HMeshR.var".
335 inline "cic:/CoRN/ftc/RefLemma/fP.var".
337 inline "cic:/CoRN/ftc/RefLemma/HfP.var".
339 inline "cic:/CoRN/ftc/RefLemma/HfP'.var".
341 inline "cic:/CoRN/ftc/RefLemma/fR.var".
343 inline "cic:/CoRN/ftc/RefLemma/HfR.var".
345 inline "cic:/CoRN/ftc/RefLemma/HfR'.var".
347 inline "cic:/CoRN/ftc/RefLemma/Hab'.var".
349 inline "cic:/CoRN/ftc/RefLemma/beta.var".
351 inline "cic:/CoRN/ftc/RefLemma/Hbeta.var".
355 inline "cic:/CoRN/ftc/RefLemma/alpha.con".
357 inline "cic:/CoRN/ftc/RefLemma/RL_alpha.con".
359 inline "cic:/CoRN/ftc/RefLemma/csi1.con".
361 inline "cic:/CoRN/ftc/RefLemma/RL_csi1.con".
363 inline "cic:/CoRN/ftc/RefLemma/delta1.con".
365 inline "cic:/CoRN/ftc/RefLemma/RL_delta1.con".
367 inline "cic:/CoRN/ftc/RefLemma/P'.con".
369 inline "cic:/CoRN/ftc/RefLemma/RL_P'_sep.con".
371 inline "cic:/CoRN/ftc/RefLemma/RL_P'_Mesh.con".
373 inline "cic:/CoRN/ftc/RefLemma/fP'.con".
375 inline "cic:/CoRN/ftc/RefLemma/RL_fP'_in_P'.con".
377 inline "cic:/CoRN/ftc/RefLemma/RL_P'_P_sum.con".
379 inline "cic:/CoRN/ftc/RefLemma/csi2.con".
381 inline "cic:/CoRN/ftc/RefLemma/RL_csi2.con".
383 inline "cic:/CoRN/ftc/RefLemma/delta2.con".
385 inline "cic:/CoRN/ftc/RefLemma/RL_delta2.con".
387 inline "cic:/CoRN/ftc/RefLemma/R'.con".
389 inline "cic:/CoRN/ftc/RefLemma/RL_R'_sep.con".
391 inline "cic:/CoRN/ftc/RefLemma/RL_R'_Mesh.con".
393 inline "cic:/CoRN/ftc/RefLemma/fR'.con".
395 inline "cic:/CoRN/ftc/RefLemma/RL_fR'_in_R'.con".
397 inline "cic:/CoRN/ftc/RefLemma/RL_R'_R_sum.con".
399 inline "cic:/CoRN/ftc/RefLemma/csi3.con".
401 inline "cic:/CoRN/ftc/RefLemma/RL_csi3.con".
403 inline "cic:/CoRN/ftc/RefLemma/Q.con".
405 inline "cic:/CoRN/ftc/RefLemma/RL_Q_Mesh.con".
407 inline "cic:/CoRN/ftc/RefLemma/RL_Q_sep.con".
409 inline "cic:/CoRN/ftc/RefLemma/fQ.con".
411 inline "cic:/CoRN/ftc/RefLemma/RL_fQ_in_Q.con".
413 inline "cic:/CoRN/ftc/RefLemma/RL_Q_P'_sum.con".
417 inline "cic:/CoRN/ftc/RefLemma/third_refinement_lemma.con".
420 End Third_Refinement_Lemma.
424 Section Fourth_Refinement_Lemma.
429 inline "cic:/CoRN/ftc/RefLemma/Fa.con".
431 inline "cic:/CoRN/ftc/RefLemma/RL_sum_lemma_aux.con".
436 Finally, this is inequality (2.6.7) exactly as stated (same conventions as
440 inline "cic:/CoRN/ftc/RefLemma/n.var".
442 inline "cic:/CoRN/ftc/RefLemma/m.var".
444 inline "cic:/CoRN/ftc/RefLemma/P.var".
446 inline "cic:/CoRN/ftc/RefLemma/R.var".
448 inline "cic:/CoRN/ftc/RefLemma/e.var".
450 inline "cic:/CoRN/ftc/RefLemma/e'.var".
452 inline "cic:/CoRN/ftc/RefLemma/He.var".
454 inline "cic:/CoRN/ftc/RefLemma/He'.var".
458 inline "cic:/CoRN/ftc/RefLemma/d.con".
460 inline "cic:/CoRN/ftc/RefLemma/d'.con".
464 inline "cic:/CoRN/ftc/RefLemma/HMeshP.var".
466 inline "cic:/CoRN/ftc/RefLemma/HMeshR.var".
468 inline "cic:/CoRN/ftc/RefLemma/fP.var".
470 inline "cic:/CoRN/ftc/RefLemma/HfP.var".
472 inline "cic:/CoRN/ftc/RefLemma/HfP'.var".
474 inline "cic:/CoRN/ftc/RefLemma/fR.var".
476 inline "cic:/CoRN/ftc/RefLemma/HfR.var".
478 inline "cic:/CoRN/ftc/RefLemma/HfR'.var".
482 inline "cic:/CoRN/ftc/RefLemma/Hab'.var".
486 inline "cic:/CoRN/ftc/RefLemma/fourth_refinement_lemma.con".
489 End Fourth_Refinement_Lemma.
493 Section Main_Refinement_Lemma.
496 (*#* We finish by presenting Theorem 9. *)
498 inline "cic:/CoRN/ftc/RefLemma/n.var".
500 inline "cic:/CoRN/ftc/RefLemma/m.var".
502 inline "cic:/CoRN/ftc/RefLemma/P.var".
504 inline "cic:/CoRN/ftc/RefLemma/R.var".
506 inline "cic:/CoRN/ftc/RefLemma/e.var".
508 inline "cic:/CoRN/ftc/RefLemma/e'.var".
510 inline "cic:/CoRN/ftc/RefLemma/He.var".
512 inline "cic:/CoRN/ftc/RefLemma/He'.var".
516 inline "cic:/CoRN/ftc/RefLemma/d.con".
518 inline "cic:/CoRN/ftc/RefLemma/d'.con".
522 inline "cic:/CoRN/ftc/RefLemma/HMeshP.var".
524 inline "cic:/CoRN/ftc/RefLemma/HMeshR.var".
526 inline "cic:/CoRN/ftc/RefLemma/fP.var".
528 inline "cic:/CoRN/ftc/RefLemma/HfP.var".
530 inline "cic:/CoRN/ftc/RefLemma/HfP'.var".
532 inline "cic:/CoRN/ftc/RefLemma/fR.var".
534 inline "cic:/CoRN/ftc/RefLemma/HfR.var".
536 inline "cic:/CoRN/ftc/RefLemma/HfR'.var".
538 inline "cic:/CoRN/ftc/RefLemma/refinement_lemma.con".
541 End Main_Refinement_Lemma.
545 End Refinement_Lemma.