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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/transc/PowerSeries".
21 (* $Id: PowerSeries.v,v 1.8 2004/04/23 10:01:08 lcf Exp $ *)
23 (*#* printing Exp %\ensuremath{\exp}% *)
25 (*#* printing Sin %\ensuremath{\sin}% *)
27 (*#* printing Cos %\ensuremath{\cos}% *)
29 (*#* printing Log %\ensuremath{\log}% *)
31 (*#* printing Tan %\ensuremath{\tan}% *)
35 (*#* *More on Power Series
37 We will now formally define an operator that defines a function as the
38 sum of some series given a number sequence. Along with it, we will
39 prove some important properties of these entities.
46 (*#* **General results
48 %\begin{convention}% Let [J : interval] and [x0 : IR] be a point of [J].
53 alias id "J" = "cic:/CoRN/transc/PowerSeries/Power_Series/J.var".
55 alias id "x0" = "cic:/CoRN/transc/PowerSeries/Power_Series/x0.var".
57 alias id "Hx0" = "cic:/CoRN/transc/PowerSeries/Power_Series/Hx0.var".
59 alias id "a" = "cic:/CoRN/transc/PowerSeries/Power_Series/a.var".
61 inline "cic:/CoRN/transc/PowerSeries/FPowerSeries.con".
64 The most important convergence criterium specifically for power series
65 is the Dirichlet criterium.
70 alias id "Ha" = "cic:/CoRN/transc/PowerSeries/Power_Series/Ha.var".
72 inline "cic:/CoRN/transc/PowerSeries/Power_Series/r.con" "Power_Series__".
74 inline "cic:/CoRN/transc/PowerSeries/Power_Series/Hr.con" "Power_Series__".
78 inline "cic:/CoRN/transc/PowerSeries/Dirichlet_crit.con".
81 When defining a function using its Taylor series as a motivation, the following operator can be of use.
84 inline "cic:/CoRN/transc/PowerSeries/FPowerSeries'.con".
87 This function is also continuous and has a good convergence ratio.
90 inline "cic:/CoRN/transc/PowerSeries/FPowerSeries'_cont.con".
92 inline "cic:/CoRN/transc/PowerSeries/included_FPowerSeries'.con".
96 alias id "Ha'" = "cic:/CoRN/transc/PowerSeries/Power_Series/Ha'.var".
100 inline "cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv'.con".
102 inline "cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv.con".
109 Hint Resolve FPowerSeries'_cont: continuous.
113 Section More_on_PowerSeries
117 %\begin{convention}% Let [F] and [G] be the power series defined
118 respectively by [a] and by [fun n => (a (S n))].
122 alias id "x0" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/x0.var".
124 alias id "a" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/a.var".
128 inline "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/F.con" "More_on_PowerSeries__".
130 inline "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/G.con" "More_on_PowerSeries__".
136 alias id "Hf" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hf.var".
138 alias id "Hf'" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hf'.var".
140 alias id "Hg" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hg.var".
144 (*#* We get a comparison test for power series. *)
146 inline "cic:/CoRN/transc/PowerSeries/FPowerSeries'_comp.con".
148 (*#* And a rule for differentiation. *)
154 inline "cic:/CoRN/transc/PowerSeries/Derivative_FPowerSeries1'.con".
157 End More_on_PowerSeries
164 (*#* **Function definitions through power series
166 We now define the exponential, sine and cosine functions as power
167 series, and prove their convergence. Tangent is defined as the
168 quotient of sine over cosine.
171 inline "cic:/CoRN/transc/PowerSeries/Exp_ps.con".
173 inline "cic:/CoRN/transc/PowerSeries/sin_seq.con".
175 inline "cic:/CoRN/transc/PowerSeries/sin_ps.con".
177 inline "cic:/CoRN/transc/PowerSeries/cos_seq.con".
179 inline "cic:/CoRN/transc/PowerSeries/cos_ps.con".
181 inline "cic:/CoRN/transc/PowerSeries/Exp_conv'.con".
183 inline "cic:/CoRN/transc/PowerSeries/Exp_conv.con".
185 inline "cic:/CoRN/transc/PowerSeries/sin_conv.con".
187 inline "cic:/CoRN/transc/PowerSeries/cos_conv.con".
189 inline "cic:/CoRN/transc/PowerSeries/Expon.con".
191 inline "cic:/CoRN/transc/PowerSeries/Sine.con".
193 inline "cic:/CoRN/transc/PowerSeries/Cosine.con".
195 inline "cic:/CoRN/transc/PowerSeries/Tang.con".
198 Some auxiliary domain results.
201 inline "cic:/CoRN/transc/PowerSeries/Exp_domain.con".
203 inline "cic:/CoRN/transc/PowerSeries/sin_domain.con".
205 inline "cic:/CoRN/transc/PowerSeries/cos_domain.con".
207 inline "cic:/CoRN/transc/PowerSeries/included_Exp.con".
209 inline "cic:/CoRN/transc/PowerSeries/included_Sin.con".
211 inline "cic:/CoRN/transc/PowerSeries/included_Cos.con".
214 Definition of the logarithm.
217 inline "cic:/CoRN/transc/PowerSeries/log_defn_lemma.con".
219 inline "cic:/CoRN/transc/PowerSeries/Logarithm.con".
226 Hint Resolve included_Exp included_Sin included_Cos: included.
230 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.
233 inline "cic:/CoRN/transc/PowerSeries/Exp.con".
235 inline "cic:/CoRN/transc/PowerSeries/Sin.con".
237 inline "cic:/CoRN/transc/PowerSeries/Cos.con".
239 inline "cic:/CoRN/transc/PowerSeries/Log.con".
241 inline "cic:/CoRN/transc/PowerSeries/Tan.con".