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 *********************)
19 (* $Id: Partitions.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *)
21 include "ftc/Continuity.ma".
23 (*#* printing Partition_Sum %\ensuremath{\sum_P}% #∑<sub>P</sub># *)
31 We now begin to lay the way for the definition of Riemann integral. This will
32 be done through the definition of a sequence of
33 sums that is proved to be convergent; in order to do that, we first
34 need to do a bit of work on partitions.
38 A partition is defined as a record type. For each compact interval [[a,b]]
39 and each natural number [n], a partition of [[a,b]] with [n+1] points is a
40 choice of real numbers [a [=] a0 [<=] a1 [<=] an [=] b]; the following
41 specification works as follows:
42 - [Pts] is the function that chooses the points (it is declared as a
44 - [prf1] states that [Pts] is a setoid function;
45 - [prf2] states that the points are ordered;
46 - [start] requires that [a0 [=] a] and
47 - [finish] requires that [an [=] b].
51 inline procedural "cic:/CoRN/ftc/Partitions/Partition.ind".
54 cic:/matita/CoRN-Procedural/ftc/Partitions/Pts.con
57 (*#* Two immediate consequences of this are that [ai [<=] aj] whenever
58 [i < j] and that [ai] is in [[a,b]] for all [i].
61 inline procedural "cic:/CoRN/ftc/Partitions/Partition_mon.con" as lemma.
63 inline procedural "cic:/CoRN/ftc/Partitions/Partition_in_compact.con" as lemma.
66 Each partition of [[a,b]] implies a partition of the interval
67 $[a,a_{n-1}]$#[a,a<sub>n-1</sub>]#. This partition will play an
68 important role in much of our future work, so we take some care to
72 inline procedural "cic:/CoRN/ftc/Partitions/part_pred_lemma.con" as lemma.
74 inline procedural "cic:/CoRN/ftc/Partitions/Partition_Dom.con" as definition.
77 The mesh of a partition is the greatest distance between two
78 consecutive points. For convenience's sake we also define the dual
79 concept, which is very helpful in some situations. In order to do
80 this, we begin by building a list with all the distances between
81 consecutive points; next we only need to extract the maximum and the
82 minimum of this list. Notice that this list is nonempty except in the
83 case when [a [=] b] and [n = 0]; this means that the convention we took
84 of defining the minimum and maximum of the empty list to be [0] actually
85 helps us in this case.
88 inline procedural "cic:/CoRN/ftc/Partitions/Part_Mesh_List.con" as definition.
90 inline procedural "cic:/CoRN/ftc/Partitions/Mesh.con" as definition.
92 inline procedural "cic:/CoRN/ftc/Partitions/AntiMesh.con" as definition.
95 Even partitions (partitions where all the points are evenly spaced)
96 will also play a central role in our work; the first two lemmas are
97 presented simply to make the definition of even partition lighter.
100 inline procedural "cic:/CoRN/ftc/Partitions/even_part_1.con" as lemma.
102 inline procedural "cic:/CoRN/ftc/Partitions/even_part_2.con" as lemma.
104 inline procedural "cic:/CoRN/ftc/Partitions/Even_Partition.con" as definition.
111 cic:/CoRN/ftc/Partitions/Definitions/Refinements/a.var
115 cic:/CoRN/ftc/Partitions/Definitions/Refinements/b.var
119 cic:/CoRN/ftc/Partitions/Definitions/Refinements/Hab.var
123 cic:/CoRN/ftc/Partitions/Definitions/Refinements/m.var
127 cic:/CoRN/ftc/Partitions/Definitions/Refinements/n.var
131 cic:/CoRN/ftc/Partitions/Definitions/Refinements/P.var
135 cic:/CoRN/ftc/Partitions/Definitions/Refinements/Q.var
139 We now define what it means for a partition [Q] to be a refinement of
140 [P] and prove the main property of refinements.
143 inline procedural "cic:/CoRN/ftc/Partitions/Refinement.con" as definition.
145 inline procedural "cic:/CoRN/ftc/Partitions/Refinement_prop.con" as lemma.
148 We will also need to consider arbitrary sums %of the form
149 \[\sum_{i=0}^{n-1}f(x_i)(a_{i+1}-a_i)\]%#of
150 f(x<sub>i</sub>)(a<sub>i+1</sub>-a<sub>i</sub>)# where
151 $x_i\in[a_i,a_{i+1}]$#x<sub>i</sub>∈[a<sub>i</sub>,a<sub>i+1</sub>]#.
152 For this, we again need a choice function [x] which has to satisfy
153 some condition. We define the condition and the sum for a fixed [P]:
156 inline procedural "cic:/CoRN/ftc/Partitions/Points_in_Partition.con" as definition.
158 inline procedural "cic:/CoRN/ftc/Partitions/Pts_part_lemma.con" as lemma.
160 inline procedural "cic:/CoRN/ftc/Partitions/Partition_Sum.con" as definition.
167 Implicit Arguments Points_in_Partition [a b Hab n].
171 Implicit Arguments Partition_Sum [a b Hab n P g F].
176 We now formalize some trivial and helpful constructions.
178 %\begin{convention}% We will assume a fixed compact interval [[a,b]], denoted by [I].
183 cic:/CoRN/ftc/Partitions/Definitions/a.var
187 cic:/CoRN/ftc/Partitions/Definitions/b.var
191 cic:/CoRN/ftc/Partitions/Definitions/Hab.var
196 inline procedural "cic:/CoRN/ftc/Partitions/Definitions/I.con" "Definitions__" as definition.
201 Section Getting_Points
205 From a partition we always have a canonical choice of points at which
206 to evaluate a function: just take all but the last points of the
209 %\begin{convention}% Let [Q] be a partition of [I] with [m] points.
214 cic:/CoRN/ftc/Partitions/Definitions/Getting_Points/m.var
218 cic:/CoRN/ftc/Partitions/Definitions/Getting_Points/Q.var
221 inline procedural "cic:/CoRN/ftc/Partitions/Partition_imp_points.con" as definition.
223 inline procedural "cic:/CoRN/ftc/Partitions/Partition_imp_points_1.con" as lemma.
225 inline procedural "cic:/CoRN/ftc/Partitions/Partition_imp_points_2.con" as lemma.
232 As a corollary, given any continuous function [F] and a natural number we have an immediate choice of a sum of [F] in [[a,b]].
236 cic:/CoRN/ftc/Partitions/Definitions/F.var
240 cic:/CoRN/ftc/Partitions/Definitions/contF.var
243 inline procedural "cic:/CoRN/ftc/Partitions/Even_Partition_Sum.con" as definition.
250 Implicit Arguments Partition [a b].
254 Implicit Arguments Partition_Dom [a b Hab n].
258 Implicit Arguments Mesh [a b Hab n].
262 Implicit Arguments AntiMesh [a b Hab n].
266 Implicit Arguments Pts [a b Hab lng].
270 Implicit Arguments Part_Mesh_List [n a b Hab].
274 Implicit Arguments Points_in_Partition [a b Hab n].
278 Implicit Arguments Partition_Sum [a b Hab n P g F].
282 Implicit Arguments Even_Partition [a b].
286 Implicit Arguments Even_Partition_Sum [a b].
290 Implicit Arguments Refinement [a b Hab n m].
294 Hint Resolve start finish: algebra.
301 (*#* ** Properties of the mesh
303 If a partition has more than one point then its mesh list is nonempty.
306 inline procedural "cic:/CoRN/ftc/Partitions/length_Part_Mesh_List.con" as lemma.
309 Any element of the auxiliary list defined to calculate the mesh of a partition has a very specific form.
312 inline procedural "cic:/CoRN/ftc/Partitions/Part_Mesh_List_lemma.con" as lemma.
315 Mesh and antimesh are always nonnegative.
318 inline procedural "cic:/CoRN/ftc/Partitions/Mesh_nonneg.con" as lemma.
320 inline procedural "cic:/CoRN/ftc/Partitions/AntiMesh_nonneg.con" as lemma.
323 Most important, [AntiMesh] and [Mesh] provide lower and upper bounds
324 for the distance between any two consecutive points in a partition.
326 %\begin{convention}% Let [I] be [[a,b]] and [P] be a partition of [I]
332 cic:/CoRN/ftc/Partitions/Lemmas/a.var
336 cic:/CoRN/ftc/Partitions/Lemmas/b.var
341 inline procedural "cic:/CoRN/ftc/Partitions/Lemmas/I.con" "Lemmas__" as definition.
346 cic:/CoRN/ftc/Partitions/Lemmas/Hab.var
350 cic:/CoRN/ftc/Partitions/Lemmas/n.var
354 cic:/CoRN/ftc/Partitions/Lemmas/P.var
357 inline procedural "cic:/CoRN/ftc/Partitions/Mesh_lemma.con" as lemma.
359 inline procedural "cic:/CoRN/ftc/Partitions/AntiMesh_lemma.con" as lemma.
361 inline procedural "cic:/CoRN/ftc/Partitions/Mesh_leEq.con" as lemma.
368 Section Even_Partitions
371 (*#* More technical stuff. Two equal partitions have the same mesh.
374 inline procedural "cic:/CoRN/ftc/Partitions/Mesh_wd.con" as lemma.
376 inline procedural "cic:/CoRN/ftc/Partitions/Mesh_wd'.con" as lemma.
379 The mesh of an even partition is easily calculated.
382 inline procedural "cic:/CoRN/ftc/Partitions/even_partition_Mesh.con" as lemma.
384 (*#* ** Miscellaneous
385 %\begin{convention}% Throughout this section, let [a,b:IR] and [I] be [[a,b]].
390 cic:/CoRN/ftc/Partitions/Even_Partitions/a.var
394 cic:/CoRN/ftc/Partitions/Even_Partitions/b.var
399 inline procedural "cic:/CoRN/ftc/Partitions/Even_Partitions/I.con" "Even_Partitions__" as definition.
404 cic:/CoRN/ftc/Partitions/Even_Partitions/Hab.var
408 An interesting property: in a partition, if [ai [<] aj] then [i < j].
411 inline procedural "cic:/CoRN/ftc/Partitions/Partition_Points_mon.con" as lemma.
413 inline procedural "cic:/CoRN/ftc/Partitions/refinement_resp_mult.con" as lemma.
416 %\begin{convention}% Assume [m,n] are positive natural numbers and
417 denote by [P] and [Q] the even partitions with, respectively, [m] and
421 Even partitions always have a common refinement.
425 cic:/CoRN/ftc/Partitions/Even_Partitions/m.var
429 cic:/CoRN/ftc/Partitions/Even_Partitions/n.var
433 cic:/CoRN/ftc/Partitions/Even_Partitions/Hm.var
437 cic:/CoRN/ftc/Partitions/Even_Partitions/Hn.var
442 inline procedural "cic:/CoRN/ftc/Partitions/Even_Partitions/P.con" "Even_Partitions__" as definition.
444 inline procedural "cic:/CoRN/ftc/Partitions/Even_Partitions/Q.con" "Even_Partitions__" as definition.
448 inline procedural "cic:/CoRN/ftc/Partitions/even_partition_refinement.con" as lemma.
455 Section More_Definitions
460 Some auxiliary definitions. A partition is said to be separated if all its points are distinct.
464 cic:/CoRN/ftc/Partitions/More_Definitions/a.var
468 cic:/CoRN/ftc/Partitions/More_Definitions/b.var
472 cic:/CoRN/ftc/Partitions/More_Definitions/Hab.var
475 inline procedural "cic:/CoRN/ftc/Partitions/_Separated.con" as definition.
478 Two partitions are said to be (mutually) separated if they are both
479 separated and all their points are distinct (except for the
482 %\begin{convention}% Let [P,Q] be partitions of [I] with,
483 respectively, [n] and [m] points.
488 cic:/CoRN/ftc/Partitions/More_Definitions/n.var
492 cic:/CoRN/ftc/Partitions/More_Definitions/m.var
496 cic:/CoRN/ftc/Partitions/More_Definitions/P.var
500 cic:/CoRN/ftc/Partitions/More_Definitions/Q.var
503 inline procedural "cic:/CoRN/ftc/Partitions/Separated.con" as definition.
510 Implicit Arguments _Separated [a b Hab n].
514 Implicit Arguments Separated [a b Hab n m].
518 Section Sep_Partitions
522 cic:/CoRN/ftc/Partitions/Sep_Partitions/a.var
526 cic:/CoRN/ftc/Partitions/Sep_Partitions/b.var
531 inline procedural "cic:/CoRN/ftc/Partitions/Sep_Partitions/I.con" "Sep_Partitions__" as definition.
536 cic:/CoRN/ftc/Partitions/Sep_Partitions/Hab.var
540 The antimesh of a separated partition is always positive.
543 inline procedural "cic:/CoRN/ftc/Partitions/pos_AntiMesh.con" as lemma.
546 A partition can have only one point iff the endpoints of the interval
547 are the same; moreover, if the partition is separated and the
548 endpoints of the interval are the same then it must have one point.
551 inline procedural "cic:/CoRN/ftc/Partitions/partition_length_zero.con" as lemma.
553 inline procedural "cic:/CoRN/ftc/Partitions/_Separated_imp_length_zero.con" as lemma.
555 inline procedural "cic:/CoRN/ftc/Partitions/partition_less_imp_gt_zero.con" as lemma.