set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreFunSeries".
+include "CoRN.ma".
+
(* $Id: MoreFunSeries.v,v 1.4 2004/04/23 10:00:59 lcf Exp $ *)
-(* INCLUDE
-FunctSeries
-*)
+include "ftc/FunctSeries.ma".
-(* INCLUDE
-MoreFunctions
-*)
+include "ftc/MoreFunctions.ma".
(*#* printing FSeries_Sum %\ensuremath{\sum_{\infty}}% #∑'<sub>∞</sub># *)
(* UNEXPORTED
-Section Definitions.
+Section Definitions
*)
(*#* *More on Sequences and Series
but the ones which do we simply adapt in the usual way.
*)
-inline cic:/CoRN/ftc/MoreFunSeries/J.var.
+alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/J.var".
-inline cic:/CoRN/ftc/MoreFunSeries/f.var.
+alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/f.var".
-inline cic:/CoRN/ftc/MoreFunSeries/F.var.
+alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/F.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contf.var.
+alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/contf.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contF.var.
+alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/contF.var".
-inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_IR.con".
(*#*
The equivalences between these definitions still hold.
*)
-inline cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq'_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq'_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_seq2_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_seq2_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_seq_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_seq_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_real_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_real_IR.con".
(* UNEXPORTED
-End Definitions.
+End Definitions
*)
(* UNEXPORTED
-Section More_Definitions.
+Section More_Definitions
*)
(*#*
Limit is defined and works in the same way as before.
*)
-inline cic:/CoRN/ftc/MoreFunSeries/J.var.
+alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/J.var".
-inline cic:/CoRN/ftc/MoreFunSeries/f.var.
+alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/f.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contf.var.
+alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/contf.var".
(* begin show *)
-inline cic:/CoRN/ftc/MoreFunSeries/conv.var.
+alias id "conv" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/conv.var".
(* end show *)
-inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_char.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_char.con".
(* UNEXPORTED
-End More_Definitions.
+End More_Definitions
*)
(* UNEXPORTED
-Section Irrelevance_of_Proofs.
+Section Irrelevance_of_Proofs
*)
(*#* ***Basic Properties
Proofs are irrelevant as before---they just have to be present.
*)
-inline cic:/CoRN/ftc/MoreFunSeries/J.var.
+alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/J.var".
-inline cic:/CoRN/ftc/MoreFunSeries/f.var.
+alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/f.var".
(* begin show *)
-inline cic:/CoRN/ftc/MoreFunSeries/contf.var.
+alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contf.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contf0.var.
+alias id "contf0" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contf0.var".
(* end show *)
-inline cic:/CoRN/ftc/MoreFunSeries/F.var.
+alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/F.var".
(* begin show *)
-inline cic:/CoRN/ftc/MoreFunSeries/contF.var.
+alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contF.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contF0.var.
+alias id "contF0" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contF0.var".
(* end show *)
-inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wd_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wd_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_wd_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_wd_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_wd_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_wd_IR.con".
(* UNEXPORTED
-End Irrelevance_of_Proofs.
+End Irrelevance_of_Proofs
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section More_Properties.
+Section More_Properties
*)
-inline cic:/CoRN/ftc/MoreFunSeries/J.var.
+alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/J.var".
-inline cic:/CoRN/ftc/MoreFunSeries/f.var.
+alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/f.var".
-inline cic:/CoRN/ftc/MoreFunSeries/g.var.
+alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/g.var".
(* begin show *)
-inline cic:/CoRN/ftc/MoreFunSeries/contf.var.
+alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contf.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contf0.var.
+alias id "contf0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contf0.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contg.var.
+alias id "contg" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contg.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contg0.var.
+alias id "contg0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contg0.var".
(* end show *)
-inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq'_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq'_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/F.var.
+alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/F.var".
-inline cic:/CoRN/ftc/MoreFunSeries/G.var.
+alias id "G" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/G.var".
(* begin show *)
-inline cic:/CoRN/ftc/MoreFunSeries/contF.var.
+alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contF.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contF0.var.
+alias id "contF0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contF0.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contG.var.
+alias id "contG" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contG.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contG0.var.
+alias id "contG0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contG0.var".
(* end show *)
-inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl'_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl'_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr'_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr'_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_cont_Lim_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_cont_Lim_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq_IR.con".
(* UNEXPORTED
-End More_Properties.
+End More_Properties
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Algebraic_Properties.
+Section Algebraic_Properties
*)
(*#* ***Algebraic Properties
Algebraic operations still work well.
*)
-inline cic:/CoRN/ftc/MoreFunSeries/J.var.
+alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/J.var".
-inline cic:/CoRN/ftc/MoreFunSeries/f.var.
+alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/f.var".
-inline cic:/CoRN/ftc/MoreFunSeries/g.var.
+alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/g.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contf.var.
+alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contf.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contg.var.
+alias id "contg" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contg.var".
-inline cic:/CoRN/ftc/MoreFunSeries/FLim_unique_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/FLim_unique_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_wd_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_wd_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_const_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_const_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_const_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_const_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/F.var.
+alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/F.var".
-inline cic:/CoRN/ftc/MoreFunSeries/G.var.
+alias id "G" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/G.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contF.var.
+alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contF.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contG.var.
+alias id "contG" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contG.var".
(* begin show *)
-inline cic:/CoRN/ftc/MoreFunSeries/convF.var.
+alias id "convF" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/convF.var".
-inline cic:/CoRN/ftc/MoreFunSeries/convG.var.
+alias id "convG" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/convG.var".
(* end show *)
-inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus'_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus'_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus'_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus'_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult'_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult'_IR.con".
(* UNEXPORTED
-End Algebraic_Properties.
+End Algebraic_Properties
*)
(* UNEXPORTED
-Section More_Algebraic_Properties.
+Section More_Algebraic_Properties
*)
(*#*
If we work with the limit function things fit in just as well.
*)
-inline cic:/CoRN/ftc/MoreFunSeries/J.var.
+alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/J.var".
-inline cic:/CoRN/ftc/MoreFunSeries/f.var.
+alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/f.var".
-inline cic:/CoRN/ftc/MoreFunSeries/g.var.
+alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/g.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contf.var.
+alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/contf.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contg.var.
+alias id "contg" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/contg.var".
(* begin show *)
-inline cic:/CoRN/ftc/MoreFunSeries/Hf.var.
+alias id "Hf" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/Hf.var".
-inline cic:/CoRN/ftc/MoreFunSeries/Hg.var.
+alias id "Hg" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/Hg.var".
(* end show *)
-inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_plus.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_plus.con".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_inv_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_inv_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_inv.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_inv.con".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_minus.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_minus.con".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_mult.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_mult.con".
(* UNEXPORTED
-End More_Algebraic_Properties.
+End More_Algebraic_Properties
*)
(* UNEXPORTED
-Section Other.
+Section Other
*)
(*#* ***Miscellaneous
Finally, we define a mapping between sequences of real numbers and sequences of (constant) functions and prove that convergence is preserved.
*)
-inline cic:/CoRN/ftc/MoreFunSeries/seq_to_funseq.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/seq_to_funseq.con".
-inline cic:/CoRN/ftc/MoreFunSeries/funseq_conv.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/funseq_conv.con".
(*#*
Another interesting fact: if a sequence of constant functions converges then it must converge to a constant function.
*)
-inline cic:/CoRN/ftc/MoreFunSeries/fun_const_Lim.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_const_Lim.con".
(* UNEXPORTED
-End Other.
+End Other
*)
(* UNEXPORTED
-Section Series_Definitions.
+Section Series_Definitions
*)
(*#* **Series
Convergence is defined as expected---through convergence in every compact interval.
*)
-inline cic:/CoRN/ftc/MoreFunSeries/J.var.
+alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/J.var".
-inline cic:/CoRN/ftc/MoreFunSeries/f.var.
+alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/f.var".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_series_conv_imp_conv_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_conv_imp_conv_IR.con".
(* begin show *)
-inline cic:/CoRN/ftc/MoreFunSeries/H.var.
+alias id "H" = "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/H.var".
(* end show *)
-inline cic:/CoRN/ftc/MoreFunSeries/fun_series_inc_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_inc_IR.con".
(*#* Assume [h(x)] is the pointwise series of [f(x)] *)
(* begin hide *)
-inline cic:/CoRN/ftc/MoreFunSeries/h.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/h.con" "Series_Definitions__".
(* end hide *)
-inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_strext_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_strext_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum.con".
-inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_char.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_char.con".
(* UNEXPORTED
-End Series_Definitions.
+End Series_Definitions
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section More_Series_Definitions.
+Section More_Series_Definitions
*)
-inline cic:/CoRN/ftc/MoreFunSeries/J.var.
+alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Series_Definitions/J.var".
-inline cic:/CoRN/ftc/MoreFunSeries/f.var.
+alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Series_Definitions/f.var".
(*#*
Absolute convergence still exists.
*)
-inline cic:/CoRN/ftc/MoreFunSeries/fun_series_abs_convergent_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_abs_convergent_IR.con".
(* UNEXPORTED
-End More_Series_Definitions.
+End More_Series_Definitions
*)
(* UNEXPORTED
-Section Convergence_Results.
+Section Convergence_Results
*)
(*#*
As before, any series converges to its sum.
*)
-inline cic:/CoRN/ftc/MoreFunSeries/J.var.
+alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Results/J.var".
-inline cic:/CoRN/ftc/MoreFunSeries/f.var.
+alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Results/f.var".
-inline cic:/CoRN/ftc/MoreFunSeries/FSeries_conv.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_conv.con".
-inline cic:/CoRN/ftc/MoreFunSeries/convergent_imp_inc.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/convergent_imp_inc.con".
-inline cic:/CoRN/ftc/MoreFunSeries/convergent_imp_Continuous.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/convergent_imp_Continuous.con".
-inline cic:/CoRN/ftc/MoreFunSeries/Continuous_FSeries_Sum.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/Continuous_FSeries_Sum.con".
(* UNEXPORTED
-End Convergence_Results.
+End Convergence_Results
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Operations.
+Section Operations
*)
(*#* **Algebraic Operations
Convergence is well defined and preserved by operations.
*)
-inline cic:/CoRN/ftc/MoreFunSeries/J.var.
+alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Operations/J.var".
-inline cic:/CoRN/ftc/MoreFunSeries/conv_fun_const_series_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/conv_fun_const_series_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_const_series_Sum_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_const_series_Sum_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/conv_zero_fun_series_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/conv_zero_fun_series_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_zero_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_zero_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/f.var.
+alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Operations/f.var".
-inline cic:/CoRN/ftc/MoreFunSeries/g.var.
+alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/Operations/g.var".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_wd_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_wd_IR.con".
(* begin show *)
-inline cic:/CoRN/ftc/MoreFunSeries/convF.var.
+alias id "convF" = "cic:/CoRN/ftc/MoreFunSeries/Operations/convF.var".
-inline cic:/CoRN/ftc/MoreFunSeries/convG.var.
+alias id "convG" = "cic:/CoRN/ftc/MoreFunSeries/Operations/convG.var".
(* end show *)
-inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_wd'.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_wd'.con".
-inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus_conv.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus_conv.con".
-inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus.con".
-inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv_conv.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv_conv.con".
-inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv.con".
-inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus_conv.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus_conv.con".
-inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus.con".
(*#*
%\begin{convention}% Let [c:IR] and [H:PartIR] be continuous in [J].
%\end{convention}%
*)
-inline cic:/CoRN/ftc/MoreFunSeries/c.var.
+alias id "c" = "cic:/CoRN/ftc/MoreFunSeries/Operations/c.var".
-inline cic:/CoRN/ftc/MoreFunSeries/H.var.
+alias id "H" = "cic:/CoRN/ftc/MoreFunSeries/Operations/H.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contH.var.
+alias id "contH" = "cic:/CoRN/ftc/MoreFunSeries/Operations/contH.var".
-inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal_conv.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal_conv.con".
-inline cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal.con".
(* UNEXPORTED
-End Operations.
+End Operations
*)
(* UNEXPORTED
-Section Convergence_Criteria.
+Section Convergence_Criteria
*)
(*#* ***Convergence Criteria
comparison test (in both versions) and the ratio test.
*)
-inline cic:/CoRN/ftc/MoreFunSeries/J.var.
+alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Criteria/J.var".
-inline cic:/CoRN/ftc/MoreFunSeries/f.var.
+alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Criteria/f.var".
-inline cic:/CoRN/ftc/MoreFunSeries/contF.var.
+alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Criteria/contF.var".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_str_comparison_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_str_comparison_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_comparison_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_comparison_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/abs_imp_conv_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/abs_imp_conv_IR.con".
-inline cic:/CoRN/ftc/MoreFunSeries/fun_ratio_test_conv_IR.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/fun_ratio_test_conv_IR.con".
(* UNEXPORTED
-End Convergence_Criteria.
+End Convergence_Criteria
*)
(* UNEXPORTED
-Section Insert_Series.
+Section Insert_Series
*)
(*#* ***Translation
position. This does not affect convergence or the sum of the series.
*)
-inline cic:/CoRN/ftc/MoreFunSeries/J.var.
+alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Insert_Series/J.var".
-inline cic:/CoRN/ftc/MoreFunSeries/f.var.
+alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Insert_Series/f.var".
-inline cic:/CoRN/ftc/MoreFunSeries/convF.var.
+alias id "convF" = "cic:/CoRN/ftc/MoreFunSeries/Insert_Series/convF.var".
-inline cic:/CoRN/ftc/MoreFunSeries/insert_series.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/insert_series.con".
-inline cic:/CoRN/ftc/MoreFunSeries/insert_series_cont.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/insert_series_cont.con".
-inline cic:/CoRN/ftc/MoreFunSeries/insert_series_sum_char.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/insert_series_sum_char.con".
-inline cic:/CoRN/ftc/MoreFunSeries/insert_series_conv.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/insert_series_conv.con".
-inline cic:/CoRN/ftc/MoreFunSeries/insert_series_sum.con.
+inline "cic:/CoRN/ftc/MoreFunSeries/insert_series_sum.con".
(* UNEXPORTED
-End Insert_Series.
+End Insert_Series
*)