Quellcode-Bibliothek measure_props.pvs

%------------------------------------------------------------------------------
% Basic properties of measures
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

measure_props[T:TYPE,          (IMPORTING subset_algebra_def[T])
              S:sigma_algebra, (IMPORTING measure_def[T,S])
              m:measure_type]: THEORY

BEGIN

  IMPORTING measure_space_def[T,S],
            sigma_algebra[T,S],
            structures@fun_preds_partial[nat,set[T],reals.<=,subset?[T]],
            measure_def[T,S],
            series@series_aux

  n,i:   VAR nat
  a,b,M: VAR measurable_set
  x,y:   VAR extended_nnreal
  X:     VAR sequence[extended_nnreal]
  DX:    VAR disjoint_indexed_measurable
  E:     VAR sequence[measurable_set]

  mu_fin?(M):bool                   = m(M)`1
  mu(M:{m:(S) | mu_fin?(m)}):nnreal = m(M)`2

  m_emptyset:           LEMMA m(emptyset[T]) = (TRUE,0)
  m_countably_additive: LEMMA x_eq(x_sum(m o DX), m(IUnion(DX)))

  m_disjoint_union:LEMMA disjoint?(a,b) => x_eq(m(union(a,b)),x_add(m(a),m(b)))
  m_monotone:      LEMMA subset?(a,b) => x_le(m(a),m(b))                % 2.6.1
  m_union:         LEMMA x_le(m(union(a,b)),x_add(m(a),m(b)))

  m_increasing_convergence: LEMMA increasing?(E) =>                     % 2.6.2
                                  x_converges?(m o E, m(IUnion(E)))

  m_decreasing_convergence: LEMMA decreasing?(E) AND mu_fin?(E(0)) =>   % 2.6.3
                                  x_converges?(m o E, m(IIntersection(E)))
END measure_props