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/Partitions".
21 (* $Id: Partitions.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *)
23 include "ftc/Continuity.ma".
25 (*#* printing Partition_Sum %\ensuremath{\sum_P}% #∑<sub>P</sub># *)
33 We now begin to lay the way for the definition of Riemann integral. This will
34 be done through the definition of a sequence of
35 sums that is proved to be convergent; in order to do that, we first
36 need to do a bit of work on partitions.
40 A partition is defined as a record type. For each compact interval [[a,b]]
41 and each natural number [n], a partition of [[a,b]] with [n+1] points is a
42 choice of real numbers [a [=] a0 [<=] a1 [<=] an [=] b]; the following
43 specification works as follows:
44 - [Pts] is the function that chooses the points (it is declared as a
46 - [prf1] states that [Pts] is a setoid function;
47 - [prf2] states that the points are ordered;
48 - [start] requires that [a0 [=] a] and
49 - [finish] requires that [an [=] b].
53 inline "cic:/CoRN/ftc/Partitions/Partition.ind".
55 coercion cic:/matita/CoRN-Decl/ftc/Partitions/Pts.con 0 (* compounds *).
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 "cic:/CoRN/ftc/Partitions/Partition_mon.con".
63 inline "cic:/CoRN/ftc/Partitions/Partition_in_compact.con".
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 "cic:/CoRN/ftc/Partitions/part_pred_lemma.con".
74 inline "cic:/CoRN/ftc/Partitions/Partition_Dom.con".
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 "cic:/CoRN/ftc/Partitions/Part_Mesh_List.con".
90 inline "cic:/CoRN/ftc/Partitions/Mesh.con".
92 inline "cic:/CoRN/ftc/Partitions/AntiMesh.con".
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 "cic:/CoRN/ftc/Partitions/even_part_1.con".
102 inline "cic:/CoRN/ftc/Partitions/even_part_2.con".
104 inline "cic:/CoRN/ftc/Partitions/Even_Partition.con".
110 inline "cic:/CoRN/ftc/Partitions/a.var".
112 inline "cic:/CoRN/ftc/Partitions/b.var".
114 inline "cic:/CoRN/ftc/Partitions/Hab.var".
116 inline "cic:/CoRN/ftc/Partitions/m.var".
118 inline "cic:/CoRN/ftc/Partitions/n.var".
120 inline "cic:/CoRN/ftc/Partitions/P.var".
122 inline "cic:/CoRN/ftc/Partitions/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 "cic:/CoRN/ftc/Partitions/Refinement.con".
131 inline "cic:/CoRN/ftc/Partitions/Refinement_prop.con".
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 "cic:/CoRN/ftc/Partitions/Points_in_Partition.con".
144 inline "cic:/CoRN/ftc/Partitions/Pts_part_lemma.con".
146 inline "cic:/CoRN/ftc/Partitions/Partition_Sum.con".
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 inline "cic:/CoRN/ftc/Partitions/a.var".
170 inline "cic:/CoRN/ftc/Partitions/b.var".
172 inline "cic:/CoRN/ftc/Partitions/Hab.var".
176 inline "cic:/CoRN/ftc/Partitions/I.con".
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 inline "cic:/CoRN/ftc/Partitions/m.var".
195 inline "cic:/CoRN/ftc/Partitions/Q.var".
197 inline "cic:/CoRN/ftc/Partitions/Partition_imp_points.con".
199 inline "cic:/CoRN/ftc/Partitions/Partition_imp_points_1.con".
201 inline "cic:/CoRN/ftc/Partitions/Partition_imp_points_2.con".
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 inline "cic:/CoRN/ftc/Partitions/F.var".
213 inline "cic:/CoRN/ftc/Partitions/contF.var".
215 inline "cic:/CoRN/ftc/Partitions/Even_Partition_Sum.con".
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 "cic:/CoRN/ftc/Partitions/length_Part_Mesh_List.con".
281 Any element of the auxiliary list defined to calculate the mesh of a partition has a very specific form.
284 inline "cic:/CoRN/ftc/Partitions/Part_Mesh_List_lemma.con".
287 Mesh and antimesh are always nonnegative.
290 inline "cic:/CoRN/ftc/Partitions/Mesh_nonneg.con".
292 inline "cic:/CoRN/ftc/Partitions/AntiMesh_nonneg.con".
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 inline "cic:/CoRN/ftc/Partitions/a.var".
305 inline "cic:/CoRN/ftc/Partitions/b.var".
309 inline "cic:/CoRN/ftc/Partitions/I.con".
313 inline "cic:/CoRN/ftc/Partitions/Hab.var".
315 inline "cic:/CoRN/ftc/Partitions/n.var".
317 inline "cic:/CoRN/ftc/Partitions/P.var".
319 inline "cic:/CoRN/ftc/Partitions/Mesh_lemma.con".
321 inline "cic:/CoRN/ftc/Partitions/AntiMesh_lemma.con".
323 inline "cic:/CoRN/ftc/Partitions/Mesh_leEq.con".
330 Section Even_Partitions.
333 (*#* More technical stuff. Two equal partitions have the same mesh.
336 inline "cic:/CoRN/ftc/Partitions/Mesh_wd.con".
338 inline "cic:/CoRN/ftc/Partitions/Mesh_wd'.con".
341 The mesh of an even partition is easily calculated.
344 inline "cic:/CoRN/ftc/Partitions/even_partition_Mesh.con".
346 (*#* ** Miscellaneous
347 %\begin{convention}% Throughout this section, let [a,b:IR] and [I] be [[a,b]].
351 inline "cic:/CoRN/ftc/Partitions/a.var".
353 inline "cic:/CoRN/ftc/Partitions/b.var".
357 inline "cic:/CoRN/ftc/Partitions/I.con".
361 inline "cic:/CoRN/ftc/Partitions/Hab.var".
364 An interesting property: in a partition, if [ai [<] aj] then [i < j].
367 inline "cic:/CoRN/ftc/Partitions/Partition_Points_mon.con".
369 inline "cic:/CoRN/ftc/Partitions/refinement_resp_mult.con".
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 inline "cic:/CoRN/ftc/Partitions/m.var".
382 inline "cic:/CoRN/ftc/Partitions/n.var".
384 inline "cic:/CoRN/ftc/Partitions/Hm.var".
386 inline "cic:/CoRN/ftc/Partitions/Hn.var".
390 inline "cic:/CoRN/ftc/Partitions/P.con".
392 inline "cic:/CoRN/ftc/Partitions/Q.con".
396 inline "cic:/CoRN/ftc/Partitions/even_partition_refinement.con".
403 Section More_Definitions.
408 Some auxiliary definitions. A partition is said to be separated if all its points are distinct.
411 inline "cic:/CoRN/ftc/Partitions/a.var".
413 inline "cic:/CoRN/ftc/Partitions/b.var".
415 inline "cic:/CoRN/ftc/Partitions/Hab.var".
417 inline "cic:/CoRN/ftc/Partitions/_Separated.con".
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 inline "cic:/CoRN/ftc/Partitions/n.var".
431 inline "cic:/CoRN/ftc/Partitions/m.var".
433 inline "cic:/CoRN/ftc/Partitions/P.var".
435 inline "cic:/CoRN/ftc/Partitions/Q.var".
437 inline "cic:/CoRN/ftc/Partitions/Separated.con".
440 End More_Definitions.
444 Implicit Arguments _Separated [a b Hab n].
448 Implicit Arguments Separated [a b Hab n m].
452 Section Sep_Partitions.
455 inline "cic:/CoRN/ftc/Partitions/a.var".
457 inline "cic:/CoRN/ftc/Partitions/b.var".
461 inline "cic:/CoRN/ftc/Partitions/I.con".
465 inline "cic:/CoRN/ftc/Partitions/Hab.var".
468 The antimesh of a separated partition is always positive.
471 inline "cic:/CoRN/ftc/Partitions/pos_AntiMesh.con".
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 "cic:/CoRN/ftc/Partitions/partition_length_zero.con".
481 inline "cic:/CoRN/ftc/Partitions/_Separated_imp_length_zero.con".
483 inline "cic:/CoRN/ftc/Partitions/partition_less_imp_gt_zero.con".