(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

(* This file was automatically generated: do not edit *********************)

include "CoRN.ma".

(* $Id: Integral.v,v 1.10 2004/04/23 10:00:59 lcf Exp $ *)

include "ftc/RefLemma.ma".

(*#* printing integral %\ensuremath{\int_I}% #&int;<sub>I</sub># *)

(*#* printing Integral %\ensuremath{\int_I}% #&int;<sub>I</sub># *)

(* begin hide *)

(* UNEXPORTED
Section Lemmas
*)

inline procedural "cic:/CoRN/ftc/Integral/Lemmas/Sumx_wd_weird.con" "Lemmas__" as definition.

inline procedural "cic:/CoRN/ftc/Integral/Sumx_weird_lemma.con" as lemma.

(* UNEXPORTED
End Lemmas
*)

(* end hide *)

(* UNEXPORTED
Section Integral
*)

(*#* *Integral

Having proved the main properties of partitions and refinements, we
will define the integral of a continuous function [F] in the interval
[[a,b]] as the limit of the sequence of Sums of $F$ for even
partitions of increasing number of points.

%\begin{convention}% All throughout, [a,b] will be real numbers, the
interval [[a,b]] will be denoted by [I] and [F,G] will be
continuous functions in [I].
%\end{convention}%
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Integral/a.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Integral/b.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Integral/Hab.var
*)

(* begin hide *)

inline procedural "cic:/CoRN/ftc/Integral/Integral/I.con" "Integral__" as definition.

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Integral/F.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Integral/contF.var
*)

inline procedural "cic:/CoRN/ftc/Integral/Integral/contF'.con" "Integral__" as definition.

(* end hide *)

(* UNEXPORTED
Section Darboux_Sum
*)

inline procedural "cic:/CoRN/ftc/Integral/integral_seq.con" as definition.

inline procedural "cic:/CoRN/ftc/Integral/Cauchy_Darboux_Seq.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/integral.con" as definition.

(* UNEXPORTED
End Darboux_Sum
*)

(* UNEXPORTED
Section Integral_Thm
*)

(*#*
The following shows that in fact the integral of [F] is the limit of
any sequence of partitions of mesh converging to 0.

%\begin{convention}% Let [e] be a positive real number and [P] be a
partition of [I] with [n] points and mesh smaller than the
modulus of continuity of [F] for [e].  Let [fP] be a choice of points
respecting [P].
%\end{convention}%
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Integral/Integral_Thm/n.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Integral/Integral_Thm/P.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Integral/Integral_Thm/e.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Integral/Integral_Thm/He.var
*)

(* begin hide *)

inline procedural "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/d.con" "Integral__Integral_Thm__" as definition.

(* end hide *)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HmeshP.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Integral/Integral_Thm/fP.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP'.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Integral/Integral_Thm/incF.var
*)

inline procedural "cic:/CoRN/ftc/Integral/partition_Sum_conv_integral.con" as lemma.

(* UNEXPORTED
End Integral_Thm
*)

(* UNEXPORTED
End Integral
*)

(* UNEXPORTED
Section Basic_Properties
*)

(*#*
The usual extensionality and strong extensionality results hold.
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/a.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/b.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Hab.var
*)

(* begin hide *)

inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/I.con" "Basic_Properties__" as definition.

(* end hide *)

(* NOTATION
Notation Integral := (integral _ _ Hab).
*)

(* UNEXPORTED
Section Well_Definedness
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/F.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/G.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contF.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contG.var
*)

inline procedural "cic:/CoRN/ftc/Integral/integral_strext.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/integral_strext'.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/integral_wd.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/integral_wd'.con" as lemma.

(* UNEXPORTED
End Well_Definedness
*)

(* UNEXPORTED
Section Linearity_and_Monotonicity
*)

(* UNEXPORTED
Opaque Even_Partition.
*)

(*#*
The integral is a linear and monotonous function; in order to prove these facts we also need the important equalities $\int_a^bdx=b-a$#&int;<sub>a</sub><sup>b</sup>dx=b-a# and $\int_a^af(x)dx=0$#&int;<sub>a</sub><sup>a</sup>=0#.
*)

inline procedural "cic:/CoRN/ftc/Integral/integral_one.con" as lemma.

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/F.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/G.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contF.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contG.var
*)

inline procedural "cic:/CoRN/ftc/Integral/integral_comm_scal.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/integral_plus.con" as lemma.

(* UNEXPORTED
Transparent Even_Partition.
*)

inline procedural "cic:/CoRN/ftc/Integral/integral_empty.con" as lemma.

(* UNEXPORTED
End Linearity_and_Monotonicity
*)

