X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftransc%2FTaylorSeries.ma;h=7e00f92c8cfdca1801b8a8f725ecc873cd56a9bc;hb=b637879a2b3f2ceda65afb3c950061189c4730b7;hp=d29decd124fec51c57f6fa980c30debdc250fb41;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma b/helm/software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma index d29decd12..7e00f92c8 100644 --- a/helm/software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma +++ b/helm/software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma @@ -16,15 +16,13 @@ set "baseuri" "cic:/matita/CoRN-Decl/transc/TaylorSeries". +include "CoRN.ma". + (* $Id: TaylorSeries.v,v 1.7 2004/04/23 10:01:08 lcf Exp $ *) -(* INCLUDE -PowerSeries -*) +include "transc/PowerSeries.ma". -(* INCLUDE -Taylor -*) +include "ftc/Taylor.ma". (*#* *Taylor Series @@ -42,22 +40,22 @@ point of [J]. *) (* UNEXPORTED -Section Definitions. +Section Definitions *) -inline cic:/CoRN/transc/TaylorSeries/J.var. +alias id "J" = "cic:/CoRN/transc/TaylorSeries/Definitions/J.var". -inline cic:/CoRN/transc/TaylorSeries/pJ.var. +alias id "pJ" = "cic:/CoRN/transc/TaylorSeries/Definitions/pJ.var". -inline cic:/CoRN/transc/TaylorSeries/F.var. +alias id "F" = "cic:/CoRN/transc/TaylorSeries/Definitions/F.var". -inline cic:/CoRN/transc/TaylorSeries/diffF.var. +alias id "diffF" = "cic:/CoRN/transc/TaylorSeries/Definitions/diffF.var". -inline cic:/CoRN/transc/TaylorSeries/a.var. +alias id "a" = "cic:/CoRN/transc/TaylorSeries/Definitions/a.var". -inline cic:/CoRN/transc/TaylorSeries/Ha.var. +alias id "Ha" = "cic:/CoRN/transc/TaylorSeries/Definitions/Ha.var". -inline cic:/CoRN/transc/TaylorSeries/Taylor_Series'.con. +inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series'.con". (*#* %\begin{convention}% Assume also that [f] is the sequence of @@ -65,11 +63,11 @@ derivatives of [F]. %\end{convention}% *) -inline cic:/CoRN/transc/TaylorSeries/f.var. +alias id "f" = "cic:/CoRN/transc/TaylorSeries/Definitions/f.var". -inline cic:/CoRN/transc/TaylorSeries/derF.var. +alias id "derF" = "cic:/CoRN/transc/TaylorSeries/Definitions/derF.var". -inline cic:/CoRN/transc/TaylorSeries/Taylor_Series.con. +inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series.con". (* UNEXPORTED Opaque N_Deriv. @@ -77,16 +75,16 @@ Opaque N_Deriv. (*#* Characterizations of the Taylor remainder. *) -inline cic:/CoRN/transc/TaylorSeries/Taylor_Rem_char.con. +inline "cic:/CoRN/transc/TaylorSeries/Taylor_Rem_char.con". -inline cic:/CoRN/transc/TaylorSeries/abs_Taylor_Rem_char.con. +inline "cic:/CoRN/transc/TaylorSeries/abs_Taylor_Rem_char.con". (* UNEXPORTED -End Definitions. +End Definitions *) (* UNEXPORTED -Section Convergence_in_IR. +Section Convergence_in_IR *) (*#* **Convergence @@ -97,27 +95,27 @@ derivatives of [F] that guarantees convergence of its Taylor series to [F]. *) -inline cic:/CoRN/transc/TaylorSeries/H.var. +alias id "H" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/H.var". -inline cic:/CoRN/transc/TaylorSeries/F.var. +alias id "F" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/F.var". -inline cic:/CoRN/transc/TaylorSeries/a.var. +alias id "a" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/a.var". -inline cic:/CoRN/transc/TaylorSeries/Ha.var. +alias id "Ha" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/Ha.var". -inline cic:/CoRN/transc/TaylorSeries/f.var. +alias id "f" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/f.var". -inline cic:/CoRN/transc/TaylorSeries/derF.var. +alias id "derF" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/derF.var". -inline cic:/CoRN/transc/TaylorSeries/Taylor_Series_imp_cont.con. +inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_imp_cont.con". -inline cic:/CoRN/transc/TaylorSeries/Taylor_Series_lemma_cont.con. +inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_lemma_cont.con". -inline cic:/CoRN/transc/TaylorSeries/Taylor_bnd.con. +inline "cic:/CoRN/transc/TaylorSeries/Taylor_bnd.con". (* begin show *) -inline cic:/CoRN/transc/TaylorSeries/bndf.var. +alias id "bndf" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/bndf.var". (* end show *) @@ -127,15 +125,15 @@ Opaque nexp_op fac. (* begin hide *) -inline cic:/CoRN/transc/TaylorSeries/H1.con. +inline "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/H1.con" "Convergence_in_IR__". (* UNEXPORTED Transparent nexp_op. *) -inline cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma1.con. +inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma1.con". -inline cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma2.con. +inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma2.con". (* end hide *) @@ -149,7 +147,7 @@ Transparent nexp_op. Opaque nexp_op. *) -inline cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_IR.con. +inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_IR.con". (* begin hide *) @@ -157,13 +155,13 @@ inline cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_IR.con. Transparent nexp_op. *) -inline cic:/CoRN/transc/TaylorSeries/Taylor_majoration_lemma.con. +inline "cic:/CoRN/transc/TaylorSeries/Taylor_majoration_lemma.con". (* UNEXPORTED Opaque N_Deriv fac. *) -inline cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma3.con. +inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_lemma3.con". (* end hide *) @@ -175,7 +173,7 @@ will separately assume convergence. (* begin show *) -inline cic:/CoRN/transc/TaylorSeries/Hf.var. +alias id "Hf" = "cic:/CoRN/transc/TaylorSeries/Convergence_in_IR/Hf.var". (* end show *) @@ -187,14 +185,14 @@ Transparent fac. Opaque mult. *) -inline cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_to_fun.con. +inline "cic:/CoRN/transc/TaylorSeries/Taylor_Series_conv_to_fun.con". (* UNEXPORTED -End Convergence_in_IR. +End Convergence_in_IR *) (* UNEXPORTED -Section Other_Results. +Section Other_Results *) (*#* @@ -202,7 +200,7 @@ The condition for the previous lemma is not very easy to prove. We give some helpful lemmas. *) -inline cic:/CoRN/transc/TaylorSeries/Taylor_bnd_trans.con. +inline "cic:/CoRN/transc/TaylorSeries/Taylor_bnd_trans.con". (* begin hide *) @@ -210,11 +208,11 @@ inline cic:/CoRN/transc/TaylorSeries/Taylor_bnd_trans.con. Opaque nexp_op. *) -inline cic:/CoRN/transc/TaylorSeries/convergence_lemma.con. +inline "cic:/CoRN/transc/TaylorSeries/convergence_lemma.con". (* end hide *) -inline cic:/CoRN/transc/TaylorSeries/bnd_imp_Taylor_bnd.con. +inline "cic:/CoRN/transc/TaylorSeries/bnd_imp_Taylor_bnd.con". (*#* Finally, a uniqueness criterium: two functions [F] and [G] are equal, @@ -222,39 +220,39 @@ provided that their derivatives coincide at a given point and their Taylor series converge to themselves. *) -inline cic:/CoRN/transc/TaylorSeries/F.var. +alias id "F" = "cic:/CoRN/transc/TaylorSeries/Other_Results/F.var". -inline cic:/CoRN/transc/TaylorSeries/G.var. +alias id "G" = "cic:/CoRN/transc/TaylorSeries/Other_Results/G.var". -inline cic:/CoRN/transc/TaylorSeries/a.var. +alias id "a" = "cic:/CoRN/transc/TaylorSeries/Other_Results/a.var". -inline cic:/CoRN/transc/TaylorSeries/f.var. +alias id "f" = "cic:/CoRN/transc/TaylorSeries/Other_Results/f.var". -inline cic:/CoRN/transc/TaylorSeries/g.var. +alias id "g" = "cic:/CoRN/transc/TaylorSeries/Other_Results/g.var". -inline cic:/CoRN/transc/TaylorSeries/derF.var. +alias id "derF" = "cic:/CoRN/transc/TaylorSeries/Other_Results/derF.var". -inline cic:/CoRN/transc/TaylorSeries/derG.var. +alias id "derG" = "cic:/CoRN/transc/TaylorSeries/Other_Results/derG.var". -inline cic:/CoRN/transc/TaylorSeries/bndf.var. +alias id "bndf" = "cic:/CoRN/transc/TaylorSeries/Other_Results/bndf.var". -inline cic:/CoRN/transc/TaylorSeries/bndg.var. +alias id "bndg" = "cic:/CoRN/transc/TaylorSeries/Other_Results/bndg.var". (* begin show *) -inline cic:/CoRN/transc/TaylorSeries/Heq.var. +alias id "Heq" = "cic:/CoRN/transc/TaylorSeries/Other_Results/Heq.var". (* end show *) (* begin hide *) -inline cic:/CoRN/transc/TaylorSeries/Hf.con. +inline "cic:/CoRN/transc/TaylorSeries/Other_Results/Hf.con" "Other_Results__". (* end hide *) -inline cic:/CoRN/transc/TaylorSeries/Taylor_unique_crit.con. +inline "cic:/CoRN/transc/TaylorSeries/Taylor_unique_crit.con". (* UNEXPORTED -End Other_Results. +End Other_Results *)