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".
19 (* $Id: Partitions.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *)
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 (*#* Two immediate consequences of this are that [ai [<=] aj] whenever
56 [i < j] and that [ai] is in [[a,b]] for all [i].
59 inline cic:/CoRN/ftc/Partitions/Partition_mon.con.
61 inline cic:/CoRN/ftc/Partitions/Partition_in_compact.con.
64 Each partition of [[a,b]] implies a partition of the interval
65 $[a,a_{n-1}]$#[a,a<sub>n-1</sub>]#. This partition will play an
66 important role in much of our future work, so we take some care to
70 inline cic:/CoRN/ftc/Partitions/part_pred_lemma.con.
72 inline cic:/CoRN/ftc/Partitions/Partition_Dom.con.
75 The mesh of a partition is the greatest distance between two
76 consecutive points. For convenience's sake we also define the dual
77 concept, which is very helpful in some situations. In order to do
78 this, we begin by building a list with all the distances between
79 consecutive points; next we only need to extract the maximum and the
80 minimum of this list. Notice that this list is nonempty except in the
81 case when [a [=] b] and [n = 0]; this means that the convention we took
82 of defining the minimum and maximum of the empty list to be [0] actually
83 helps us in this case.
86 inline cic:/CoRN/ftc/Partitions/Part_Mesh_List.con.
88 inline cic:/CoRN/ftc/Partitions/Mesh.con.
90 inline cic:/CoRN/ftc/Partitions/AntiMesh.con.
93 Even partitions (partitions where all the points are evenly spaced)
94 will also play a central role in our work; the first two lemmas are
95 presented simply to make the definition of even partition lighter.
98 inline cic:/CoRN/ftc/Partitions/even_part_1.con.
100 inline cic:/CoRN/ftc/Partitions/even_part_2.con.
102 inline cic:/CoRN/ftc/Partitions/Even_Partition.con.
108 inline cic:/CoRN/ftc/Partitions/a.var.
110 inline cic:/CoRN/ftc/Partitions/b.var.
112 inline cic:/CoRN/ftc/Partitions/Hab.var.
114 inline cic:/CoRN/ftc/Partitions/m.var.
116 inline cic:/CoRN/ftc/Partitions/n.var.
118 inline cic:/CoRN/ftc/Partitions/P.var.
120 inline cic:/CoRN/ftc/Partitions/Q.var.
123 We now define what it means for a partition [Q] to be a refinement of
124 [P] and prove the main property of refinements.
127 inline cic:/CoRN/ftc/Partitions/Refinement.con.
129 inline cic:/CoRN/ftc/Partitions/Refinement_prop.con.
132 We will also need to consider arbitrary sums %of the form
133 \[\sum_{i=0}^{n-1}f(x_i)(a_{i+1}-a_i)\]%#of
134 f(x<sub>i</sub>)(a<sub>i+1</sub>-a<sub>i</sub>)# where
135 $x_i\in[a_i,a_{i+1}]$#x<sub>i</sub>∈[a<sub>i</sub>,a<sub>i+1</sub>]#.
136 For this, we again need a choice function [x] which has to satisfy
137 some condition. We define the condition and the sum for a fixed [P]:
140 inline cic:/CoRN/ftc/Partitions/Points_in_Partition.con.
142 inline cic:/CoRN/ftc/Partitions/Pts_part_lemma.con.
144 inline cic:/CoRN/ftc/Partitions/Partition_Sum.con.
151 Implicit Arguments Points_in_Partition [a b Hab n].
155 Implicit Arguments Partition_Sum [a b Hab n P g F].
160 We now formalize some trivial and helpful constructions.
162 %\begin{convention}% We will assume a fixed compact interval [[a,b]], denoted by [I].
166 inline cic:/CoRN/ftc/Partitions/a.var.
168 inline cic:/CoRN/ftc/Partitions/b.var.
170 inline cic:/CoRN/ftc/Partitions/Hab.var.
174 inline cic:/CoRN/ftc/Partitions/I.con.
179 Section Getting_Points.
183 From a partition we always have a canonical choice of points at which
184 to evaluate a function: just take all but the last points of the
187 %\begin{convention}% Let [Q] be a partition of [I] with [m] points.
191 inline cic:/CoRN/ftc/Partitions/m.var.
193 inline cic:/CoRN/ftc/Partitions/Q.var.
195 inline cic:/CoRN/ftc/Partitions/Partition_imp_points.con.
197 inline cic:/CoRN/ftc/Partitions/Partition_imp_points_1.con.
199 inline cic:/CoRN/ftc/Partitions/Partition_imp_points_2.con.
206 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]].
209 inline cic:/CoRN/ftc/Partitions/F.var.
211 inline cic:/CoRN/ftc/Partitions/contF.var.
213 inline cic:/CoRN/ftc/Partitions/Even_Partition_Sum.con.
220 Implicit Arguments Partition [a b].
224 Implicit Arguments Partition_Dom [a b Hab n].
228 Implicit Arguments Mesh [a b Hab n].
232 Implicit Arguments AntiMesh [a b Hab n].
236 Implicit Arguments Pts [a b Hab lng].
240 Implicit Arguments Part_Mesh_List [n a b Hab].
244 Implicit Arguments Points_in_Partition [a b Hab n].
248 Implicit Arguments Partition_Sum [a b Hab n P g F].
252 Implicit Arguments Even_Partition [a b].
256 Implicit Arguments Even_Partition_Sum [a b].
260 Implicit Arguments Refinement [a b Hab n m].
264 Hint Resolve start finish: algebra.
271 (*#* ** Properties of the mesh
273 If a partition has more than one point then its mesh list is nonempty.
276 inline cic:/CoRN/ftc/Partitions/length_Part_Mesh_List.con.
279 Any element of the auxiliary list defined to calculate the mesh of a partition has a very specific form.
282 inline cic:/CoRN/ftc/Partitions/Part_Mesh_List_lemma.con.
285 Mesh and antimesh are always nonnegative.
288 inline cic:/CoRN/ftc/Partitions/Mesh_nonneg.con.
290 inline cic:/CoRN/ftc/Partitions/AntiMesh_nonneg.con.
293 Most important, [AntiMesh] and [Mesh] provide lower and upper bounds
294 for the distance between any two consecutive points in a partition.
296 %\begin{convention}% Let [I] be [[a,b]] and [P] be a partition of [I]
301 inline cic:/CoRN/ftc/Partitions/a.var.
303 inline cic:/CoRN/ftc/Partitions/b.var.
307 inline cic:/CoRN/ftc/Partitions/I.con.
311 inline cic:/CoRN/ftc/Partitions/Hab.var.
313 inline cic:/CoRN/ftc/Partitions/n.var.
315 inline cic:/CoRN/ftc/Partitions/P.var.
317 inline cic:/CoRN/ftc/Partitions/Mesh_lemma.con.
319 inline cic:/CoRN/ftc/Partitions/AntiMesh_lemma.con.
321 inline cic:/CoRN/ftc/Partitions/Mesh_leEq.con.
328 Section Even_Partitions.
331 (*#* More technical stuff. Two equal partitions have the same mesh.
334 inline cic:/CoRN/ftc/Partitions/Mesh_wd.con.
336 inline cic:/CoRN/ftc/Partitions/Mesh_wd'.con.
339 The mesh of an even partition is easily calculated.
342 inline cic:/CoRN/ftc/Partitions/even_partition_Mesh.con.
344 (*#* ** Miscellaneous
345 %\begin{convention}% Throughout this section, let [a,b:IR] and [I] be [[a,b]].
349 inline cic:/CoRN/ftc/Partitions/a.var.
351 inline cic:/CoRN/ftc/Partitions/b.var.
355 inline cic:/CoRN/ftc/Partitions/I.con.
359 inline cic:/CoRN/ftc/Partitions/Hab.var.
362 An interesting property: in a partition, if [ai [<] aj] then [i < j].
365 inline cic:/CoRN/ftc/Partitions/Partition_Points_mon.con.
367 inline cic:/CoRN/ftc/Partitions/refinement_resp_mult.con.
370 %\begin{convention}% Assume [m,n] are positive natural numbers and
371 denote by [P] and [Q] the even partitions with, respectively, [m] and
375 Even partitions always have a common refinement.
378 inline cic:/CoRN/ftc/Partitions/m.var.
380 inline cic:/CoRN/ftc/Partitions/n.var.
382 inline cic:/CoRN/ftc/Partitions/Hm.var.
384 inline cic:/CoRN/ftc/Partitions/Hn.var.
388 inline cic:/CoRN/ftc/Partitions/P.con.
390 inline cic:/CoRN/ftc/Partitions/Q.con.
394 inline cic:/CoRN/ftc/Partitions/even_partition_refinement.con.
401 Section More_Definitions.
406 Some auxiliary definitions. A partition is said to be separated if all its points are distinct.
409 inline cic:/CoRN/ftc/Partitions/a.var.
411 inline cic:/CoRN/ftc/Partitions/b.var.
413 inline cic:/CoRN/ftc/Partitions/Hab.var.
415 inline cic:/CoRN/ftc/Partitions/_Separated.con.
418 Two partitions are said to be (mutually) separated if they are both
419 separated and all their points are distinct (except for the
422 %\begin{convention}% Let [P,Q] be partitions of [I] with,
423 respectively, [n] and [m] points.
427 inline cic:/CoRN/ftc/Partitions/n.var.
429 inline cic:/CoRN/ftc/Partitions/m.var.
431 inline cic:/CoRN/ftc/Partitions/P.var.
433 inline cic:/CoRN/ftc/Partitions/Q.var.
435 inline cic:/CoRN/ftc/Partitions/Separated.con.
438 End More_Definitions.
442 Implicit Arguments _Separated [a b Hab n].
446 Implicit Arguments Separated [a b Hab n m].
450 Section Sep_Partitions.
453 inline cic:/CoRN/ftc/Partitions/a.var.
455 inline cic:/CoRN/ftc/Partitions/b.var.
459 inline cic:/CoRN/ftc/Partitions/I.con.
463 inline cic:/CoRN/ftc/Partitions/Hab.var.
466 The antimesh of a separated partition is always positive.
469 inline cic:/CoRN/ftc/Partitions/pos_AntiMesh.con.
472 A partition can have only one point iff the endpoints of the interval
473 are the same; moreover, if the partition is separated and the
474 endpoints of the interval are the same then it must have one point.
477 inline cic:/CoRN/ftc/Partitions/partition_length_zero.con.
479 inline cic:/CoRN/ftc/Partitions/_Separated_imp_length_zero.con.
481 inline cic:/CoRN/ftc/Partitions/partition_less_imp_gt_zero.con.