power_series: THEORY
%----------------------------------------------------------------------------
%
% Definition of power series:
%
%               n
%           ----
%  powerseries(a)(x) =    \     a(k)*x^k
%           /
%           ----
%           k = 0
%
%               n
%           ----
%  powerseries(a,m)(x) =  \     a(k)*x^k
%           /
%           ----
%           k = m
%
%
% Author: Ricky W. Butler        10/2/00
%
% NOTES:
%  * powerseq is defined using IF-THEN-ELSE to avoid 0^0
%
%----------------------------------------------------------------------------
BEGIN
   
%   reals: LIBRARY "../reals"

   IMPORTING series, ints@factorial, reals@exponent_props

   x,r,y: VAR real
   c,px: VAR posreal
   x1,z: VAR nonzero_real
   n,m: VAR nat
   a: VAR sequence[real]
   S: VAR set[real]
   pn: VAR posnat

%   powerseq(a,x): sequence[real] = (LAMBDA (k: nat): a(k)*x^k)
%   rule out 0^0

   hat_02n: LEMMA 0^pn = 0


   AUTO_REWRITE+ expt_x0         % LEMMA x^0 = 1
   AUTO_REWRITE+ expt_x1         % LEMMA x^1 = x
   AUTO_REWRITE+ expt_1i         % LEMMA 1^i = 1
   AUTO_REWRITE+ hat_02n         % LEMMA 0^pn = 0

   powerseq(a,x): sequence[real] = (LAMBDA (k: nat): a(k)*x^k)


   powerseries(a)(x): sequence[real] = series(powerseq(a,x))

   powerseries(a,m)(x): sequence[real] = series(powerseq(a,x),m)

   absolutely_convergent_series?(a): boolean = convergent?(series(abs(a)))

   divergent_series?(a): boolean = NOT convergent?(series(a))


   powerseries_bounded: LEMMA convergent?(powerseries(a)(x)) IMPLIES
                                bounded?(powerseq(a, x))
                                



%  *** if convergent at one point x1, then abs convergent within (-x1,x1) ***
                                
   powerseries_conv_point: THEOREM convergent?(powerseries(a)(x1)) AND
                                 abs(x) < abs(x1)
                                    IMPLIES 
                          absolutely_convergent_series?(powerseq(a,x))

   powerseries_conv: COROLLARY convergent?(powerseries(a)(x)) AND
                                 abs(y) < abs(x)
                                    IMPLIES 
                               convergent?(powerseries(a)(y))


   powerseries_diverg: COROLLARY divergent_series?(powerseq(a,x1)) AND
                                 abs(x) > abs(x1)
                                    IMPLIES 
                          divergent_series?(powerseq(a,x))


   series_convergent_within(a,c): bool =
       (FORALL x: abs(x) < c IMPLIES convergent?(series(powerseq(a,x))))

   series_divergent_outside(a,c): bool =
       (FORALL x:  abs(x) > c IMPLIES divergent_series?(powerseq(a,x)))

   series_convergent_only_at_0(a): bool = 
       convergent?(series(powerseq(a,0))) AND
       (FORALL x:  x /= 0 IMPLIES divergent_series?(powerseq(a,x)))
 
%  ------ behavior of series at x = c or x = -c is not predictable ------


   zero_powerseries_conv: LEMMA convergent?(powerseries(a)(0))

   powerseries_three_cases: THEOREM
           (FORALL (x: real): convergent?(powerseries(a)(x))) OR
           (series_convergent_only_at_0(a)) OR
           (EXISTS (r: posreal): series_convergent_within(a,r) AND
                                 series_divergent_outside(a,r))

   interval(c): set[real] = {x: real | -c < x AND x < c}

   powerseries_conv_abs_intv: LEMMA 
         (FORALL (x: (interval(c))): convergent?(series(powerseq(a,x)))) 
    IMPLIES (FORALL (x: (interval(c))): convergent?(series(abs(powerseq(a,x)))))


%  ----- old form retained to preserve old proofs -----

   apowerseq(a,x): sequence[real] = (LAMBDA (k: nat): IF k = 0 THEN a(0)
                                                      ELSE a(k)*x^k
                                                      ENDIF)

   apow_rew: LEMMA powerseq(a,x) = apowerseq(a,x)

%  to fix old proofs replace (expand "powerseq")
%                    with    (rewrite "apow_rew") (expand "apowerseq")


END power_series