]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/procedural/CoRN/ftc/MoreFunSeries.mma
ground_2 released and permanently renamed as ground
[helm.git] / helm / software / matita / contribs / procedural / CoRN / ftc / MoreFunSeries.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: MoreFunSeries.v,v 1.4 2004/04/23 10:00:59 lcf Exp $ *)
20
21 include "ftc/FunctSeries.ma".
22
23 include "ftc/MoreFunctions.ma".
24
25 (*#* printing FSeries_Sum %\ensuremath{\sum_{\infty}}% #&sum;'<sub>&infin;</sub># *)
26
27 (* UNEXPORTED
28 Section Definitions
29 *)
30
31 (*#* *More on Sequences and Series
32
33 We will now extend our convergence definitions and results for
34 sequences and series of functions defined in compact intervals to
35 arbitrary intervals.
36
37 %\begin{convention}% Throughout this file, [J] will be an interval,
38 [f, g] will be sequences of continuous (in [J]) functions and [F,G]
39 will be continuous (in [J]) functions.
40 %\end{convention}%
41
42 **Sequences
43
44 First we will consider the case of sequences.
45
46 ***Definitions
47
48 Some of the definitions do not make sense in this more general setting
49 (for instance, because the norm of a function is no longer defined),
50 but the ones which do we simply adapt in the usual way.
51 *)
52
53 (* UNEXPORTED
54 cic:/CoRN/ftc/MoreFunSeries/Definitions/J.var
55 *)
56
57 (* UNEXPORTED
58 cic:/CoRN/ftc/MoreFunSeries/Definitions/f.var
59 *)
60
61 (* UNEXPORTED
62 cic:/CoRN/ftc/MoreFunSeries/Definitions/F.var
63 *)
64
65 (* UNEXPORTED
66 cic:/CoRN/ftc/MoreFunSeries/Definitions/contf.var
67 *)
68
69 (* UNEXPORTED
70 cic:/CoRN/ftc/MoreFunSeries/Definitions/contF.var
71 *)
72
73 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_IR.con" as definition.
74
75 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_IR.con" as definition.
76
77 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_IR.con" as definition.
78
79 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_IR.con" as definition.
80
81 (*#*
82 The equivalences between these definitions still hold.
83 *)
84
85 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq'_IR.con" as lemma.
86
87 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_seq2_IR.con" as lemma.
88
89 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_seq_IR.con" as lemma.
90
91 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_real_IR.con" as lemma.
92
93 (* UNEXPORTED
94 End Definitions
95 *)
96
97 (* UNEXPORTED
98 Section More_Definitions
99 *)
100
101 (*#*
102 Limit is defined and works in the same way as before.
103 *)
104
105 (* UNEXPORTED
106 cic:/CoRN/ftc/MoreFunSeries/More_Definitions/J.var
107 *)
108
109 (* UNEXPORTED
110 cic:/CoRN/ftc/MoreFunSeries/More_Definitions/f.var
111 *)
112
113 (* UNEXPORTED
114 cic:/CoRN/ftc/MoreFunSeries/More_Definitions/contf.var
115 *)
116
117 (* begin show *)
118
119 (* UNEXPORTED
120 cic:/CoRN/ftc/MoreFunSeries/More_Definitions/conv.var
121 *)
122
123 (* end show *)
124
125 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_IR.con" as definition.
126
127 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_char.con" as lemma.
128
129 (* UNEXPORTED
130 End More_Definitions
131 *)
132
133 (* UNEXPORTED
134 Section Irrelevance_of_Proofs
135 *)
136
137 (*#* ***Basic Properties
138
139 Proofs are irrelevant as before---they just have to be present.
140 *)
141
142 (* UNEXPORTED
143 cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/J.var
144 *)
145
146 (* UNEXPORTED
147 cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/f.var
148 *)
149
150 (* begin show *)
151
152 (* UNEXPORTED
153 cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contf.var
154 *)
155
156 (* UNEXPORTED
157 cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contf0.var
158 *)
159
160 (* end show *)
161
162 (* UNEXPORTED
163 cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/F.var
164 *)
165
166 (* begin show *)
167
168 (* UNEXPORTED
169 cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contF.var
170 *)
171
172 (* UNEXPORTED
173 cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contF0.var
174 *)
175
176 (* end show *)
177
178 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wd_IR.con" as lemma.
179
180 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_wd_IR.con" as lemma.
181
182 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_wd_IR.con" as lemma.
183
184 (* UNEXPORTED
185 End Irrelevance_of_Proofs
186 *)
187
188 (* UNEXPORTED
189 Opaque Cauchy_fun_seq_Lim_IR.
190 *)
191
192 (* UNEXPORTED
193 Section More_Properties
194 *)
195
196 (* UNEXPORTED
197 cic:/CoRN/ftc/MoreFunSeries/More_Properties/J.var
198 *)
199
200 (* UNEXPORTED
201 cic:/CoRN/ftc/MoreFunSeries/More_Properties/f.var
202 *)
203
204 (* UNEXPORTED
205 cic:/CoRN/ftc/MoreFunSeries/More_Properties/g.var
206 *)
207
208 (* begin show *)
209
210 (* UNEXPORTED
211 cic:/CoRN/ftc/MoreFunSeries/More_Properties/contf.var
212 *)
213
214 (* UNEXPORTED
215 cic:/CoRN/ftc/MoreFunSeries/More_Properties/contf0.var
216 *)
217
218 (* UNEXPORTED
219 cic:/CoRN/ftc/MoreFunSeries/More_Properties/contg.var
220 *)
221
222 (* UNEXPORTED
223 cic:/CoRN/ftc/MoreFunSeries/More_Properties/contg0.var
224 *)
225
226 (* end show *)
227
228 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq'_IR.con" as lemma.
229
230 (* UNEXPORTED
231 cic:/CoRN/ftc/MoreFunSeries/More_Properties/F.var
232 *)
233
234 (* UNEXPORTED
235 cic:/CoRN/ftc/MoreFunSeries/More_Properties/G.var
236 *)
237
238 (* begin show *)
239
240 (* UNEXPORTED
241 cic:/CoRN/ftc/MoreFunSeries/More_Properties/contF.var
242 *)
243
244 (* UNEXPORTED
245 cic:/CoRN/ftc/MoreFunSeries/More_Properties/contF0.var
246 *)
247
248 (* UNEXPORTED
249 cic:/CoRN/ftc/MoreFunSeries/More_Properties/contG.var
250 *)
251
252 (* UNEXPORTED
253 cic:/CoRN/ftc/MoreFunSeries/More_Properties/contG0.var
254 *)
255
256 (* end show *)
257
258 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl_IR.con" as lemma.
259
260 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr_IR.con" as lemma.
261
262 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl'_IR.con" as lemma.
263
264 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr'_IR.con" as lemma.
265
266 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_cont_Lim_IR.con" as lemma.
267
268 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq_IR.con" as lemma.
269
270 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq_IR.con" as lemma.
271
272 (* UNEXPORTED
273 End More_Properties
274 *)
275
276 (* UNEXPORTED
277 Hint Resolve Cauchy_cont_Lim_IR: continuous.
278 *)
279
280 (* UNEXPORTED
281 Section Algebraic_Properties
282 *)
283
284 (*#* ***Algebraic Properties
285
286 Algebraic operations still work well.
287 *)
288
289 (* UNEXPORTED
290 cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/J.var
291 *)
292
293 (* UNEXPORTED
294 cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/f.var
295 *)
296
297 (* UNEXPORTED
298 cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/g.var
299 *)
300
301 (* UNEXPORTED
302 cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contf.var
303 *)
304
305 (* UNEXPORTED
306 cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contg.var
307 *)
308
309 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FLim_unique_IR.con" as lemma.
310
311 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_wd_IR.con" as lemma.
312
313 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_const_IR.con" as lemma.
314
315 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_const_IR.con" as lemma.
316
317 (* UNEXPORTED
318 cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/F.var
319 *)
320
321 (* UNEXPORTED
322 cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/G.var
323 *)
324
325 (* UNEXPORTED
326 cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contF.var
327 *)
328
329 (* UNEXPORTED
330 cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contG.var
331 *)
332
333 (* begin show *)
334
335 (* UNEXPORTED
336 cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/convF.var
337 *)
338
339 (* UNEXPORTED
340 cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/convG.var
341 *)
342
343 (* end show *)
344
345 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus'_IR.con" as lemma.
346
347 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus'_IR.con" as lemma.
348
349 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult'_IR.con" as lemma.
350
351 (* UNEXPORTED
352 End Algebraic_Properties
353 *)
354
355 (* UNEXPORTED
356 Section More_Algebraic_Properties
357 *)
358
359 (*#*
360 If we work with the limit function things fit in just as well.
361 *)
362
363 (* UNEXPORTED
364 cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/J.var
365 *)
366
367 (* UNEXPORTED
368 cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/f.var
369 *)
370
371 (* UNEXPORTED
372 cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/g.var
373 *)
374
375 (* UNEXPORTED
376 cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/contf.var
377 *)
378
379 (* UNEXPORTED
380 cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/contg.var
381 *)
382
383 (* begin show *)
384
385 (* UNEXPORTED
386 cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/Hf.var
387 *)
388
389 (* UNEXPORTED
390 cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/Hg.var
391 *)
392
393 (* end show *)
394
395 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus_IR.con" as lemma.
396
397 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_plus.con" as lemma.
398
399 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_inv_IR.con" as lemma.
400
401 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_inv.con" as lemma.
402
403 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus_IR.con" as lemma.
404
405 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_minus.con" as lemma.
406
407 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult_IR.con" as lemma.
408
409 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_mult.con" as lemma.
410
411 (* UNEXPORTED
412 End More_Algebraic_Properties
413 *)
414
415 (* UNEXPORTED
416 Section Other
417 *)
418
419 (*#* ***Miscellaneous
420
421 Finally, we define a mapping between sequences of real numbers and sequences of (constant) functions and prove that convergence is preserved.
422 *)
423
424 inline procedural "cic:/CoRN/ftc/MoreFunSeries/seq_to_funseq.con" as definition.
425
426 inline procedural "cic:/CoRN/ftc/MoreFunSeries/funseq_conv.con" as lemma.
427
428 (*#*
429 Another interesting fact: if a sequence of constant functions converges then it must converge to a constant function.
430 *)
431
432 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_const_Lim.con" as lemma.
433
434 (* UNEXPORTED
435 End Other
436 *)
437
438 (* UNEXPORTED
439 Section Series_Definitions
440 *)
441
442 (*#* **Series
443
444 We now consider series of functions defined in arbitrary intervals.
445
446 Convergence is defined as expected---through convergence in every compact interval.
447 *)
448
449 (* UNEXPORTED
450 cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/J.var
451 *)
452
453 (* UNEXPORTED
454 cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/f.var
455 *)
456
457 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_IR.con" as definition.
458
459 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_series_conv_imp_conv_IR.con" as lemma.
460
461 (* begin show *)
462
463 (* UNEXPORTED
464 cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/H.var
465 *)
466
467 (* end show *)
468
469 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_series_inc_IR.con" as lemma.
470
471 (*#* Assume [h(x)] is the pointwise series of [f(x)] *)
472
473 (* begin hide *)
474
475 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/h.con" "Series_Definitions__" as definition.
476
477 (* end hide *)
478
479 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_strext_IR.con" as lemma.
480
481 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum.con" as definition.
482
483 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_char.con" as lemma.
484
485 (* UNEXPORTED
486 End Series_Definitions
487 *)
488
489 (* UNEXPORTED
490 Implicit Arguments FSeries_Sum [J f].
491 *)
492
493 (* UNEXPORTED
494 Section More_Series_Definitions
495 *)
496
497 (* UNEXPORTED
498 cic:/CoRN/ftc/MoreFunSeries/More_Series_Definitions/J.var
499 *)
500
501 (* UNEXPORTED
502 cic:/CoRN/ftc/MoreFunSeries/More_Series_Definitions/f.var
503 *)
504
505 (*#*
506 Absolute convergence still exists.
507 *)
508
509 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_series_abs_convergent_IR.con" as definition.
510
511 (* UNEXPORTED
512 End More_Series_Definitions
513 *)
514
515 (* UNEXPORTED
516 Section Convergence_Results
517 *)
518
519 (*#*
520 As before, any series converges to its sum.
521 *)
522
523 (* UNEXPORTED
524 cic:/CoRN/ftc/MoreFunSeries/Convergence_Results/J.var
525 *)
526
527 (* UNEXPORTED
528 cic:/CoRN/ftc/MoreFunSeries/Convergence_Results/f.var
529 *)
530
531 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_conv.con" as lemma.
532
533 inline procedural "cic:/CoRN/ftc/MoreFunSeries/convergent_imp_inc.con" as lemma.
534
535 inline procedural "cic:/CoRN/ftc/MoreFunSeries/convergent_imp_Continuous.con" as lemma.
536
537 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Continuous_FSeries_Sum.con" as lemma.
538
539 (* UNEXPORTED
540 End Convergence_Results
541 *)
542
543 (* UNEXPORTED
544 Hint Resolve convergent_imp_inc: included.
545 *)
546
547 (* UNEXPORTED
548 Hint Resolve convergent_imp_Continuous Continuous_FSeries_Sum: continuous.
549 *)
550
551 (* UNEXPORTED
552 Section Operations
553 *)
554
555 (*#* **Algebraic Operations
556
557 Convergence is well defined and preserved by operations.
558 *)
559
560 (* UNEXPORTED
561 cic:/CoRN/ftc/MoreFunSeries/Operations/J.var
562 *)
563
564 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_const_series_IR.con" as lemma.
565
566 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_const_series_Sum_IR.con" as lemma.
567
568 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_zero_fun_series_IR.con" as lemma.
569
570 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_zero_IR.con" as lemma.
571
572 (* UNEXPORTED
573 cic:/CoRN/ftc/MoreFunSeries/Operations/f.var
574 *)
575
576 (* UNEXPORTED
577 cic:/CoRN/ftc/MoreFunSeries/Operations/g.var
578 *)
579
580 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_wd_IR.con" as lemma.
581
582 (* begin show *)
583
584 (* UNEXPORTED
585 cic:/CoRN/ftc/MoreFunSeries/Operations/convF.var
586 *)
587
588 (* UNEXPORTED
589 cic:/CoRN/ftc/MoreFunSeries/Operations/convG.var
590 *)
591
592 (* end show *)
593
594 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_wd'.con" as lemma.
595
596 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus_conv.con" as lemma.
597
598 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus.con" as lemma.
599
600 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv_conv.con" as lemma.
601
602 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv.con" as lemma.
603
604 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus_conv.con" as lemma.
605
606 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus.con" as lemma.
607
608 (*#*
609 %\begin{convention}% Let [c:IR] and [H:PartIR] be continuous in [J].
610 %\end{convention}%
611 *)
612
613 (* UNEXPORTED
614 cic:/CoRN/ftc/MoreFunSeries/Operations/c.var
615 *)
616
617 (* UNEXPORTED
618 cic:/CoRN/ftc/MoreFunSeries/Operations/H.var
619 *)
620
621 (* UNEXPORTED
622 cic:/CoRN/ftc/MoreFunSeries/Operations/contH.var
623 *)
624
625 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal_conv.con" as lemma.
626
627 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal.con" as lemma.
628
629 (* UNEXPORTED
630 End Operations
631 *)
632
633 (* UNEXPORTED
634 Section Convergence_Criteria
635 *)
636
637 (*#* ***Convergence Criteria
638
639 The most important tests for convergence of series still apply: the
640 comparison test (in both versions) and the ratio test.
641 *)
642
643 (* UNEXPORTED
644 cic:/CoRN/ftc/MoreFunSeries/Convergence_Criteria/J.var
645 *)
646
647 (* UNEXPORTED
648 cic:/CoRN/ftc/MoreFunSeries/Convergence_Criteria/f.var
649 *)
650
651 (* UNEXPORTED
652 cic:/CoRN/ftc/MoreFunSeries/Convergence_Criteria/contF.var
653 *)
654
655 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_str_comparison_IR.con" as lemma.
656
657 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_comparison_IR.con" as lemma.
658
659 inline procedural "cic:/CoRN/ftc/MoreFunSeries/abs_imp_conv_IR.con" as lemma.
660
661 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_ratio_test_conv_IR.con" as lemma.
662
663 (* UNEXPORTED
664 End Convergence_Criteria
665 *)
666
667 (* UNEXPORTED
668 Section Insert_Series
669 *)
670
671 (*#* ***Translation
672
673 When working in particular with power series and Taylor series, it is 
674 sometimes useful to ``shift'' all the terms in the series one position 
675 forward, that is, replacing each $f_{i+1}$#f<sub>i+1</sub># with
676 $f_i$#f<sub>i</sub># and inserting the null function in the first 
677 position.  This does not affect convergence or the sum of the series.
678 *)
679
680 (* UNEXPORTED
681 cic:/CoRN/ftc/MoreFunSeries/Insert_Series/J.var
682 *)
683
684 (* UNEXPORTED
685 cic:/CoRN/ftc/MoreFunSeries/Insert_Series/f.var
686 *)
687
688 (* UNEXPORTED
689 cic:/CoRN/ftc/MoreFunSeries/Insert_Series/convF.var
690 *)
691
692 inline procedural "cic:/CoRN/ftc/MoreFunSeries/insert_series.con" as definition.
693
694 inline procedural "cic:/CoRN/ftc/MoreFunSeries/insert_series_cont.con" as lemma.
695
696 inline procedural "cic:/CoRN/ftc/MoreFunSeries/insert_series_sum_char.con" as lemma.
697
698 inline procedural "cic:/CoRN/ftc/MoreFunSeries/insert_series_conv.con" as lemma.
699
700 inline procedural "cic:/CoRN/ftc/MoreFunSeries/insert_series_sum.con" as lemma.
701
702 (* UNEXPORTED
703 End Insert_Series
704 *)
705