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
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
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
(*#* 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
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
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
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.
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
(*#* 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
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
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
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
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
(* 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
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