]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/CoRN/transc/PowerSeries.mma
made executable again
[helm.git] / matita / matita / contribs / procedural / CoRN / transc / PowerSeries.mma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "CoRN.ma".
18
19 (* $Id: PowerSeries.v,v 1.8 2004/04/23 10:01:08 lcf Exp $ *)
20
21 (*#* printing Exp %\ensuremath{\exp}% *)
22
23 (*#* printing Sin %\ensuremath{\sin}% *)
24
25 (*#* printing Cos %\ensuremath{\cos}% *)
26
27 (*#* printing Log %\ensuremath{\log}% *)
28
29 (*#* printing Tan %\ensuremath{\tan}% *)
30
31 include "ftc/FTC.ma".
32
33 (*#* *More on Power Series
34
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.
38 *)
39
40 (* UNEXPORTED
41 Section Power_Series
42 *)
43
44 (*#* **General results
45
46 %\begin{convention}% Let [J : interval] and [x0 : IR] be a point of [J].
47 Let [a : nat -> IR].
48 %\end{convention}%
49 *)
50
51 (* UNEXPORTED
52 cic:/CoRN/transc/PowerSeries/Power_Series/J.var
53 *)
54
55 (* UNEXPORTED
56 cic:/CoRN/transc/PowerSeries/Power_Series/x0.var
57 *)
58
59 (* UNEXPORTED
60 cic:/CoRN/transc/PowerSeries/Power_Series/Hx0.var
61 *)
62
63 (* UNEXPORTED
64 cic:/CoRN/transc/PowerSeries/Power_Series/a.var
65 *)
66
67 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries.con" as definition.
68
69 (*#*
70 The most important convergence criterium specifically for power series
71 is the Dirichlet criterium.
72 *)
73
74 (* begin show *)
75
76 (* UNEXPORTED
77 cic:/CoRN/transc/PowerSeries/Power_Series/Ha.var
78 *)
79
80 inline procedural "cic:/CoRN/transc/PowerSeries/Power_Series/r.con" "Power_Series__" as definition.
81
82 inline procedural "cic:/CoRN/transc/PowerSeries/Power_Series/Hr.con" "Power_Series__" as definition.
83
84 (* end show *)
85
86 inline procedural "cic:/CoRN/transc/PowerSeries/Dirichlet_crit.con" as lemma.
87
88 (*#*
89 When defining a function using its Taylor series as a motivation, the following operator can be of use.
90 *)
91
92 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'.con" as definition.
93
94 (*#*
95 This function is also continuous and has a good convergence ratio.
96 *)
97
98 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_cont.con" as lemma.
99
100 inline procedural "cic:/CoRN/transc/PowerSeries/included_FPowerSeries'.con" as lemma.
101
102 (* begin show *)
103
104 (* UNEXPORTED
105 cic:/CoRN/transc/PowerSeries/Power_Series/Ha'.var
106 *)
107
108 (* end show *)
109
110 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv'.con" as lemma.
111
112 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv.con" as lemma.
113
114 (* UNEXPORTED
115 End Power_Series
116 *)
117
118 (* UNEXPORTED
119 Hint Resolve FPowerSeries'_cont: continuous.
120 *)
121
122 (* UNEXPORTED
123 Section More_on_PowerSeries
124 *)
125
126 (*#*
127 %\begin{convention}% Let [F] and [G] be the power series defined
128 respectively by [a] and by [fun n => (a (S n))].
129 %\end{convention}%
130 *)
131
132 (* UNEXPORTED
133 cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/x0.var
134 *)
135
136 (* UNEXPORTED
137 cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/a.var
138 *)
139
140 (* begin hide *)
141
142 inline procedural "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/F.con" "More_on_PowerSeries__" as definition.
143
144 inline procedural "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/G.con" "More_on_PowerSeries__" as definition.
145
146 (* end hide *)
147
148 (* begin show *)
149
150 (* UNEXPORTED
151 cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hf.var
152 *)
153
154 (* UNEXPORTED
155 cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hf'.var
156 *)
157
158 (* UNEXPORTED
159 cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hg.var
160 *)
161
162 (* end show *)
163
164 (*#* We get a comparison test for power series. *)
165
166 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_comp.con" as lemma.
167
168 (*#* And a rule for differentiation. *)
169
170 (* UNEXPORTED
171 Opaque nring fac.
172 *)
173
174 inline procedural "cic:/CoRN/transc/PowerSeries/Derivative_FPowerSeries1'.con" as lemma.
175
176 (* UNEXPORTED
177 End More_on_PowerSeries
178 *)
179
180 (* UNEXPORTED
181 Section Definitions
182 *)
183
184 (*#* **Function definitions through power series
185
186 We now define the exponential, sine and cosine functions as power
187 series, and prove their convergence.  Tangent is defined as the
188 quotient of sine over cosine.
189 *)
190
191 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_ps.con" as definition.
192
193 inline procedural "cic:/CoRN/transc/PowerSeries/sin_seq.con" as definition.
194
195 inline procedural "cic:/CoRN/transc/PowerSeries/sin_ps.con" as definition.
196
197 inline procedural "cic:/CoRN/transc/PowerSeries/cos_seq.con" as definition.
198
199 inline procedural "cic:/CoRN/transc/PowerSeries/cos_ps.con" as definition.
200
201 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_conv'.con" as lemma.
202
203 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_conv.con" as lemma.
204
205 inline procedural "cic:/CoRN/transc/PowerSeries/sin_conv.con" as lemma.
206
207 inline procedural "cic:/CoRN/transc/PowerSeries/cos_conv.con" as lemma.
208
209 inline procedural "cic:/CoRN/transc/PowerSeries/Expon.con" as definition.
210
211 inline procedural "cic:/CoRN/transc/PowerSeries/Sine.con" as definition.
212
213 inline procedural "cic:/CoRN/transc/PowerSeries/Cosine.con" as definition.
214
215 inline procedural "cic:/CoRN/transc/PowerSeries/Tang.con" as definition.
216
217 (*#*
218 Some auxiliary domain results.
219 *)
220
221 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_domain.con" as lemma.
222
223 inline procedural "cic:/CoRN/transc/PowerSeries/sin_domain.con" as lemma.
224
225 inline procedural "cic:/CoRN/transc/PowerSeries/cos_domain.con" as lemma.
226
227 inline procedural "cic:/CoRN/transc/PowerSeries/included_Exp.con" as lemma.
228
229 inline procedural "cic:/CoRN/transc/PowerSeries/included_Sin.con" as lemma.
230
231 inline procedural "cic:/CoRN/transc/PowerSeries/included_Cos.con" as lemma.
232
233 (*#*
234 Definition of the logarithm.
235 *)
236
237 inline procedural "cic:/CoRN/transc/PowerSeries/log_defn_lemma.con" as lemma.
238
239 inline procedural "cic:/CoRN/transc/PowerSeries/Logarithm.con" as definition.
240
241 (* UNEXPORTED
242 End Definitions
243 *)
244
245 (* UNEXPORTED
246 Hint Resolve included_Exp included_Sin included_Cos: included.
247 *)
248
249 (*#*
250 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.
251 *)
252
253 inline procedural "cic:/CoRN/transc/PowerSeries/Exp.con" as definition.
254
255 inline procedural "cic:/CoRN/transc/PowerSeries/Sin.con" as definition.
256
257 inline procedural "cic:/CoRN/transc/PowerSeries/Cos.con" as definition.
258
259 inline procedural "cic:/CoRN/transc/PowerSeries/Log.con" as definition.
260
261 inline procedural "cic:/CoRN/transc/PowerSeries/Tan.con" as definition.
262