Section Definitions.

Partitions



We now begin to lay the way for the definition of Riemann integral. This will be done through the definition of a sequence of sums that is proved to be convergent; in order to do that, we first need to do a bit of work on partitions.

Definitions



A partition is defined as a record type. For each compact interval [a,b] and each natural number n, a partition of [a,b] with n+1 points is a choice of real numbers a = a0 ≤ a1 ≤ an = b; the following specification works as follows:
  • Pts is the function that chooses the points (it is declared as a coercion);
  • prf1 states that Pts is a setoid function;
  • prf2 states that the points are ordered;
  • start requires that a0 = a and
  • finish requires that an = b.



Record Partition (a b : IR) (Hab : a [<=] b) (lng : N) : Type :=
  {Pts :> forall i, i <= lng -> IR;
   prf1 : forall i j, i = j -> forall Hi Hj, Pts i Hi [=] Pts j Hj;
   prf2 : forall i Hi HSi, Pts i Hi [<=] Pts (S i) HSi;
   start : forall H, Pts 0 H [=] a;
   finish : forall H, Pts lng H [=] b}.

Two immediate consequences of this are that ai ≤ aj whenever i < j and that ai is in [a,b] for all i.

Lemma Partition_mon : forall a b Hab lng (P : Partition a b Hab lng) i j Hi Hj,
 i <= j -> P i Hi [<=] P j Hj.

Lemma Partition_in_compact : forall a b Hab lng (P : Partition a b Hab lng) i Hi,
 compact a b Hab (P i Hi).

Each partition of [a,b] implies a partition of the interval [a,an-1]. This partition will play an important role in much of our future work, so we take some care to define it.

Lemma part_pred_lemma : forall a b Hab lng (P : Partition a b Hab lng) i Hi, a [<=] P i Hi.

Definition Partition_Dom a b Hab n P :
  Partition a _ (part_pred_lemma a b Hab (S n) P n (le_n_Sn n)) n.
Defined.

The mesh of a partition is the greatest distance between two consecutive points. For convenience's sake we also define the dual concept, which is very helpful in some situations. In order to do this, we begin by building a list with all the distances between consecutive points; next we only need to extract the maximum and the minimum of this list. Notice that this list is nonempty except in the case when a = b and n = 0; this means that the convention we took of defining the minimum and maximum of the empty list to be 0 actually helps us in this case.

Definition Part_Mesh_List n a b Hab (P : Partition a b Hab n) : list IR.
Defined.

Definition Mesh a b Hab n P := maxlist (Part_Mesh_List n a b Hab P).

Definition AntiMesh a b Hab n P := minlist (Part_Mesh_List n a b Hab P).

Even partitions (partitions where all the points are evenly spaced) will also play a central role in our work; the first two lemmas are presented simply to make the definition of even partition lighter.

