X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FMoreIntegrals.ma;h=88fff5d7a1ef943e1366aa3aa5131a7f91f9bf5a;hb=effab341df3fb2bfe403e51d360e81c8b0455e1a;hp=062018bf97caea93fe06710fd26f4854b9b4affb;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma index 062018bf9..88fff5d7a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma @@ -16,18 +16,16 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreIntegrals". +include "CoRN.ma". + (* $Id: MoreIntegrals.v,v 1.6 2004/04/23 10:00:59 lcf Exp $ *) -(* INCLUDE -Integral -*) +include "ftc/Integral.ma". -(* INCLUDE -MoreFunctions -*) +include "ftc/MoreFunctions.ma". (* UNEXPORTED -Section Lemmas. +Section Lemmas *) (*#* printing Integral %\ensuremath{\int}% #∫# *) @@ -50,22 +48,22 @@ partial functions continuous in [[Min(a,b),Max(a,b)]]. Before we define the new integral we need to some trivial interval inclusions. *) -inline cic:/CoRN/ftc/MoreIntegrals/a.var. +alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Lemmas/a.var". -inline cic:/CoRN/ftc/MoreIntegrals/b.var. +alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Lemmas/b.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Lemmas/Hab.var". -inline cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_lft.con. +inline "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_lft.con". -inline cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_rht.con. +inline "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_rht.con". (* UNEXPORTED -End Lemmas. +End Lemmas *) (* UNEXPORTED -Section Definitions. +Section Definitions *) (*#* @@ -76,26 +74,26 @@ classical definition, and it collapses to the old one in the case [a [<=] b]. *) -inline cic:/CoRN/ftc/MoreIntegrals/a.var. +alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/a.var". -inline cic:/CoRN/ftc/MoreIntegrals/b.var. +alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/b.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/Hab.var". -inline cic:/CoRN/ftc/MoreIntegrals/F.var. +alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/F.var". -inline cic:/CoRN/ftc/MoreIntegrals/HF.var. +alias id "HF" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/HF.var". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_inc1.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_inc1.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_inc2.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_inc2.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_integral.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_integral.con". (* UNEXPORTED -End Definitions. +End Definitions *) (* UNEXPORTED @@ -103,7 +101,7 @@ Implicit Arguments Integral [a b Hab F]. *) (* UNEXPORTED -Section Properties_of_Integral. +Section Properties_of_Integral *) (*#* **Properties of the Integral @@ -112,71 +110,71 @@ All our old properties carry over to this new definition---and some new ones, too. We begin with (strong) extensionality. *) -inline cic:/CoRN/ftc/MoreIntegrals/a.var. +alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/a.var". -inline cic:/CoRN/ftc/MoreIntegrals/b.var. +alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/b.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/Hab.var". -inline cic:/CoRN/ftc/MoreIntegrals/F.var. +alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/F.var". -inline cic:/CoRN/ftc/MoreIntegrals/G.var. +alias id "G" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/G.var". -inline cic:/CoRN/ftc/MoreIntegrals/contF.var. +alias id "contF" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/contF.var". -inline cic:/CoRN/ftc/MoreIntegrals/contG.var. +alias id "contG" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/contG.var". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_strext.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_strext.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_strext'.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_strext'.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_wd.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_wd.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_wd'.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_wd'.con". (*#* The integral is a linear operator. *) -inline cic:/CoRN/ftc/MoreIntegrals/Integral_const.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_const.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_comm_scal.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_comm_scal.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_plus.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_plus.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_inv.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_inv.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_minus.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_minus.con". -inline cic:/CoRN/ftc/MoreIntegrals/linear_Integral.con. +inline "cic:/CoRN/ftc/MoreIntegrals/linear_Integral.con". (*#* If the endpoints are equal then the integral vanishes. *) -inline cic:/CoRN/ftc/MoreIntegrals/Integral_empty.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_empty.con". (*#* And the norm provides an upper bound for the absolute value of the integral. *) -inline cic:/CoRN/ftc/MoreIntegrals/Integral_leEq_norm.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_leEq_norm.con". (* UNEXPORTED -End Properties_of_Integral. +End Properties_of_Integral *) (* UNEXPORTED -Section More_Properties. +Section More_Properties *) (*#* Two other ways of stating the addition law for domains. *) -inline cic:/CoRN/ftc/MoreIntegrals/integral_plus_Integral.con. +inline "cic:/CoRN/ftc/MoreIntegrals/integral_plus_Integral.con". -inline cic:/CoRN/ftc/MoreIntegrals/integral_plus_integral'.con. +inline "cic:/CoRN/ftc/MoreIntegrals/integral_plus_integral'.con". (*#* And now we can prove the addition law for domains with our general operator. @@ -185,81 +183,81 @@ And now we can prove the addition law for domains with our general operator. %\end{convention}% *) -inline cic:/CoRN/ftc/MoreIntegrals/a.var. +alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/a.var". -inline cic:/CoRN/ftc/MoreIntegrals/b.var. +alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/b.var". -inline cic:/CoRN/ftc/MoreIntegrals/c.var. +alias id "c" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/c.var". (* begin show *) -inline cic:/CoRN/ftc/MoreIntegrals/Hab'.var. +alias id "Hab'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hab'.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hac'.var. +alias id "Hac'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hac'.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hcb'.var. +alias id "Hcb'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hcb'.var". -inline cic:/CoRN/ftc/MoreIntegrals/Habc'.var. +alias id "Habc'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc'.var". (* end show *) -inline cic:/CoRN/ftc/MoreIntegrals/F.var. +alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/F.var". (* begin show *) -inline cic:/CoRN/ftc/MoreIntegrals/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hab.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hac.var. +alias id "Hac" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hac.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hcb.var. +alias id "Hcb" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hcb.var". -inline cic:/CoRN/ftc/MoreIntegrals/Habc.var. +alias id "Habc" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc.var". (* end show *) (* begin hide *) -inline cic:/CoRN/ftc/MoreIntegrals/le_abc_ab.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_ab.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/le_abc_ac.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_ac.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/le_abc_cb.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_cb.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/le_abc_a.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_a.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/le_abc_b.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_b.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/le_abc_c.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_c.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/le_ab_a.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ab_a.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/le_cb_c.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_cb_c.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/le_ac_a.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ac_a.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/le_ab_b.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ab_b.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/le_cb_b.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_cb_b.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/le_ac_c.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ac_c.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/Habc_abc.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_abc.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/Habc_ab.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_ab.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/Habc_ac.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_ac.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/Habc_cb.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_cb.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/Habc_a.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_a.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/Habc_b.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_b.con" "More_Properties__". -inline cic:/CoRN/ftc/MoreIntegrals/Habc_c.con. +inline "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_c.con" "More_Properties__". (* end hide *) -inline cic:/CoRN/ftc/MoreIntegrals/Integral_plus_Integral.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_plus_Integral.con". (*#* Notice that, unlike in the classical case, an extra hypothesis (the @@ -267,38 +265,38 @@ continuity of [F] in the interval [[Min(a,b,c),Max(a,b,c)]]) must be assumed. *) (* UNEXPORTED -End More_Properties. +End More_Properties *) (* UNEXPORTED -Section Corollaries. +Section Corollaries *) -inline cic:/CoRN/ftc/MoreIntegrals/a.var. +alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/a.var". -inline cic:/CoRN/ftc/MoreIntegrals/b.var. +alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/b.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/Hab.var". -inline cic:/CoRN/ftc/MoreIntegrals/F.var. +alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/F.var". -inline cic:/CoRN/ftc/MoreIntegrals/contF.var. +alias id "contF" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/contF.var". (*#* As a corollary, we get the following rule: *) -inline cic:/CoRN/ftc/MoreIntegrals/Integral_op.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_op.con". (*#* Finally, some miscellaneous results: *) -inline cic:/CoRN/ftc/MoreIntegrals/Integral_less_norm.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_less_norm.con". -inline cic:/CoRN/ftc/MoreIntegrals/ub_Integral.con. +inline "cic:/CoRN/ftc/MoreIntegrals/ub_Integral.con". (* UNEXPORTED -End Corollaries. +End Corollaries *) -inline cic:/CoRN/ftc/MoreIntegrals/Integral_ap_zero.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_ap_zero.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_eq_zero.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_eq_zero.con".