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".
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}% *)
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 inline cic:/CoRN/transc/PowerSeries/J.var.
55 inline cic:/CoRN/transc/PowerSeries/x0.var.
57 inline cic:/CoRN/transc/PowerSeries/Hx0.var.
59 inline cic:/CoRN/transc/PowerSeries/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 inline cic:/CoRN/transc/PowerSeries/Ha.var.
72 inline cic:/CoRN/transc/PowerSeries/r.con.
74 inline cic:/CoRN/transc/PowerSeries/Hr.con.
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 inline cic:/CoRN/transc/PowerSeries/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 inline cic:/CoRN/transc/PowerSeries/x0.var.
124 inline cic:/CoRN/transc/PowerSeries/a.var.
128 inline cic:/CoRN/transc/PowerSeries/F.con.
130 inline cic:/CoRN/transc/PowerSeries/G.con.
136 inline cic:/CoRN/transc/PowerSeries/Hf.var.
138 inline cic:/CoRN/transc/PowerSeries/Hf'.var.
140 inline cic:/CoRN/transc/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.