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.
110 alias id "a" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/a.var".
112 alias id "b" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/b.var".
114 alias id "Hab" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/Hab.var".
116 alias id "m" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/m.var".
118 alias id "n" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/n.var".
120 alias id "P" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/P.var".
122 alias id "Q" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/Q.var".
125 We now define what it means for a partition [Q] to be a refinement of
126 [P] and prove the main property of refinements.
129 inline procedural "cic:/CoRN/ftc/Partitions/Refinement.con" as definition.
131 inline procedural "cic:/CoRN/ftc/Partitions/Refinement_prop.con" as lemma.
134 We will also need to consider arbitrary sums %of the form
135 \[\sum_{i=0}^{n-1}f(x_i)(a_{i+1}-a_i)\]%#of
136 f(x<sub>i</sub>)(a<sub>i+1</sub>-a<sub>i</sub>)# where
137 $x_i\in[a_i,a_{i+1}]$#x<sub>i</sub>∈[a<sub>i</sub>,a<sub>i+1</sub>]#.
138 For this, we again need a choice function [x] which has to satisfy
139 some condition. We define the condition and the sum for a fixed [P]:
142 inline procedural "cic:/CoRN/ftc/Partitions/Points_in_Partition.con" as definition.
144 inline procedural "cic:/CoRN/ftc/Partitions/Pts_part_lemma.con" as lemma.
146 inline procedural "cic:/CoRN/ftc/Partitions/Partition_Sum.con" as definition.
153 Implicit Arguments Points_in_Partition [a b Hab n].
157 Implicit Arguments Partition_Sum [a b Hab n P g F].
162 We now formalize some trivial and helpful constructions.
164 %\begin{convention}% We will assume a fixed compact interval [[a,b]], denoted by [I].
168 alias id "a" = "cic:/CoRN/ftc/Partitions/Definitions/a.var".
170 alias id "b" = "cic:/CoRN/ftc/Partitions/Definitions/b.var".
172 alias id "Hab" = "cic:/CoRN/ftc/Partitions/Definitions/Hab.var".
176 inline procedural "cic:/CoRN/ftc/Partitions/Definitions/I.con" "Definitions__" as definition.
181 Section Getting_Points
185 From a partition we always have a canonical choice of points at which
186 to evaluate a function: just take all but the last points of the
189 %\begin{convention}% Let [Q] be a partition of [I] with [m] points.
193 alias id "m" = "cic:/CoRN/ftc/Partitions/Definitions/Getting_Points/m.var".
195 alias id "Q" = "cic:/CoRN/ftc/Partitions/Definitions/Getting_Points/Q.var".
197 inline procedural "cic:/CoRN/ftc/Partitions/Partition_imp_points.con" as definition.
199 inline procedural "cic:/CoRN/ftc/Partitions/Partition_imp_points_1.con" as lemma.
201 inline procedural "cic:/CoRN/ftc/Partitions/Partition_imp_points_2.con" as lemma.
208 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]].
211 alias id "F" = "cic:/CoRN/ftc/Partitions/Definitions/F.var".
213 alias id "contF" = "cic:/CoRN/ftc/Partitions/Definitions/contF.var".
215 inline procedural "cic:/CoRN/ftc/Partitions/Even_Partition_Sum.con" as definition.
222 Implicit Arguments Partition [a b].
226 Implicit Arguments Partition_Dom [a b Hab n].
230 Implicit Arguments Mesh [a b Hab n].
234 Implicit Arguments AntiMesh [a b Hab n].
238 Implicit Arguments Pts [a b Hab lng].
242 Implicit Arguments Part_Mesh_List [n a b Hab].
246 Implicit Arguments Points_in_Partition [a b Hab n].
250 Implicit Arguments Partition_Sum [a b Hab n P g F].
254 Implicit Arguments Even_Partition [a b].
258 Implicit Arguments Even_Partition_Sum [a b].
262 Implicit Arguments Refinement [a b Hab n m].
266 Hint Resolve start finish: algebra.
273 (*#* ** Properties of the mesh
275 If a partition has more than one point then its mesh list is nonempty.
278 inline procedural "cic:/CoRN/ftc/Partitions/length_Part_Mesh_List.con" as lemma.
281 Any element of the auxiliary list defined to calculate the mesh of a partition has a very specific form.
284 inline procedural "cic:/CoRN/ftc/Partitions/Part_Mesh_List_lemma.con" as lemma.
287 Mesh and antimesh are always nonnegative.
290 inline procedural "cic:/CoRN/ftc/Partitions/Mesh_nonneg.con" as lemma.
292 inline procedural "cic:/CoRN/ftc/Partitions/AntiMesh_nonneg.con" as lemma.
295 Most important, [AntiMesh] and [Mesh] provide lower and upper bounds
296 for the distance between any two consecutive points in a partition.
298 %\begin{convention}% Let [I] be [[a,b]] and [P] be a partition of [I]
303 alias id "a" = "cic:/CoRN/ftc/Partitions/Lemmas/a.var".
305 alias id "b" = "cic:/CoRN/ftc/Partitions/Lemmas/b.var".
309 inline procedural "cic:/CoRN/ftc/Partitions/Lemmas/I.con" "Lemmas__" as definition.
313 alias id "Hab" = "cic:/CoRN/ftc/Partitions/Lemmas/Hab.var".
315 alias id "n" = "cic:/CoRN/ftc/Partitions/Lemmas/n.var".
317 alias id "P" = "cic:/CoRN/ftc/Partitions/Lemmas/P.var".
319 inline procedural "cic:/CoRN/ftc/Partitions/Mesh_lemma.con" as lemma.
321 inline procedural "cic:/CoRN/ftc/Partitions/AntiMesh_lemma.con" as lemma.
323 inline procedural "cic:/CoRN/ftc/Partitions/Mesh_leEq.con" as lemma.
330 Section Even_Partitions
333 (*#* More technical stuff. Two equal partitions have the same mesh.
336 inline procedural "cic:/CoRN/ftc/Partitions/Mesh_wd.con" as lemma.
338 inline procedural "cic:/CoRN/ftc/Partitions/Mesh_wd'.con" as lemma.
341 The mesh of an even partition is easily calculated.
344 inline procedural "cic:/CoRN/ftc/Partitions/even_partition_Mesh.con" as lemma.
346 (*#* ** Miscellaneous
347 %\begin{convention}% Throughout this section, let [a,b:IR] and [I] be [[a,b]].
351 alias id "a" = "cic:/CoRN/ftc/Partitions/Even_Partitions/a.var".
353 alias id "b" = "cic:/CoRN/ftc/Partitions/Even_Partitions/b.var".
357 inline procedural "cic:/CoRN/ftc/Partitions/Even_Partitions/I.con" "Even_Partitions__" as definition.
361 alias id "Hab" = "cic:/CoRN/ftc/Partitions/Even_Partitions/Hab.var".
364 An interesting property: in a partition, if [ai [<] aj] then [i < j].
367 inline procedural "cic:/CoRN/ftc/Partitions/Partition_Points_mon.con" as lemma.
369 inline procedural "cic:/CoRN/ftc/Partitions/refinement_resp_mult.con" as lemma.
372 %\begin{convention}% Assume [m,n] are positive natural numbers and
373 denote by [P] and [Q] the even partitions with, respectively, [m] and
377 Even partitions always have a common refinement.
380 alias id "m" = "cic:/CoRN/ftc/Partitions/Even_Partitions/m.var".
382 alias id "n" = "cic:/CoRN/ftc/Partitions/Even_Partitions/n.var".
384 alias id "Hm" = "cic:/CoRN/ftc/Partitions/Even_Partitions/Hm.var".
386 alias id "Hn" = "cic:/CoRN/ftc/Partitions/Even_Partitions/Hn.var".
390 inline procedural "cic:/CoRN/ftc/Partitions/Even_Partitions/P.con" "Even_Partitions__" as definition.
392 inline procedural "cic:/CoRN/ftc/Partitions/Even_Partitions/Q.con" "Even_Partitions__" as definition.
396 inline procedural "cic:/CoRN/ftc/Partitions/even_partition_refinement.con" as lemma.
403 Section More_Definitions
408 Some auxiliary definitions. A partition is said to be separated if all its points are distinct.
411 alias id "a" = "cic:/CoRN/ftc/Partitions/More_Definitions/a.var".
413 alias id "b" = "cic:/CoRN/ftc/Partitions/More_Definitions/b.var".
415 alias id "Hab" = "cic:/CoRN/ftc/Partitions/More_Definitions/Hab.var".
417 inline procedural "cic:/CoRN/ftc/Partitions/_Separated.con" as definition.
420 Two partitions are said to be (mutually) separated if they are both
421 separated and all their points are distinct (except for the
424 %\begin{convention}% Let [P,Q] be partitions of [I] with,
425 respectively, [n] and [m] points.
429 alias id "n" = "cic:/CoRN/ftc/Partitions/More_Definitions/n.var".
431 alias id "m" = "cic:/CoRN/ftc/Partitions/More_Definitions/m.var".
433 alias id "P" = "cic:/CoRN/ftc/Partitions/More_Definitions/P.var".
435 alias id "Q" = "cic:/CoRN/ftc/Partitions/More_Definitions/Q.var".
437 inline procedural "cic:/CoRN/ftc/Partitions/Separated.con" as definition.
444 Implicit Arguments _Separated [a b Hab n].
448 Implicit Arguments Separated [a b Hab n m].
452 Section Sep_Partitions
455 alias id "a" = "cic:/CoRN/ftc/Partitions/Sep_Partitions/a.var".
457 alias id "b" = "cic:/CoRN/ftc/Partitions/Sep_Partitions/b.var".
461 inline procedural "cic:/CoRN/ftc/Partitions/Sep_Partitions/I.con" "Sep_Partitions__" as definition.
465 alias id "Hab" = "cic:/CoRN/ftc/Partitions/Sep_Partitions/Hab.var".
468 The antimesh of a separated partition is always positive.
471 inline procedural "cic:/CoRN/ftc/Partitions/pos_AntiMesh.con" as lemma.
474 A partition can have only one point iff the endpoints of the interval
475 are the same; moreover, if the partition is separated and the
476 endpoints of the interval are the same then it must have one point.
479 inline procedural "cic:/CoRN/ftc/Partitions/partition_length_zero.con" as lemma.
481 inline procedural "cic:/CoRN/ftc/Partitions/_Separated_imp_length_zero.con" as lemma.
483 inline procedural "cic:/CoRN/ftc/Partitions/partition_less_imp_gt_zero.con" as lemma.