X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Procedural%2Freals%2FSeries.mma;h=3ad3ce01b943ccb59e23c75b5703c8dd6ed02f9a;hb=a89360d64f1fcbba917ad743b97a2d973ecf6db2;hp=9a898a409859de5e0d5aecb20e770cdec0afc3e6;hpb=3e1e59644a24ed855a7f21bf9eab76f96577fd17;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Procedural/reals/Series.mma b/helm/software/matita/contribs/CoRN-Procedural/reals/Series.mma index 9a898a409..3ad3ce01b 100644 --- a/helm/software/matita/contribs/CoRN-Procedural/reals/Series.mma +++ b/helm/software/matita/contribs/CoRN-Procedural/reals/Series.mma @@ -45,7 +45,7 @@ To each such sequence we can assign a sequence of partial sums. alias id "x" = "cic:/CoRN/reals/Series/Definitions/x.var". -inline procedural "cic:/CoRN/reals/Series/seq_part_sum.con". +inline procedural "cic:/CoRN/reals/Series/seq_part_sum.con" as definition. (*#* For subsequent purposes it will be very useful to be able to write the @@ -53,15 +53,15 @@ difference between two arbitrary elements of the sequence of partial sums as a sum of elements of the original sequence. *) -inline procedural "cic:/CoRN/reals/Series/seq_part_sum_n.con". +inline procedural "cic:/CoRN/reals/Series/seq_part_sum_n.con" as lemma. (*#* A series is convergent iff its sequence of partial Sums is a Cauchy sequence. To each convergent series we can assign a Sum. *) -inline procedural "cic:/CoRN/reals/Series/convergent.con". +inline procedural "cic:/CoRN/reals/Series/convergent.con" as definition. -inline procedural "cic:/CoRN/reals/Series/series_sum.con". +inline procedural "cic:/CoRN/reals/Series/series_sum.con" as definition. (*#* Divergence can be characterized in a positive way, which will sometimes be useful. We thus define divergence of sequences and series and prove the @@ -69,25 +69,25 @@ obvious fact that no sequence can be both convergent and divergent, whether considered either as a sequence or as a series. *) -inline procedural "cic:/CoRN/reals/Series/divergent_seq.con". +inline procedural "cic:/CoRN/reals/Series/divergent_seq.con" as definition. -inline procedural "cic:/CoRN/reals/Series/divergent.con". +inline procedural "cic:/CoRN/reals/Series/divergent.con" as definition. -inline procedural "cic:/CoRN/reals/Series/conv_imp_not_div.con". +inline procedural "cic:/CoRN/reals/Series/conv_imp_not_div.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/div_imp_not_conv.con". +inline procedural "cic:/CoRN/reals/Series/div_imp_not_conv.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/convergent_imp_not_divergent.con". +inline procedural "cic:/CoRN/reals/Series/convergent_imp_not_divergent.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/divergent_imp_not_convergent.con". +inline procedural "cic:/CoRN/reals/Series/divergent_imp_not_convergent.con" as lemma. (*#* Finally we have the well known fact that every convergent series converges to zero as a sequence. *) -inline procedural "cic:/CoRN/reals/Series/series_seq_Lim.con". +inline procedural "cic:/CoRN/reals/Series/series_seq_Lim.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/series_seq_Lim'.con". +inline procedural "cic:/CoRN/reals/Series/series_seq_Lim'.con" as lemma. (* UNEXPORTED End Definitions @@ -101,7 +101,7 @@ alias id "x" = "cic:/CoRN/reals/Series/More_Definitions/x.var". (*#* We also define absolute convergence. *) -inline procedural "cic:/CoRN/reals/Series/abs_convergent.con". +inline procedural "cic:/CoRN/reals/Series/abs_convergent.con" as definition. (* UNEXPORTED End More_Definitions @@ -116,7 +116,7 @@ Section Power_Series Power series are an important special case. *) -inline procedural "cic:/CoRN/reals/Series/power_series.con". +inline procedural "cic:/CoRN/reals/Series/power_series.con" as definition. (*#* Specially important is the case when [c] is a positive real number @@ -133,13 +133,13 @@ alias id "H0c" = "cic:/CoRN/reals/Series/Power_Series/H0c.var". alias id "Hc1" = "cic:/CoRN/reals/Series/Power_Series/Hc1.var". -inline procedural "cic:/CoRN/reals/Series/c_exp_Lim.con". +inline procedural "cic:/CoRN/reals/Series/c_exp_Lim.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/power_series_Lim1.con". +inline procedural "cic:/CoRN/reals/Series/power_series_Lim1.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/power_series_conv.con". +inline procedural "cic:/CoRN/reals/Series/power_series_conv.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/power_series_sum.con". +inline procedural "cic:/CoRN/reals/Series/power_series_sum.con" as lemma. (* UNEXPORTED End Power_Series @@ -155,9 +155,9 @@ Some operations with series preserve convergence. We start by defining the series that is zero everywhere. *) -inline procedural "cic:/CoRN/reals/Series/conv_zero_series.con". +inline procedural "cic:/CoRN/reals/Series/conv_zero_series.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/series_sum_zero.con". +inline procedural "cic:/CoRN/reals/Series/series_sum_zero.con" as lemma. (*#* Next we consider extensionality, as well as the sum and difference of two convergent series. @@ -174,25 +174,25 @@ alias id "convX" = "cic:/CoRN/reals/Series/Operations/convX.var". alias id "convY" = "cic:/CoRN/reals/Series/Operations/convY.var". -inline procedural "cic:/CoRN/reals/Series/convergent_wd.con". +inline procedural "cic:/CoRN/reals/Series/convergent_wd.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/series_sum_wd.con". +inline procedural "cic:/CoRN/reals/Series/series_sum_wd.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/conv_series_plus.con". +inline procedural "cic:/CoRN/reals/Series/conv_series_plus.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/series_sum_plus.con". +inline procedural "cic:/CoRN/reals/Series/series_sum_plus.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/conv_series_minus.con". +inline procedural "cic:/CoRN/reals/Series/conv_series_minus.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/series_sum_minus.con". +inline procedural "cic:/CoRN/reals/Series/series_sum_minus.con" as lemma. (*#* Multiplication by a scalar [c] is also permitted. *) alias id "c" = "cic:/CoRN/reals/Series/Operations/c.var". -inline procedural "cic:/CoRN/reals/Series/conv_series_mult_scal.con". +inline procedural "cic:/CoRN/reals/Series/conv_series_mult_scal.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/series_sum_mult_scal.con". +inline procedural "cic:/CoRN/reals/Series/series_sum_mult_scal.con" as lemma. (* UNEXPORTED End Operations @@ -208,9 +208,9 @@ alias id "convX" = "cic:/CoRN/reals/Series/More_Operations/convX.var". (*#* As a corollary, we get the series of the inverses. *) -inline procedural "cic:/CoRN/reals/Series/conv_series_inv.con". +inline procedural "cic:/CoRN/reals/Series/conv_series_inv.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/series_sum_inv.con". +inline procedural "cic:/CoRN/reals/Series/series_sum_inv.con" as lemma. (* UNEXPORTED End More_Operations @@ -232,15 +232,15 @@ alias id "x" = "cic:/CoRN/reals/Series/Almost_Everywhere/x.var". alias id "y" = "cic:/CoRN/reals/Series/Almost_Everywhere/y.var". -inline procedural "cic:/CoRN/reals/Series/aew_eq.con". +inline procedural "cic:/CoRN/reals/Series/aew_eq.con" as definition. alias id "aew_equal" = "cic:/CoRN/reals/Series/Almost_Everywhere/aew_equal.var". -inline procedural "cic:/CoRN/reals/Series/aew_Cauchy.con". +inline procedural "cic:/CoRN/reals/Series/aew_Cauchy.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/aew_Cauchy2.con". +inline procedural "cic:/CoRN/reals/Series/aew_Cauchy2.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/aew_series_conv.con". +inline procedural "cic:/CoRN/reals/Series/aew_series_conv.con" as lemma. (* UNEXPORTED End Almost_Everywhere @@ -258,7 +258,7 @@ alias id "y" = "cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/y.var". alias id "aew_equal" = "cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/aew_equal.var". -inline procedural "cic:/CoRN/reals/Series/aew_Lim.con". +inline procedural "cic:/CoRN/reals/Series/aew_Lim.con" as lemma. (* UNEXPORTED End Cauchy_Almost_Everywhere @@ -280,21 +280,21 @@ alias id "x" = "cic:/CoRN/reals/Series/Convergence_Criteria/x.var". general (but simpler) form. *) -inline procedural "cic:/CoRN/reals/Series/str_comparison.con". +inline procedural "cic:/CoRN/reals/Series/str_comparison.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/comparison.con". +inline procedural "cic:/CoRN/reals/Series/comparison.con" as lemma. (*#* As a corollary, we get that every absolutely convergent series converges. *) -inline procedural "cic:/CoRN/reals/Series/abs_imp_conv.con". +inline procedural "cic:/CoRN/reals/Series/abs_imp_conv.con" as lemma. (*#* Next we have the ratio test, both as a positive and negative result. *) -inline procedural "cic:/CoRN/reals/Series/divergent_crit.con". +inline procedural "cic:/CoRN/reals/Series/divergent_crit.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/tail_series.con". +inline procedural "cic:/CoRN/reals/Series/tail_series.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/join_series.con". +inline procedural "cic:/CoRN/reals/Series/join_series.con" as lemma. (* UNEXPORTED End Convergence_Criteria @@ -306,9 +306,9 @@ Section More_CC alias id "x" = "cic:/CoRN/reals/Series/More_CC/x.var". -inline procedural "cic:/CoRN/reals/Series/ratio_test_conv.con". +inline procedural "cic:/CoRN/reals/Series/ratio_test_conv.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/ratio_test_div.con". +inline procedural "cic:/CoRN/reals/Series/ratio_test_div.con" as lemma. (* UNEXPORTED End More_CC @@ -334,19 +334,19 @@ alias id "mon_x" = "cic:/CoRN/reals/Series/Alternate_Series/mon_x.var". (* begin hide *) -inline procedural "cic:/CoRN/reals/Series/Alternate_Series/y.con" "Alternate_Series__". +inline procedural "cic:/CoRN/reals/Series/Alternate_Series/y.con" "Alternate_Series__" as definition. -inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma1.con" "Alternate_Series__". +inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma1.con" "Alternate_Series__" as definition. -inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma2.con" "Alternate_Series__". +inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma2.con" "Alternate_Series__" as definition. -inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma3.con" "Alternate_Series__". +inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma3.con" "Alternate_Series__" as definition. -inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma4.con" "Alternate_Series__". +inline procedural "cic:/CoRN/reals/Series/Alternate_Series/alternate_lemma4.con" "Alternate_Series__" as definition. (* end hide *) -inline procedural "cic:/CoRN/reals/Series/alternate_series_conv.con". +inline procedural "cic:/CoRN/reals/Series/alternate_series_conv.con" as lemma. (* UNEXPORTED End Alternate_Series @@ -362,17 +362,17 @@ We end this chapter by defining two important numbers in mathematics: [pi] and $e$#e#, both as sums of convergent series. *) -inline procedural "cic:/CoRN/reals/Series/e_series.con". +inline procedural "cic:/CoRN/reals/Series/e_series.con" as definition. -inline procedural "cic:/CoRN/reals/Series/e_series_conv.con". +inline procedural "cic:/CoRN/reals/Series/e_series_conv.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/E.con". +inline procedural "cic:/CoRN/reals/Series/E.con" as definition. -inline procedural "cic:/CoRN/reals/Series/pi_series.con". +inline procedural "cic:/CoRN/reals/Series/pi_series.con" as definition. -inline procedural "cic:/CoRN/reals/Series/pi_series_conv.con". +inline procedural "cic:/CoRN/reals/Series/pi_series_conv.con" as lemma. -inline procedural "cic:/CoRN/reals/Series/pi.con". +inline procedural "cic:/CoRN/reals/Series/pi.con" as definition. (* UNEXPORTED End Important_Numbers