The Refinement Lemmas

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): Theorem Let f be a continuous function on a compact interval [a,b] with modulus of continuity (From our point of view, the modulus of continuity is simply the proof that f is continuous.) omega. Let P be a partition of [a,b] and eps [>] [0] be such that mesh(P) [<] omega(eps). Then |S(f,P)-∫f(x)dx|≤ε(b-a) where S(f,P) denotes any sum of the function f respecting the partition P (as previously defined). The proof of this theorem relies on the fact that for any two partitions P and R of [a,b] it is possible to define a partition Q which is ``almost'' a common refinement of P and R---that is, given eps [>] [0] it is possible to define Q such that for every point x of either P or R there is a point y of Q such that |x[-]y| [<] eps. This requires three separate constructions (done in three separate files) which are then properly combined to give the final result. We recommend the reader to ignore this technical constructions. First we prove that if P and R are both separated (though not necessarily separated from each other) then we can define a partition P' arbitrarily close to P (that is, such that given alpha [>] [0] and xi [>] [0] P' satisfies both mesh(P') [<] mesh(P) [+] xi and for every choice of points x_i respecting P there is a choice of points x'_i respecting P' such that |S(f,P)-S(f,P')| [<] alpha) that is separated from R. Then we prove that given any partition P and assuming a [#] b we can define a partition P' arbitrarily close to P (in the same sense as above) which is separated. Finally we prove that every two separated partitions P and R have a common refinement---as every two points in P and R are apart, we can decide which one is smaller. We use here the technical results about ordering that we proved in the file IntegralLemmas.v. Using the results from these files, we prove our main lemma in several steps (and versions). Throughout this section:

• a,b:IR and I denotes [a,b];
• F is a partial function continuous in I.

This is the first part of the proof of Theorem 2.9.

• P, Q are partitions of I with, respectively, n and m points;
• Q is a refinement of P;
• e is a positive real number;
• d is the modulus of continuity of F for e;
• the mesh of P is less or equal to d;
• fP and fQ are choices of points respecting the partitions P and Q,

respectively.

This is inequality (2.6.7).

• P, Q, R are partitions of I with, respectively, j, n and k points;
• Q is a common refinement of P and R;
• e, e' are positive real numbers;
• d, d' are the moduli of continuity of F for e, e';
• the Mesh of P is less or equal to d;
• the Mesh of R is less or equal to d';
• fP, fQ and fR are choices of points respecting the partitions P, Q

and R, respectively.

This is an approximation of inequality (2.6.7), but without assuming the existence of a common refinement of P and R.

• P, R are partitions of I with, respectively, n and m points;
• e, e' are positive real numbers;
• d, d' are the moduli of continuity of F for e, e';
• the Mesh of P is less than d;
• the Mesh of R is less than d';
• fP and fR are choices of points respecting the partitions P and R,

respectively;

• beta is a positive real number.

Finally, this is inequality (2.6.7) exactly as stated (same conventions as above)

We finish by presenting Theorem 9.