%-------------------------------------------------------------------------
%
% Finite Measure Theory file.
%
%     Author: David Lester, Manchester University
%
%
%     Version 1.0           10/4/05
%-------------------------------------------------------------------------

finite_measure[T:TYPE,          (IMPORTING subset_algebra_def[T])
               S:sigma_algebra, (IMPORTING measure_def[T,S])
               mu:finite_measure]: THEORY

BEGIN

  IMPORTING sets_lemmas_aux,             % Proof only,     RWB: was sets_aux@
            sets_aux@indexed_sets_aux[nat,T],
            sigma_algebra[T,S],
            series@series_aux,               % Proof only
            structures@fun_preds_partial[nat,set[T],reals.<=,subset?[T]]

  X:   VAR [nat->(S)]
  A,B: VAR (S)

  fm_emptyset:      LEMMA mu(emptyset) = 0
  fm_convergence:   LEMMA disjoint?(X)
                               => convergence(series(mu o X), mu(IUnion(X)))
  fm_disjointunion: LEMMA disjoint?(A,B) => mu(union(A,B)) = mu(A) + mu(B)
  fm_complement:    LEMMA mu(complement(A)) = mu(fullset) - mu(A)
  fm_union:         LEMMA mu(union(A,B))
                                        = mu(A) + mu(B) - mu(intersection(A,B))
  fm_intersection:  LEMMA mu(intersection(A,B))
                                        = mu(A) + mu(B) - mu(union(A,B))
  fm_difference:    LEMMA mu(difference(A,B))
                                        = mu(A) - mu(B) + mu(difference(B,A))
  fm_subset:        LEMMA subset?(A,B)   => mu(B) = mu(A) + mu(difference(B,A))
  fm_subset_le:     LEMMA subset?(A,B)   => mu(A) <= mu(B)
  fm_monotone:      LEMMA subset?(A,B)   => mu(A) <= mu(B)              % 2.6.1
  fm_IUnion:        LEMMA increasing?(X) => convergence(mu o X, mu(IUnion(X)))
  fm_IIntersection: LEMMA decreasing?(X)
                               => convergence(mu o X, mu(IIntersection(X)))

  IMPORTING measure_def[T,S]

  measure_from:measure_type = lambda A: (TRUE,mu(A))

END finite_measure