...

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / reals / Series.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/reals/Series.mma b/helm/software/matita/contribs/CoRN-Procedural/reals/Series.mma
index 9a898a409859de5e0d5aecb20e770cdec0afc3e6..80e034a8d8e5263fe4ba32e74b54c951e00e0460 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/reals/Series.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/reals/Series.mma
@@ -43,9 +43,11 @@ To each such sequence we can assign a sequence of partial sums.
 %\end{convention}%
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/Definitions/x.var".
+(* UNEXPORTED
+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 +55,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 +71,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
@@ -97,11 +99,13 @@ End Definitions
 Section More_Definitions
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/More_Definitions/x.var".
+(* UNEXPORTED
+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 +120,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
@@ -127,19 +131,25 @@ we can also compute its sum.
 %\end{convention}%
 *)
 
-alias id "c" = "cic:/CoRN/reals/Series/Power_Series/c.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Power_Series/c.var
+*)
 
-alias id "H0c" = "cic:/CoRN/reals/Series/Power_Series/H0c.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Power_Series/H0c.var
+*)
 
-alias id "Hc1" = "cic:/CoRN/reals/Series/Power_Series/Hc1.var".
+(* UNEXPORTED
+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 +165,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.
@@ -166,33 +176,43 @@ of two convergent series.
 %\end{convention}%
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/Operations/x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Operations/x.var
+*)
 
-alias id "y" = "cic:/CoRN/reals/Series/Operations/y.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Operations/y.var
+*)
 
-alias id "convX" = "cic:/CoRN/reals/Series/Operations/convX.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Operations/convX.var
+*)
 
-alias id "convY" = "cic:/CoRN/reals/Series/Operations/convY.var".
+(* UNEXPORTED
+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".
+(* UNEXPORTED
+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
@@ -202,15 +222,19 @@ End Operations
 Section More_Operations
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/More_Operations/x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/More_Operations/x.var
+*)
 
-alias id "convX" = "cic:/CoRN/reals/Series/More_Operations/convX.var".
+(* UNEXPORTED
+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
@@ -228,19 +252,25 @@ and derive an important corollary for series.
 Let [x,y : nat->IR] be equal after some natural number.
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/Almost_Everywhere/x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Almost_Everywhere/x.var
+*)
 
-alias id "y" = "cic:/CoRN/reals/Series/Almost_Everywhere/y.var".
+(* UNEXPORTED
+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".
+(* UNEXPORTED
+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
@@ -252,13 +282,19 @@ Section Cauchy_Almost_Everywhere
 
 (*#* Suppose furthermore that [x,y] are Cauchy sequences. *)
 
-alias id "x" = "cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/x.var
+*)
 
-alias id "y" = "cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/y.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/y.var
+*)
 
-alias id "aew_equal" = "cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/aew_equal.var".
+(* UNEXPORTED
+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
@@ -274,27 +310,29 @@ Section Convergence_Criteria
 %\end{convention}%
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/Convergence_Criteria/x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Convergence_Criteria/x.var
+*)
 
 (*#* We include the comparison test for series, both in a strong and in a less 
 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
@@ -304,11 +342,13 @@ End Convergence_Criteria
 Section More_CC
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/More_CC/x.var".
+(* UNEXPORTED
+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
@@ -324,29 +364,37 @@ Alternate series are a special case.  Suppose that [x] is nonnegative and
 decreasing convergent to 0.
 *)
 
-alias id "x" = "cic:/CoRN/reals/Series/Alternate_Series/x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Alternate_Series/x.var
+*)
 
-alias id "pos_x" = "cic:/CoRN/reals/Series/Alternate_Series/pos_x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Alternate_Series/pos_x.var
+*)
 
-alias id "Lim_x" = "cic:/CoRN/reals/Series/Alternate_Series/Lim_x.var".
+(* UNEXPORTED
+cic:/CoRN/reals/Series/Alternate_Series/Lim_x.var
+*)
 
-alias id "mon_x" = "cic:/CoRN/reals/Series/Alternate_Series/mon_x.var".
+(* UNEXPORTED
+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 +410,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