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

BEGIN

  IMPORTING series@series_aux,
            series@absconv_series,
            sets_aux@infinite_image,
            sets_aux@countable_props,
            sets_aux@countable_image,
            analysis@convergence_ops       % proof only

  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])

% Following should probably be in analysis@sequence_props.pvs:

  extract_bij:        LEMMA bijective?[nat,(image(f,fullset[nat]))](f)

  subseq_def:         LEMMA subseq(a,b) IFF EXISTS f: FORALL n: a(n) = b(f(n))


  S: VAR countably_infinite_set[nat]

  IMPORTING orders@integer_enumerations[nat]

  inj_is_bij_extract:      LEMMA EXISTS phi,f: inj = phi o f

  nonneg_series_inj_conv:  LEMMA convergent?(series(nna)) =>
                                 convergent?(series(nna o inj))

  nonneg_series_inj_limit: LEMMA convergent?(series(nna)) =>
                                 limit(series(nna)) >= limit(series(nna o inj))

% Any absolutely convergent series can be arbitrarily rearranged omitting
% terms.

  aa: VAR absconvergent_series

  abs_series_inj_conv: LEMMA convergent?(series(aa o inj))

END absconv_series_aux