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 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 "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 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 "cic:/CoRN/ftc/Partitions/Definitions/I.con" "Definitions__".
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 "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 alias id "F" = "cic:/CoRN/ftc/Partitions/Definitions/F.var".
213 alias id "contF" = "cic:/CoRN/ftc/Partitions/Definitions/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 alias id "a" = "cic:/CoRN/ftc/Partitions/Lemmas/a.var".
305 alias id "b" = "cic:/CoRN/ftc/Partitions/Lemmas/b.var".
309 inline "cic:/CoRN/ftc/Partitions/Lemmas/I.con" "Lemmas__".
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 "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 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 "cic:/CoRN/ftc/Partitions/Even_Partitions/I.con" "Even_Partitions__".
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 "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 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 "cic:/CoRN/ftc/Partitions/Even_Partitions/P.con" "Even_Partitions__".
392 inline "cic:/CoRN/ftc/Partitions/Even_Partitions/Q.con" "Even_Partitions__".
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 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 "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 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 "cic:/CoRN/ftc/Partitions/Separated.con".
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 "cic:/CoRN/ftc/Partitions/Sep_Partitions/I.con" "Sep_Partitions__".
465 alias id "Hab" = "cic:/CoRN/ftc/Partitions/Sep_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".