%----------------------------------------------------------------------------
%
% Absolutely Convergent Series
%
% Author: David Lester (Manchester University)          22/04/05
% 
%----------------------------------------------------------------------------
absconv_series: THEORY

BEGIN

  IMPORTING series_lems

  n,m:     VAR nat
  x:       VAR real
  nnx,nny: VAR nnreal
  f:       VAR extraction
  a,b:     VAR sequence[real]
  nna,nnb: VAR sequence[nnreal]
  phi:     VAR (bijective?[nat,nat])
  inj:     VAR (injective?[nat,nat])

  Convergent_Series: TYPE+ = {s: sequence[real] | convergent?(series(s))}
                             CONTAINING (LAMBDA n: 0)

  absconvergent?(a):bool = convergent?(series(abs(a)))

  absconvergent_series: TYPE+ = (absconvergent?)

  absconvergent_series_is_convergent:
        JUDGEMENT absconvergent_series SUBTYPE_OF Convergent_Series

  aa,bb: VAR absconvergent_series

  abs_series_bij_abs: LEMMA
         convergence(series(aa o phi),x) IFF convergence(series(aa),x)

  abs_series_bij_conv_abs: LEMMA
         convergent?(series(aa o phi)) IFF convergent?(series(aa))

  abs_series_bij_limit_abs: LEMMA
         limit(series(aa o phi)) = limit(series(aa))


% extractions of sequences ...

  extract_convergent: LEMMA convergent?(series(a)) => convergent?(series(a) o f)

  extract_comp: LEMMA series(a o f)
        = series(lambda n: IF (EXISTS m: n = f(m)) THEN a(n) ELSE 0 ENDIF) o f

  subseq_absconvergent: LEMMA subseq(a,bb) => absconvergent?(a)

  nonneg_subseq:      LEMMA subseq(nna,nnb) AND convergence(series(nnb),nny) =>
                            EXISTS nnx:
                                convergence(series(nna),nnx) AND nnx <= nny


  sum_absconvergent:  LEMMA absconvergent?(aa+bb)
 
  opp_absconvergent:  LEMMA absconvergent?(-aa)

  diff_absconvergent: LEMMA absconvergent?(aa-bb)

  scal_absconvergent: LEMMA absconvergent?(x*aa)


END absconv_series