(* UNEXPORTED
Section Linearity_and_Monotonicity'
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/F.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/G.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contF.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contG.var
*)

(*#*
%\begin{convention}% Let [alpha, beta : IR] and assume that
[h := alpha{**}F{+}beta{**}G] is continuous.
%\end{convention}%
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/alpha.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/beta.var
*)

(* begin hide *)

inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/h.con" "Basic_Properties__Linearity_and_Monotonicity'__" as definition.

(* end hide *)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contH.var
*)

inline procedural "cic:/CoRN/ftc/Integral/linear_integral.con" as lemma.

(* UNEXPORTED
Opaque nring.
*)

inline procedural "cic:/CoRN/ftc/Integral/monotonous_integral.con" as lemma.

(* UNEXPORTED
Transparent nring.
*)

(* UNEXPORTED
End Linearity_and_Monotonicity'
*)

(* UNEXPORTED
Section Corollaries
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/F.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/G.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contF.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contG.var
*)

(*#*
As corollaries we can calculate integrals of group operations applied to functions.
*)

inline procedural "cic:/CoRN/ftc/Integral/integral_const.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/integral_minus.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/integral_inv.con" as lemma.

(*#*
We can also bound integrals by bounding the integrated functions.
*)

inline procedural "cic:/CoRN/ftc/Integral/lb_integral.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/ub_integral.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/integral_leEq_norm.con" as lemma.

(* UNEXPORTED
End Corollaries
*)

(* UNEXPORTED
Section Integral_Sum
*)

(*#*
We now relate the sum of integrals in adjoining intervals to the
integral over the union of those intervals.

%\begin{convention}% Let [c] be a real number such that
$c\in[a,b]$#c&isin;[a,b]#.
%\end{convention}%
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/F.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/c.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hab'.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac'.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb'.var
*)

(* UNEXPORTED
Section Partition_Join
*)

(*#*
We first prove that every pair of partitions, one of [[a,c]]
and another of [[c,b]] defines a partition of [[a,b]] the mesh
of which is less or equal to the maximum of the mesh of the original
partitions (actually it is equal, but we don't need the other
inequality).

%\begin{convention}% Let [P,Q] be partitions respectively of
[[a,c]] and [[c,b]] with [n] and [m] points.
%\end{convention}%
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/n.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/m.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/P.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/Q.var
*)

(* begin hide *)

inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux.con" as lemma.

(* end hide *)

inline procedural "cic:/CoRN/ftc/Integral/partition_join_fun.con" as definition.

(* begin hide *)

inline procedural "cic:/CoRN/ftc/Integral/pjf_1.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/pjf_2.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/pjf_2'.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/pjf_3.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf1.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf2.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/partition_join_start.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/partition_join_finish.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/partition_join.con" as definition.

(* end hide *)

(*#*
%\begin{convention}% [fP, fQ] are choices of points respecting [P] and [Q].
%\end{convention}%
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fP.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP'.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fQ.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ'.var
*)

(* begin hide *)

inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux'.con" as lemma.

(* end hide *)

inline procedural "cic:/CoRN/ftc/Integral/partition_join_pts.con" as definition.

(* begin hide *)

inline procedural "cic:/CoRN/ftc/Integral/pjp_1.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/pjp_2.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/pjp_3.con" as lemma.

(* end hide *)

inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_in_partition.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_wd.con" as lemma.

(* UNEXPORTED
Opaque partition_join.
*)

(* UNEXPORTED
Transparent partition_join.
*)

(* UNEXPORTED
Opaque minus.
*)

(* UNEXPORTED
Transparent minus.
*)

(* UNEXPORTED
Opaque minus.
*)

(* UNEXPORTED
Transparent minus.
*)

inline procedural "cic:/CoRN/ftc/Integral/partition_join_Sum_lemma.con" as lemma.

inline procedural "cic:/CoRN/ftc/Integral/partition_join_mesh.con" as lemma.

(* UNEXPORTED
End Partition_Join
*)

(*#*
With these results in mind, the following is a trivial consequence:
*)

(* UNEXPORTED
Opaque Even_Partition.
*)

inline procedural "cic:/CoRN/ftc/Integral/integral_plus_integral.con" as lemma.

(* UNEXPORTED
End Integral_Sum
*)

(* UNEXPORTED
Transparent Even_Partition.
*)

(* UNEXPORTED
End Basic_Properties
*)

(*#*
The following are simple consequences of this result and of previous ones.
*)

inline procedural "cic:/CoRN/ftc/Integral/integral_less_norm.con" as lemma.

(* end hide *)

inline procedural "cic:/CoRN/ftc/Integral/integral_gt_zero.con" as lemma.

(* end hide *)

(*#* remove printing Integral *)