Lemma even_part_1 : forall a b n Hn, a[+]nring 0[*] (b[-]a[/] _[//]nring_ap_zero' IR n Hn) [=] a.

Lemma even_part_2 : forall a b n Hn, a[+]nring n[*] (b[-]a[/] _[//]nring_ap_zero' IR n Hn) [=] b.

Definition Even_Partition a b Hab n (Hn : 0 <> n) : Partition a b Hab n.
Defined.

Section Refinements.

Variables a b : IR.
Hypothesis Hab : a [<=] b.
Variables m n : N.
Variable P : (Partition a b Hab n).
Variable Q : (Partition a b Hab m).

We now define what it means for a partition Q to be a refinement of P and prove the main property of refinements.

Definition Refinement := {f : N -> N |
  f 0 = 0 /\ f n = m /\ (forall i j, i < j -> f i < f j) |
  forall i Hi, {H' : f i <= m | P i Hi [=] Q (f i) H'}}.

Lemma Refinement_prop : Refinement -> forall i (Hi : i <= m) (HSi : (S i) <= m),
 {j : N | {Hj : j <= n | {HSj : S j <= n | P _ Hj [<=] Q _ Hi | Q _ HSi [<=] P _ HSj}}}.

We will also need to consider arbitrary sums of f(xi)(ai+1-ai) where xi∈[ai,ai+1]. For this, we again need a choice function x which has to satisfy some condition. We define the condition and the sum for a fixed P:

Definition Points_in_Partition (g : forall i, i < n -> IR) : CProp :=
  forall i Hi, Compact (prf2 _ _ _ _ P i (lt_le_weak _ _ Hi) Hi) (g i Hi).

Lemma Pts_part_lemma : forall g, Points_in_Partition g -> forall i Hi, compact a b Hab (g i Hi).

Definition ∑P g F (H : Points_in_Partition g) (incF : ⊆ (Compact Hab) (Dom F)) :=
 Sumx (fun i Hi => F (g i Hi) (incF _ (Pts_part_lemma _ H i Hi)) [*]
     (P (S i) Hi[-]P i (lt_le_weak _ _ Hi))).

End Refinements.


Constructions



We now formalize some trivial and helpful constructions.

We will assume a fixed compact interval [a,b], denoted by I.

Variables a b : IR.
Hypothesis Hab : a [<=] b.

Section Getting_Points.

From a partition we always have a canonical choice of points at which to evaluate a function: just take all but the last points of the partition.

Let Q be a partition of I with m points.

Variable m : N.
Variable Q : Partition a b Hab m.

Definition Partition_imp_points : forall i : N, i < m -> IR.
Defined.

Lemma Partition_imp_points_1 : Points_in_Partition Q Partition_imp_points.

Lemma Partition_imp_points_2 : nat_less_n_fun Partition_imp_points.

End Getting_Points.

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].

Variable F : PartIR.
Hypothesis contF : Continuous_I Hab F.

Definition Even_Partition_Sum (n : N) (Hn : 0 <> n) : IR.
Defined.

End Definitions.



Section Lemmas.

Properties of the mesh



If a partition has more than one point then its mesh list is nonempty.

Lemma length_Part_Mesh_List : forall n (a b : IR) (Hab : a [<=] b) (P : Partition Hab n),
 0 < n -> 0 < length (Part_Mesh_List P).

Any element of the auxiliary list defined to calculate the mesh of a partition has a very specific form.

Lemma Part_Mesh_List_lemma : forall n (a b : IR) (Hab : a [<=] b) (P : Partition Hab n) x,
 member x (Part_Mesh_List P) ->
 {i : N | {Hi : i <= n | {Hi' : S i <= n | x [=] P _ Hi'[-]P _ Hi}}}.

Mesh and antimesh are always nonnegative.

Lemma Mesh_nonneg : forall n (a b : IR) (Hab : a [<=] b) (P : Partition Hab n), 0 [<=] Mesh P.

Lemma AntiMesh_nonneg : forall n (a b : IR) (Hab : a [<=] b) (P : Partition Hab n),
 0 [<=] AntiMesh P.

Most important, AntiMesh and Mesh provide lower and upper bounds for the distance between any two consecutive points in a partition.

Let I be [a,b] and P be a partition of I with n points.

Variables a b : IR.
Hypothesis Hab : a [<=] b.

Variable n : N.
Variable P : Partition Hab n.

Lemma Mesh_lemma : forall i H H', P (S i) H'[-]P i H [<=] Mesh P.

Lemma AntiMesh_lemma : forall i H H', AntiMesh P [<=] P (S i) H'[-]P i H.


Lemma Mesh_leEq : forall m (Q : Partition Hab m), Refinement P Q -> Mesh Q [<=] Mesh P.


End Lemmas.

Section Even_Partitions.

More technical stuff. Two equal partitions have the same mesh.

Lemma Mesh_wd : forall n a b b' (Hab : a [<=] b) (Hab' : a [<=] b')
 (P : Partition Hab n) (Q : Partition Hab' n),
 (forall i Hi, P i Hi [=] Q i Hi) -> Mesh P [=] Mesh Q.

Lemma Mesh_wd' : forall n a b (Hab : a [<=] b) (P Q : Partition Hab n),
 (forall i Hi, P i Hi [=] Q i Hi) -> Mesh P [=] Mesh Q.

The mesh of an even partition is easily calculated.

Lemma even_partition_Mesh : forall m Hm a b (Hab : a [<=] b),
 Mesh (Even_Partition Hab m Hm) [=] (b[-]a[/] _[//]nring_ap_zero' _ _ Hm).

Miscellaneous

Throughout this section, let a,b:IR and I be [a,b].

Variables a b : IR.
Hypothesis Hab : a [<=] b.

An interesting property: in a partition, if ai < aj then i < j.

Lemma Partition_Points_mon : forall n (P : Partition Hab n) i j Hi Hj,
 P i Hi [<] P j Hj -> i < j.

Lemma refinement_resp_mult : forall m n Hm Hn, {k : N | m = n * k} ->
 Refinement (Even_Partition Hab n Hn) (Even_Partition Hab m Hm).

Assume m,n are positive natural numbers and denote by P and Q the even partitions with, respectively, m and n points.

Even partitions always have a common refinement.

Variables m n : N.
Hypothesis Hm : 0 <> m.
Hypothesis Hn : 0 <> n.


Lemma even_partition_refinement : {N : N | {HN : 0 <> N |
 Refinement P (Even_Partition Hab N HN) |
 Refinement Q (Even_Partition Hab N HN)}}.

End Even_Partitions.

Section More_Definitions.

Separation



Some auxiliary definitions. A partition is said to be separated if all its points are distinct.

Variables a b : IR.
Hypothesis Hab : a [<=] b.

Definition _Separated n (P : Partition Hab n) := forall i Hi H', P i Hi [<] P (S i) H'.

Two partitions are said to be (mutually) separated if they are both separated and all their points are distinct (except for the endpoints).

Let P,Q be partitions of I with, respectively, n and m points.

Variables n m : N.

Variable P : Partition Hab n.
Variable Q : Partition Hab m.

Definition Separated := _Separated _ P and _Separated _ Q and
 (forall i j, 0 < i -> 0 < j -> i < n -> j < m -> forall Hi Hj, P i Hi [#] Q j Hj).

End More_Definitions.


Section Sep_Partitions.

Variables a b : IR.
Hypothesis Hab : a [<=] b.

The antimesh of a separated partition is always positive.

Lemma pos_AntiMesh : forall n (P : Partition Hab n),
 0 < n -> _Separated P -> 0 [<] AntiMesh P.

A partition can have only one point iff the endpoints of the interval are the same; moreover, if the partition is separated and the endpoints of the interval are the same then it must have one point.

Lemma partition_length_zero : Partition Hab 0 -> a [=] b.

Lemma _Separated_imp_length_zero : forall n (P : Partition Hab n),
 _Separated P -> a [=] b -> 0 = n.

Lemma partition_less_imp_gt_zero : forall n (P : Partition Hab n), a [<] b -> 0 < n.

End Sep_Partitions.