%-------------------------------------------------------------------------
% Measure Theory Definition file.
%
%     Author: David Lester, Manchester University
%
%  EXPORTS: finite_measure?
%
%     Version 1.0           10/04/05
%     Version 1.1           20/08/07 Extended to subset algebra (DRL)
%-------------------------------------------------------------------------

generalized_measure_def[T:TYPE,S:setofsets[T]]: THEORY

BEGIN

  ASSUMING

    S_empty:        ASSUMPTION S(emptyset)

  ENDASSUMING

  IMPORTING series@series,
            sets_aux@indexed_sets_aux[nat,T],
            sets_aux@nat_indexed_sets[T],
            metric_space@convergence_aux,
            extended_nnreal@extended_nnreal

%  limit: MACRO [(convergence_sequences.convergent?)->real]
%                                          = convergence_sequences.limit ;

  i,j,n: VAR nat
  f:     VAR [(S)->extended_nnreal]
  g:     VAR [(S)->nnreal]
  A:     VAR [nat->(S)]
  a,b:   VAR (S)
  x:     VAR set[T]

  disjoint_indexed_measurable?(A):bool = disjoint?(A)

  disjoint_indexed_measurable: TYPE+ = 
       (disjoint_indexed_measurable?) CONTAINING (LAMBDA i: emptyset[T])

  disjoint_indexed_measurable_is_disjoint_indexed_set: JUDGEMENT
       disjoint_indexed_measurable SUBTYPE_OF disjoint_indexed_set[nat,T]

  X:   VAR disjoint_indexed_measurable

  measure_empty?(f):bool
    = f(emptyset[T]) = (TRUE,0)

  measure_countably_additive?(f): bool
    = FORALL X: S(IUnion(X)) => x_eq(x_sum(f o X),f(IUnion(X)))

  measure_complete?(f):bool
    = (FORALL x,a: (subset?(x,a) AND f(a) = (TRUE,0)) => S(x))

  measure?(f):bool              = measure_empty?(f) AND
                                  measure_countably_additive?(f)
  complete_measure?(f):bool     = measure?(f) AND measure_complete?(f)

  zero_measure(a):extended_nnreal = (TRUE,0)

  measure_type:         TYPE+ = (measure?)              CONTAINING zero_measure

  trivial_measure:measure_type
   = lambda a: IF empty?(a) THEN (TRUE,0) ELSE (FALSE,0) ENDIF

  complete_measure: TYPE+ = (complete_measure?) CONTAINING trivial_measure

  complete_measure_is_measure:
                JUDGEMENT complete_measure     SUBTYPE_OF measure_type

  measure_disjoint_union: LEMMA
    measure?(f) AND disjoint?(a,b) AND S(union(a,b)) =>
                                          x_eq(f(union(a,b)),x_add(f(a),f(b)))

  finite_measure?(g):bool
    = g(emptyset[T]) = 0 AND
      FORALL X: S(IUnion(X)) => convergence(series(g o X),g(IUnion(X)))

  complete_finite_measure?(g):bool
    = finite_measure?(g) AND FORALL x,a: subset?(x,a) AND g(a) = 0 => S(x)

  trivial_finite_measure(A:(S)):[nnreal] = 0

  finite_measure:   TYPE+ = (finite_measure?) CONTAINING trivial_finite_measure
  complete_finite_measure: TYPE  = (complete_finite_measure?)

  complete_finite_measure_is_finite_measure:
                   JUDGEMENT complete_finite_measure SUBTYPE_OF finite_measure

  to_measure(m:finite_measure):measure_type = lambda a: (TRUE,m(a))

  F: VAR sequence[measure_type]

  x_sum_measure:   LEMMA measure?(lambda a: (x_sum(lambda i: F(i)(a))))

END generalized_measure_def