Quelle  measure_contraction_props.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Measure Contraction Properties 
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Decomposition of an integral into a
%   sequence of integrals over measures contractions
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

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

BEGIN

  IMPORTING measure_props[T,S,mu],
            measure_contraction[T,S],
            integral_convergence_scaf % Proof only

  A: VAR disjoint_indexed_measurable
  h: VAR measurable_function
  x: VAR T
  n: VAR nat

  convergent?: MACRO pred[sequence[real]] = topological_convergence.convergent?

  contraction_integrable_def: LEMMA
    IUnion(A) = fullset[T] AND
    (FORALL x:  h(x) >= 0) =>
    (integrable?[T,S,mu](h) <=>
     ((FORALL n: integrable?[T,S,contraction(mu,A(n))](h)) AND
      convergent?(series(lambda n: integral[T,S,contraction(mu,A(n))](h)))))

END measure_contraction_props