--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+
projects / helm.git / blobdiff