Quelle  ast_def.pvs

%-------------------------------------------------------------------------
% Extension of a measure to and outer measure
%
%     Author: David Lester, Manchester University
%
%     Version 1.0           20/08/07 Initial (DRL)
%     Version 1.1           29/07/09    Now suitable for interval measures
%                                       (DRL)
%-------------------------------------------------------------------------
ast_def[T:TYPE,A:(nonempty?[set[T]])]: THEORY

BEGIN

  ASSUMING IMPORTING subset_algebra_def[T]

    A_empty:        ASSUMPTION A(emptyset)
    A_fullset:      ASSUMPTION A(fullset)
    A_intersection: ASSUMPTION FORALL (a,b:(A)): A(intersection(a,b))
    A_difference:   ASSUMPTION FORALL (a,b:(A)):
                               finite_disjoint_union?(A)(difference(a,b))

  ENDASSUMING

  IMPORTING generalized_measure_def[T,A],
            outer_measure_def[T],
            extended_nnreal@double_index[set[T]] % Proof Only

  mu: VAR measure_type
  z:  VAR extended_nnreal
  epsilon: VAR posreal
  X:  VAR set[T]
  Y:  VAR (A)
  I:  VAR sequence[(A)]
  a,b: VAR set[T]
  i,n:  VAR nat

  A_difference_union:  LEMMA A(a) AND finite_disjoint_union?(A)(b) =>
                             finite_disjoint_union?(A)(difference(a,b))

  measure_subadditive: LEMMA A(IUnion(I)) => x_le(mu(IUnion(I)), x_sum(mu o I))

  generalized_monotonicity: LEMMA 
    disjoint?(I)           AND
    subset?(IUnion(n,I),Y) AND
    (FORALL i: i >= n => empty?(I(i))) =>
    x_le(x_sum(mu o I),mu(Y))

  generalized_measure_monotone: LEMMA FORALL (a,b:(A),mu): subset?(a,b)  =>
                                                           x_le(mu(a),mu(b))

  ast(mu):outer_measure = lambda X:                                     % 7.1.3
    x_inf({z | EXISTS I: x_eq(x_sum(mu o I),z) AND subset?(X,IUnion(I))})

  outer_measure_eq: LEMMA x_eq(ast(mu)(Y),mu(Y))                        % 7.1.3

  outer_measure_def: LEMMA
    EXISTS I: subset?(X,IUnion(I)) AND
              x_le(x_sum(mu o I),x_add(ast(mu)(X),epsilon))

END ast_def