countable_convergence[T:TYPE]: THEORY
%------------------------------------------------------------------------------
% Convergence properties for countable sums.
%
%  MODIFICATIONS:
%
%     Author: David Lester, Manchester University 20/4/05
%
%------------------------------------------------------------------------------


BEGIN

  IMPORTING sets_aux@countable_props[T],
            denumerable_enumeration[T],
            finite_enumeration[T],
            sigma_bijection_nat, sigma_bijection,
            analysis@convergence_ops,
            reals@sigma,
            absconv_series_aux,
            series@series

  a:   VAR real
  X,Y: VAR countable_set[T]
  t:   VAR T
  f,g: VAR [T -> real]
  F:   VAR non_empty_finite_set[T]
  n:   VAR nat
  phi: VAR (bijective?[nat,nat])


  convergent?(X)(g): bool
    = is_finite(X) OR absconvergent?(g o denumerable_enumeration(X))

  convergent_zero:   LEMMA convergent?(X)(LAMBDA t: 0)

  convergent_plus:   LEMMA convergent?(X)(f) AND convergent?(X)(g) =>
                           convergent?(X)(f+g)

  convergent_scal:   LEMMA convergent?(X)(f) => convergent?(X)(a*f)

  convergent_opp:    LEMMA convergent?(X)(f) => convergent?(X)(-f)

  convergent_diff:   LEMMA convergent?(X)(f) AND convergent?(X)(g) =>
                           convergent?(X)(f-g)

  convergent_le:     LEMMA (FORALL t: abs(g(t)) <= abs(f(t))) AND
                           convergent?(X)(f) => convergent?(X)(g)

  convergent_zeros:  LEMMA (FORALL (t:(X)): g(t) = 0) => convergent?(X)(g)

  convergent_empty:  LEMMA convergent?(emptyset[T])(g)

  convergent_singleton: LEMMA convergent?(singleton(t))(g)

  convergent_subset: LEMMA subset?(X,Y) AND convergent?(Y)(g) =>
                           convergent?(X)(g)

  convergent_intersection: LEMMA
         convergent?(X)(g) OR convergent?(Y)(g) =>
                           convergent?(intersection(X,Y))(g)

  convergent_difference: LEMMA
         convergent?(X)(g) => convergent?(difference(X,Y))(g)

  convergent_disjoint_union: LEMMA
         disjoint?(X,Y) AND convergent?(X)(g) AND convergent?(Y)(g) =>
                            convergent?(union(X,Y))(g)

  convergent_union: LEMMA
         convergent?(X)(g) AND convergent?(Y)(g) =>
                           convergent?(union(X,Y))(g)

  convergent_add: LEMMA convergent?(X)(g) =>
                           convergent?(add(t,X))(g)

  convergent_remove: LEMMA convergent?(X)(g) =>
                           convergent?(remove(t,X))(g)

  convergent_abs: LEMMA convergent?(X)(g) IFF convergent?(X)(abs(g))

END countable_convergence