Quelle  measure_completion_aux.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Auxilliary results to complete a measure 
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Note: not described in Berberian 
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

measure_completion_aux[T:TYPE]: THEORY

BEGIN

  IMPORTING subset_algebra_def[T],
            measure_def,
            measure_theory,
            measure_props

  XS: VAR setofsets[T]
  A,B,X:  VAR set[T]
  z:  VAR extended_nnreal

  almost_measurable?(S:sigma_algebra[T],m:measure_type[T,S])(X):bool
    = EXISTS (Y:(S),N1,N2:negligible[T,S,m]): X = difference(union(Y,N1),N2)

  empty_almost_measurable: LEMMA
    FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
      almost_measurable?(S,m)(emptyset[T])

  complement_almost_measurable: LEMMA
    FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
      almost_measurable?(S,m)(X) <=> almost_measurable?(S,m)(complement(X))

  Union_almost_measurable: LEMMA
    FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
      every(almost_measurable?(S,m),XS) AND is_countable(XS) =>
            almost_measurable?(S,m)(Union(XS))

  completion(S:sigma_algebra[T],m:measure_type[T,S]):sigma_algebra[T]
    = {X | almost_measurable?(S,m)(X)}

  generated_completion: LEMMA FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
    generated_sigma_algebra(union(S,fullset[negligible[T,S,m]]))
      = completion(S,m)

  completion_extends: LEMMA FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
                            S(X) => completion(S,m)(X)

  negligible_completion: LEMMA FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
                            negligible_set?[T,S,m](X) => completion(S,m)(X)

  is_completion(S:sigma_algebra[T],m:measure_type[T,S])(A,B):bool
    = completion(S,m)(A) AND S(B) =>
      EXISTS (N1,N2:negligible[T,S,m]): A = difference(union(B,N1),N2)

  m_completions: LEMMA FORALL (S:sigma_algebra[T],m:measure_type[T,S],X,A,B):
                       completion(S,m)(X) AND S(A) AND S(B) AND
                       is_completion(S,m)(X,A) AND  is_completion(S,m)(X,B) =>
                       x_eq(m(A),m(B))

  choose_completion: LEMMA FORALL (S:sigma_algebra[T],m:measure_type[T,S],X):
                       completion(S,m)(X) => 
         is_completion(S,m)(X,choose({Y:(S) | EXISTS (N1,N2:negligible[T,S,m]):
                 X = difference(union(Y,N1),N2)}))

  completion(S:sigma_algebra[T],m:measure_type[T,S]):
                                            complete_measure[T,completion(S,m)]
    = lambda (X:(completion(S,m))):
        m(choose({Y:(S) | EXISTS (N1,N2:negligible[T,S,m]):
                 X = difference(union(Y,N1),N2)}))

  completion_measurable: LEMMA
    FORALL (S:sigma_algebra[T],m:measure_type[T,S],X:(S)):
           x_eq(completion(S,m)(X),m(X))

  completion_negligible: LEMMA
    FORALL (S:sigma_algebra[T],m:measure_type[T,S],N:negligible[T,S,m]):
           completion(S,m)(N) = (TRUE,0)

END measure_completion_aux