(**************************************************************************)
(* ___ *)
(* ||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}% #∫I# *)
(*#* printing Integral %\ensuremath{\int_I}% #∫I# *)
(* 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$#∫abdx=b-a# and $\int_a^af(x)dx=0$#∫aa=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∈[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 *)