X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fcontribs%2Fprocedural%2FCoRN%2Ftransc%2FPowerSeries.mma;fp=matitaB%2Fmatita%2Fcontribs%2Fprocedural%2FCoRN%2Ftransc%2FPowerSeries.mma;h=b91f4a5f3d7cde37688ae32fe40d463b642fa6c7;hb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;hp=0000000000000000000000000000000000000000;hpb=f04a064bb34aabaf91dc0c48e3b08b37ecd7b0a2;p=helm.git diff --git a/matitaB/matita/contribs/procedural/CoRN/transc/PowerSeries.mma b/matitaB/matita/contribs/procedural/CoRN/transc/PowerSeries.mma new file mode 100644 index 000000000..b91f4a5f3 --- /dev/null +++ b/matitaB/matita/contribs/procedural/CoRN/transc/PowerSeries.mma @@ -0,0 +1,262 @@ +(**************************************************************************) +(* ___ *) +(* ||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: PowerSeries.v,v 1.8 2004/04/23 10:01:08 lcf Exp $ *) + +(*#* printing Exp %\ensuremath{\exp}% *) + +(*#* printing Sin %\ensuremath{\sin}% *) + +(*#* printing Cos %\ensuremath{\cos}% *) + +(*#* printing Log %\ensuremath{\log}% *) + +(*#* printing Tan %\ensuremath{\tan}% *) + +include "ftc/FTC.ma". + +(*#* *More on Power Series + +We will now formally define an operator that defines a function as the +sum of some series given a number sequence. Along with it, we will +prove some important properties of these entities. +*) + +(* UNEXPORTED +Section Power_Series +*) + +(*#* **General results + +%\begin{convention}% Let [J : interval] and [x0 : IR] be a point of [J]. +Let [a : nat -> IR]. +%\end{convention}% +*) + +(* UNEXPORTED +cic:/CoRN/transc/PowerSeries/Power_Series/J.var +*) + +(* UNEXPORTED +cic:/CoRN/transc/PowerSeries/Power_Series/x0.var +*) + +(* UNEXPORTED +cic:/CoRN/transc/PowerSeries/Power_Series/Hx0.var +*) + +(* UNEXPORTED +cic:/CoRN/transc/PowerSeries/Power_Series/a.var +*) + +inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries.con" as definition. + +(*#* +The most important convergence criterium specifically for power series +is the Dirichlet criterium. +*) + +(* begin show *) + +(* UNEXPORTED +cic:/CoRN/transc/PowerSeries/Power_Series/Ha.var +*) + +inline procedural "cic:/CoRN/transc/PowerSeries/Power_Series/r.con" "Power_Series__" as definition. + +inline procedural "cic:/CoRN/transc/PowerSeries/Power_Series/Hr.con" "Power_Series__" as definition. + +(* end show *) + +inline procedural "cic:/CoRN/transc/PowerSeries/Dirichlet_crit.con" as lemma. + +(*#* +When defining a function using its Taylor series as a motivation, the following operator can be of use. +*) + +inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'.con" as definition. + +(*#* +This function is also continuous and has a good convergence ratio. +*) + +inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_cont.con" as lemma. + +inline procedural "cic:/CoRN/transc/PowerSeries/included_FPowerSeries'.con" as lemma. + +(* begin show *) + +(* UNEXPORTED +cic:/CoRN/transc/PowerSeries/Power_Series/Ha'.var +*) + +(* end show *) + +inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv'.con" as lemma. + +inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv.con" as lemma. + +(* UNEXPORTED +End Power_Series +*) + +(* UNEXPORTED +Hint Resolve FPowerSeries'_cont: continuous. +*) + +(* UNEXPORTED +Section More_on_PowerSeries +*) + +(*#* +%\begin{convention}% Let [F] and [G] be the power series defined +respectively by [a] and by [fun n => (a (S n))]. +%\end{convention}% +*) + +(* UNEXPORTED +cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/x0.var +*) + +(* UNEXPORTED +cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/a.var +*) + +(* begin hide *) + +inline procedural "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/F.con" "More_on_PowerSeries__" as definition. + +inline procedural "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/G.con" "More_on_PowerSeries__" as definition. + +(* end hide *) + +(* begin show *) + +(* UNEXPORTED +cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hf.var +*) + +(* UNEXPORTED +cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hf'.var +*) + +(* UNEXPORTED +cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hg.var +*) + +(* end show *) + +(*#* We get a comparison test for power series. *) + +inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_comp.con" as lemma. + +(*#* And a rule for differentiation. *) + +(* UNEXPORTED +Opaque nring fac. +*) + +inline procedural "cic:/CoRN/transc/PowerSeries/Derivative_FPowerSeries1'.con" as lemma. + +(* UNEXPORTED +End More_on_PowerSeries +*) + +(* UNEXPORTED +Section Definitions +*) + +(*#* **Function definitions through power series + +We now define the exponential, sine and cosine functions as power +series, and prove their convergence. Tangent is defined as the +quotient of sine over cosine. +*) + +inline procedural "cic:/CoRN/transc/PowerSeries/Exp_ps.con" as definition. + +inline procedural "cic:/CoRN/transc/PowerSeries/sin_seq.con" as definition. + +inline procedural "cic:/CoRN/transc/PowerSeries/sin_ps.con" as definition. + +inline procedural "cic:/CoRN/transc/PowerSeries/cos_seq.con" as definition. + +inline procedural "cic:/CoRN/transc/PowerSeries/cos_ps.con" as definition. + +inline procedural "cic:/CoRN/transc/PowerSeries/Exp_conv'.con" as lemma. + +inline procedural "cic:/CoRN/transc/PowerSeries/Exp_conv.con" as lemma. + +inline procedural "cic:/CoRN/transc/PowerSeries/sin_conv.con" as lemma. + +inline procedural "cic:/CoRN/transc/PowerSeries/cos_conv.con" as lemma. + +inline procedural "cic:/CoRN/transc/PowerSeries/Expon.con" as definition. + +inline procedural "cic:/CoRN/transc/PowerSeries/Sine.con" as definition. + +inline procedural "cic:/CoRN/transc/PowerSeries/Cosine.con" as definition. + +inline procedural "cic:/CoRN/transc/PowerSeries/Tang.con" as definition. + +(*#* +Some auxiliary domain results. +*) + +inline procedural "cic:/CoRN/transc/PowerSeries/Exp_domain.con" as lemma. + +inline procedural "cic:/CoRN/transc/PowerSeries/sin_domain.con" as lemma. + +inline procedural "cic:/CoRN/transc/PowerSeries/cos_domain.con" as lemma. + +inline procedural "cic:/CoRN/transc/PowerSeries/included_Exp.con" as lemma. + +inline procedural "cic:/CoRN/transc/PowerSeries/included_Sin.con" as lemma. + +inline procedural "cic:/CoRN/transc/PowerSeries/included_Cos.con" as lemma. + +(*#* +Definition of the logarithm. +*) + +inline procedural "cic:/CoRN/transc/PowerSeries/log_defn_lemma.con" as lemma. + +inline procedural "cic:/CoRN/transc/PowerSeries/Logarithm.con" as definition. + +(* UNEXPORTED +End Definitions +*) + +(* UNEXPORTED +Hint Resolve included_Exp included_Sin included_Cos: included. +*) + +(*#* +As most of these functions are total, it makes sense to treat them as setoid functions on the reals. In the case of logarithm and tangent, this is not possible; however, we still define some abbreviations for aesthetical reasons. +*) + +inline procedural "cic:/CoRN/transc/PowerSeries/Exp.con" as definition. + +inline procedural "cic:/CoRN/transc/PowerSeries/Sin.con" as definition. + +inline procedural "cic:/CoRN/transc/PowerSeries/Cos.con" as definition. + +inline procedural "cic:/CoRN/transc/PowerSeries/Log.con" as definition. + +inline procedural "cic:/CoRN/transc/PowerSeries/Tan.con" as definition. +