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".
197 inline "cic:/CoRN/ftc/RefLemma/ref_calc1.con".
200 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
204 Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)).
207 inline "cic:/CoRN/ftc/RefLemma/ref_calc2.con".
209 inline "cic:/CoRN/ftc/RefLemma/ref_calc3.con".
211 inline "cic:/CoRN/ftc/RefLemma/ref_calc4.con".
213 inline "cic:/CoRN/ftc/RefLemma/ref_calc5.con".
215 inline "cic:/CoRN/ftc/RefLemma/ref_calc6.con".
217 inline "cic:/CoRN/ftc/RefLemma/ref_calc7.con".
219 inline "cic:/CoRN/ftc/RefLemma/ref_calc8.con".
223 inline "cic:/CoRN/ftc/RefLemma/first_refinement_lemma.con".
226 End First_Refinement_Lemma.
230 Section Second_Refinement_Lemma.
234 This is inequality (2.6.7).
237 - [P, Q, R] are partitions of [I] with, respectively, [j, n] and [k] points;
238 - [Q] is a common refinement of [P] and [R];
239 - [e, e'] are positive real numbers;
240 - [d, d'] are the moduli of continuity of [F] for [e, e'];
241 - the Mesh of [P] is less or equal to [d];
242 - the Mesh of [R] is less or equal to [d'];
243 - [fP, fQ] and [fR] are choices of points respecting the partitions [P, Q]
244 and [R], respectively.
249 inline "cic:/CoRN/ftc/RefLemma/n.var".
251 inline "cic:/CoRN/ftc/RefLemma/j.var".
253 inline "cic:/CoRN/ftc/RefLemma/k.var".
255 inline "cic:/CoRN/ftc/RefLemma/P.var".
257 inline "cic:/CoRN/ftc/RefLemma/Q.var".
259 inline "cic:/CoRN/ftc/RefLemma/R.var".
261 inline "cic:/CoRN/ftc/RefLemma/HrefP.var".
263 inline "cic:/CoRN/ftc/RefLemma/HrefR.var".
265 inline "cic:/CoRN/ftc/RefLemma/e.var".
267 inline "cic:/CoRN/ftc/RefLemma/e'.var".
269 inline "cic:/CoRN/ftc/RefLemma/He.var".
271 inline "cic:/CoRN/ftc/RefLemma/He'.var".
275 inline "cic:/CoRN/ftc/RefLemma/d.con".
277 inline "cic:/CoRN/ftc/RefLemma/d'.con".
281 inline "cic:/CoRN/ftc/RefLemma/HMeshP.var".
283 inline "cic:/CoRN/ftc/RefLemma/HMeshR.var".
285 inline "cic:/CoRN/ftc/RefLemma/fP.var".
287 inline "cic:/CoRN/ftc/RefLemma/HfP.var".
289 inline "cic:/CoRN/ftc/RefLemma/HfP'.var".
291 inline "cic:/CoRN/ftc/RefLemma/fR.var".
293 inline "cic:/CoRN/ftc/RefLemma/HfR.var".
295 inline "cic:/CoRN/ftc/RefLemma/HfR'.var".
297 inline "cic:/CoRN/ftc/RefLemma/second_refinement_lemma.con".
300 End Second_Refinement_Lemma.
304 Section Third_Refinement_Lemma.
308 This is an approximation of inequality (2.6.7), but without assuming the existence of a common refinement of [P] and [R].
311 - [P, R] are partitions of [I] with, respectively, [n] and [m] points;
312 - [e, e'] are positive real numbers;
313 - [d, d'] are the moduli of continuity of [F] for [e, e'];
314 - the Mesh of [P] is less than [d];
315 - the Mesh of [R] is less than [d'];
316 - [fP] and [fR] are choices of points respecting the partitions [P] and [R],
318 - [beta] is a positive real number.
323 inline "cic:/CoRN/ftc/RefLemma/n.var".
325 inline "cic:/CoRN/ftc/RefLemma/m.var".
327 inline "cic:/CoRN/ftc/RefLemma/P.var".
329 inline "cic:/CoRN/ftc/RefLemma/R.var".
331 inline "cic:/CoRN/ftc/RefLemma/e.var".
333 inline "cic:/CoRN/ftc/RefLemma/e'.var".
335 inline "cic:/CoRN/ftc/RefLemma/He.var".
337 inline "cic:/CoRN/ftc/RefLemma/He'.var".
341 inline "cic:/CoRN/ftc/RefLemma/d.con".
343 inline "cic:/CoRN/ftc/RefLemma/d'.con".
347 inline "cic:/CoRN/ftc/RefLemma/HMeshP.var".
349 inline "cic:/CoRN/ftc/RefLemma/HMeshR.var".
351 inline "cic:/CoRN/ftc/RefLemma/fP.var".
353 inline "cic:/CoRN/ftc/RefLemma/HfP.var".
355 inline "cic:/CoRN/ftc/RefLemma/HfP'.var".
357 inline "cic:/CoRN/ftc/RefLemma/fR.var".
359 inline "cic:/CoRN/ftc/RefLemma/HfR.var".
361 inline "cic:/CoRN/ftc/RefLemma/HfR'.var".
363 inline "cic:/CoRN/ftc/RefLemma/Hab'.var".
365 inline "cic:/CoRN/ftc/RefLemma/beta.var".
367 inline "cic:/CoRN/ftc/RefLemma/Hbeta.var".
371 inline "cic:/CoRN/ftc/RefLemma/alpha.con".
373 inline "cic:/CoRN/ftc/RefLemma/RL_alpha.con".
375 inline "cic:/CoRN/ftc/RefLemma/csi1.con".
377 inline "cic:/CoRN/ftc/RefLemma/RL_csi1.con".
379 inline "cic:/CoRN/ftc/RefLemma/delta1.con".
381 inline "cic:/CoRN/ftc/RefLemma/RL_delta1.con".
383 inline "cic:/CoRN/ftc/RefLemma/P'.con".
385 inline "cic:/CoRN/ftc/RefLemma/RL_P'_sep.con".
387 inline "cic:/CoRN/ftc/RefLemma/RL_P'_Mesh.con".
389 inline "cic:/CoRN/ftc/RefLemma/fP'.con".
391 inline "cic:/CoRN/ftc/RefLemma/RL_fP'_in_P'.con".
393 inline "cic:/CoRN/ftc/RefLemma/RL_P'_P_sum.con".
395 inline "cic:/CoRN/ftc/RefLemma/csi2.con".
397 inline "cic:/CoRN/ftc/RefLemma/RL_csi2.con".
399 inline "cic:/CoRN/ftc/RefLemma/delta2.con".
401 inline "cic:/CoRN/ftc/RefLemma/RL_delta2.con".
403 inline "cic:/CoRN/ftc/RefLemma/R'.con".
405 inline "cic:/CoRN/ftc/RefLemma/RL_R'_sep.con".
407 inline "cic:/CoRN/ftc/RefLemma/RL_R'_Mesh.con".
409 inline "cic:/CoRN/ftc/RefLemma/fR'.con".
411 inline "cic:/CoRN/ftc/RefLemma/RL_fR'_in_R'.con".
413 inline "cic:/CoRN/ftc/RefLemma/RL_R'_R_sum.con".
415 inline "cic:/CoRN/ftc/RefLemma/csi3.con".
417 inline "cic:/CoRN/ftc/RefLemma/RL_csi3.con".
419 inline "cic:/CoRN/ftc/RefLemma/Q.con".
421 inline "cic:/CoRN/ftc/RefLemma/RL_Q_Mesh.con".
423 inline "cic:/CoRN/ftc/RefLemma/RL_Q_sep.con".
425 inline "cic:/CoRN/ftc/RefLemma/fQ.con".
427 inline "cic:/CoRN/ftc/RefLemma/RL_fQ_in_Q.con".
429 inline "cic:/CoRN/ftc/RefLemma/RL_Q_P'_sum.con".
433 inline "cic:/CoRN/ftc/RefLemma/third_refinement_lemma.con".
436 End Third_Refinement_Lemma.
440 Section Fourth_Refinement_Lemma.
445 inline "cic:/CoRN/ftc/RefLemma/Fa.con".
448 Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)).
451 inline "cic:/CoRN/ftc/RefLemma/RL_sum_lemma_aux.con".
456 Finally, this is inequality (2.6.7) exactly as stated (same conventions as
460 inline "cic:/CoRN/ftc/RefLemma/n.var".
462 inline "cic:/CoRN/ftc/RefLemma/m.var".
464 inline "cic:/CoRN/ftc/RefLemma/P.var".
466 inline "cic:/CoRN/ftc/RefLemma/R.var".
468 inline "cic:/CoRN/ftc/RefLemma/e.var".
470 inline "cic:/CoRN/ftc/RefLemma/e'.var".
472 inline "cic:/CoRN/ftc/RefLemma/He.var".
474 inline "cic:/CoRN/ftc/RefLemma/He'.var".
478 inline "cic:/CoRN/ftc/RefLemma/d.con".
480 inline "cic:/CoRN/ftc/RefLemma/d'.con".
484 inline "cic:/CoRN/ftc/RefLemma/HMeshP.var".
486 inline "cic:/CoRN/ftc/RefLemma/HMeshR.var".
488 inline "cic:/CoRN/ftc/RefLemma/fP.var".
490 inline "cic:/CoRN/ftc/RefLemma/HfP.var".
492 inline "cic:/CoRN/ftc/RefLemma/HfP'.var".
494 inline "cic:/CoRN/ftc/RefLemma/fR.var".
496 inline "cic:/CoRN/ftc/RefLemma/HfR.var".
498 inline "cic:/CoRN/ftc/RefLemma/HfR'.var".
502 inline "cic:/CoRN/ftc/RefLemma/Hab'.var".
506 inline "cic:/CoRN/ftc/RefLemma/fourth_refinement_lemma.con".
509 End Fourth_Refinement_Lemma.
513 Section Main_Refinement_Lemma.
516 (*#* We finish by presenting Theorem 9. *)
518 inline "cic:/CoRN/ftc/RefLemma/n.var".
520 inline "cic:/CoRN/ftc/RefLemma/m.var".
522 inline "cic:/CoRN/ftc/RefLemma/P.var".
524 inline "cic:/CoRN/ftc/RefLemma/R.var".
526 inline "cic:/CoRN/ftc/RefLemma/e.var".
528 inline "cic:/CoRN/ftc/RefLemma/e'.var".
530 inline "cic:/CoRN/ftc/RefLemma/He.var".
532 inline "cic:/CoRN/ftc/RefLemma/He'.var".
536 inline "cic:/CoRN/ftc/RefLemma/d.con".
538 inline "cic:/CoRN/ftc/RefLemma/d'.con".
542 inline "cic:/CoRN/ftc/RefLemma/HMeshP.var".
544 inline "cic:/CoRN/ftc/RefLemma/HMeshR.var".
546 inline "cic:/CoRN/ftc/RefLemma/fP.var".
548 inline "cic:/CoRN/ftc/RefLemma/HfP.var".
550 inline "cic:/CoRN/ftc/RefLemma/HfP'.var".
552 inline "cic:/CoRN/ftc/RefLemma/fR.var".
554 inline "cic:/CoRN/ftc/RefLemma/HfR.var".
556 inline "cic:/CoRN/ftc/RefLemma/HfR'.var".
558 inline "cic:/CoRN/ftc/RefLemma/refinement_lemma.con".
561 End Main_Refinement_Lemma.
565 End Refinement_Lemma.