1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: PowerSeries.v,v 1.8 2004/04/23 10:01:08 lcf Exp $ *)
21 (*#* printing Exp %\ensuremath{\exp}% *)
23 (*#* printing Sin %\ensuremath{\sin}% *)
25 (*#* printing Cos %\ensuremath{\cos}% *)
27 (*#* printing Log %\ensuremath{\log}% *)
29 (*#* printing Tan %\ensuremath{\tan}% *)
33 (*#* *More on Power Series
35 We will now formally define an operator that defines a function as the
36 sum of some series given a number sequence. Along with it, we will
37 prove some important properties of these entities.
44 (*#* **General results
46 %\begin{convention}% Let [J : interval] and [x0 : IR] be a point of [J].
51 alias id "J" = "cic:/CoRN/transc/PowerSeries/Power_Series/J.var".
53 alias id "x0" = "cic:/CoRN/transc/PowerSeries/Power_Series/x0.var".
55 alias id "Hx0" = "cic:/CoRN/transc/PowerSeries/Power_Series/Hx0.var".
57 alias id "a" = "cic:/CoRN/transc/PowerSeries/Power_Series/a.var".
59 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries.con".
62 The most important convergence criterium specifically for power series
63 is the Dirichlet criterium.
68 alias id "Ha" = "cic:/CoRN/transc/PowerSeries/Power_Series/Ha.var".
70 inline procedural "cic:/CoRN/transc/PowerSeries/Power_Series/r.con" "Power_Series__".
72 inline procedural "cic:/CoRN/transc/PowerSeries/Power_Series/Hr.con" "Power_Series__".
76 inline procedural "cic:/CoRN/transc/PowerSeries/Dirichlet_crit.con".
79 When defining a function using its Taylor series as a motivation, the following operator can be of use.
82 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'.con".
85 This function is also continuous and has a good convergence ratio.
88 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_cont.con".
90 inline procedural "cic:/CoRN/transc/PowerSeries/included_FPowerSeries'.con".
94 alias id "Ha'" = "cic:/CoRN/transc/PowerSeries/Power_Series/Ha'.var".
98 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv'.con".
100 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv.con".
107 Hint Resolve FPowerSeries'_cont: continuous.
111 Section More_on_PowerSeries
115 %\begin{convention}% Let [F] and [G] be the power series defined
116 respectively by [a] and by [fun n => (a (S n))].
120 alias id "x0" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/x0.var".
122 alias id "a" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/a.var".
126 inline procedural "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/F.con" "More_on_PowerSeries__".
128 inline procedural "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/G.con" "More_on_PowerSeries__".
134 alias id "Hf" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hf.var".
136 alias id "Hf'" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hf'.var".
138 alias id "Hg" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hg.var".
142 (*#* We get a comparison test for power series. *)
144 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_comp.con".
146 (*#* And a rule for differentiation. *)
152 inline procedural "cic:/CoRN/transc/PowerSeries/Derivative_FPowerSeries1'.con".
155 End More_on_PowerSeries
162 (*#* **Function definitions through power series
164 We now define the exponential, sine and cosine functions as power
165 series, and prove their convergence. Tangent is defined as the
166 quotient of sine over cosine.
169 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_ps.con".
171 inline procedural "cic:/CoRN/transc/PowerSeries/sin_seq.con".
173 inline procedural "cic:/CoRN/transc/PowerSeries/sin_ps.con".
175 inline procedural "cic:/CoRN/transc/PowerSeries/cos_seq.con".
177 inline procedural "cic:/CoRN/transc/PowerSeries/cos_ps.con".
179 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_conv'.con".
181 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_conv.con".
183 inline procedural "cic:/CoRN/transc/PowerSeries/sin_conv.con".
185 inline procedural "cic:/CoRN/transc/PowerSeries/cos_conv.con".
187 inline procedural "cic:/CoRN/transc/PowerSeries/Expon.con".
189 inline procedural "cic:/CoRN/transc/PowerSeries/Sine.con".
191 inline procedural "cic:/CoRN/transc/PowerSeries/Cosine.con".
193 inline procedural "cic:/CoRN/transc/PowerSeries/Tang.con".
196 Some auxiliary domain results.
199 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_domain.con".
201 inline procedural "cic:/CoRN/transc/PowerSeries/sin_domain.con".
203 inline procedural "cic:/CoRN/transc/PowerSeries/cos_domain.con".
205 inline procedural "cic:/CoRN/transc/PowerSeries/included_Exp.con".
207 inline procedural "cic:/CoRN/transc/PowerSeries/included_Sin.con".
209 inline procedural "cic:/CoRN/transc/PowerSeries/included_Cos.con".
212 Definition of the logarithm.
215 inline procedural "cic:/CoRN/transc/PowerSeries/log_defn_lemma.con".
217 inline procedural "cic:/CoRN/transc/PowerSeries/Logarithm.con".
224 Hint Resolve included_Exp included_Sin included_Cos: included.
228 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.
231 inline procedural "cic:/CoRN/transc/PowerSeries/Exp.con".
233 inline procedural "cic:/CoRN/transc/PowerSeries/Sin.con".
235 inline procedural "cic:/CoRN/transc/PowerSeries/Cos.con".
237 inline procedural "cic:/CoRN/transc/PowerSeries/Log.con".
239 inline procedural "cic:/CoRN/transc/PowerSeries/Tan.con".