(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

(* This file was automatically generated: do not edit *********************)

include "CoRN.ma".

(* $Id: Series.v,v 1.6 2004/04/23 10:01:05 lcf Exp $ *)

(*#* printing seq_part_sum %\ensuremath{\sum^n}% #&sum;<sup>n</sup># *)

(*#* printing series_sum %\ensuremath{\sum_0^{\infty}}% #&sum;<sub>0</sub><sup>&infin;</sup># *)

(*#* printing pi %\ensuremath{\pi}% #&pi; *)

include "reals/CSumsReals.ma".

include "reals/NRootIR.ma".

(* UNEXPORTED
Section Definitions
*)

(*#* *Series of Real Numbers
In this file we develop a theory of series of real numbers.
** Definitions

A series is simply a sequence from the natural numbers into the reals.  
To each such sequence we can assign a sequence of partial sums.

%\begin{convention}% Let [x:nat->IR].
%\end{convention}%
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/Definitions/x.var
*)

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
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" 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" as definition.

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 
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" as definition.

inline procedural "cic:/CoRN/reals/Series/divergent.con" as definition.

inline procedural "cic:/CoRN/reals/Series/conv_imp_not_div.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/div_imp_not_conv.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/convergent_imp_not_divergent.con" as lemma.

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" as lemma.

inline procedural "cic:/CoRN/reals/Series/series_seq_Lim'.con" as lemma.

(* UNEXPORTED
End Definitions
*)

(* UNEXPORTED
Section More_Definitions
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/More_Definitions/x.var
*)

(*#* We also define absolute convergence. *)

inline procedural "cic:/CoRN/reals/Series/abs_convergent.con" as definition.

(* UNEXPORTED
End More_Definitions
*)

(* UNEXPORTED
Section Power_Series
*)

(*#* **Power Series

Power series are an important special case.
*)

inline procedural "cic:/CoRN/reals/Series/power_series.con" as definition.

(*#*
Specially important is the case when [c] is a positive real number
less than 1; in this case not only the power series is convergent, but
we can also compute its sum.

%\begin{convention}% Let [c] be a real number between 0 and 1.
%\end{convention}%
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/Power_Series/c.var
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/Power_Series/H0c.var
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/Power_Series/Hc1.var
*)

inline procedural "cic:/CoRN/reals/Series/c_exp_Lim.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/power_series_Lim1.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/power_series_conv.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/power_series_sum.con" as lemma.

(* UNEXPORTED
End Power_Series
*)

(* UNEXPORTED
Section Operations
*)

(*#* **Operations

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" as lemma.

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.

%\begin{convention}% Let [x,y:nat->IR] be convergent series.
%\end{convention}%
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/Operations/x.var
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/Operations/y.var
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/Operations/convX.var
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/Operations/convY.var
*)

inline procedural "cic:/CoRN/reals/Series/convergent_wd.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/series_sum_wd.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/conv_series_plus.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/series_sum_plus.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/conv_series_minus.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/series_sum_minus.con" as lemma.

(*#* Multiplication by a scalar [c] is also permitted. *)

(* UNEXPORTED
cic:/CoRN/reals/Series/Operations/c.var
*)

inline procedural "cic:/CoRN/reals/Series/conv_series_mult_scal.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/series_sum_mult_scal.con" as lemma.

(* UNEXPORTED
End Operations
*)

(* UNEXPORTED
Section More_Operations
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/More_Operations/x.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" as lemma.

inline procedural "cic:/CoRN/reals/Series/series_sum_inv.con" as lemma.

(* UNEXPORTED
End More_Operations
*)

(* UNEXPORTED
Section Almost_Everywhere
*)

(*#* ** Almost Everywhere

In this section we strengthen some of the convergence results for sequences 
and derive an important corollary for series.

Let [x,y : nat->IR] be equal after some natural number.
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/Almost_Everywhere/x.var
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/Almost_Everywhere/y.var
*)

inline procedural "cic:/CoRN/reals/Series/aew_eq.con" as definition.

(* UNEXPORTED
cic:/CoRN/reals/Series/Almost_Everywhere/aew_equal.var
*)

inline procedural "cic:/CoRN/reals/Series/aew_Cauchy.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/aew_Cauchy2.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/aew_series_conv.con" as lemma.

(* UNEXPORTED
End Almost_Everywhere
*)

(* UNEXPORTED
Section Cauchy_Almost_Everywhere
*)

(*#* Suppose furthermore that [x,y] are Cauchy sequences. *)

(* UNEXPORTED
cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/x.var
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/y.var
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/Cauchy_Almost_Everywhere/aew_equal.var
*)

inline procedural "cic:/CoRN/reals/Series/aew_Lim.con" as lemma.

(* UNEXPORTED
End Cauchy_Almost_Everywhere
*)

(* UNEXPORTED
Section Convergence_Criteria
*)

(*#* **Convergence Criteria

%\begin{convention}% Let [x:nat->IR].
%\end{convention}%
*)

(* 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" as lemma.

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" as lemma.

(*#* Next we have the ratio test, both as a positive and negative result. *)

inline procedural "cic:/CoRN/reals/Series/divergent_crit.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/tail_series.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/join_series.con" as lemma.

(* UNEXPORTED
End Convergence_Criteria
*)

(* UNEXPORTED
Section More_CC
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/More_CC/x.var
*)

inline procedural "cic:/CoRN/reals/Series/ratio_test_conv.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/ratio_test_div.con" as lemma.

(* UNEXPORTED
End More_CC
*)

(* UNEXPORTED
Section Alternate_Series
*)

(*#* **Alternate Series

Alternate series are a special case.  Suppose that [x] is nonnegative and 
decreasing convergent to 0.
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/Alternate_Series/x.var
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/Alternate_Series/pos_x.var
*)

(* UNEXPORTED
cic:/CoRN/reals/Series/Alternate_Series/Lim_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__" as definition.

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__" as definition.

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__" as definition.

(* end hide *)

inline procedural "cic:/CoRN/reals/Series/alternate_series_conv.con" as lemma.

(* UNEXPORTED
End Alternate_Series
*)

(* UNEXPORTED
Section Important_Numbers
*)

(*#* **Important Numbers

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" as definition.

inline procedural "cic:/CoRN/reals/Series/e_series_conv.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/E.con" as definition.

inline procedural "cic:/CoRN/reals/Series/pi_series.con" as definition.

inline procedural "cic:/CoRN/reals/Series/pi_series_conv.con" as lemma.

inline procedural "cic:/CoRN/reals/Series/pi.con" as definition.

(* UNEXPORTED
End Important_Numbers
*)