Quelle  fubini_tonelli.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Fubini-Tonelli Theorems
%
%     Author: David Lester, Manchester University, NIA, Universite Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
%     Version 1.0            5/06/09  Initial Version
%------------------------------------------------------------------------------

fubini_tonelli[(IMPORTING subset_algebra_def, measure_def)
       T1,T2: TYPE,
       S1:sigma_algebra[T1],S2:sigma_algebra[T2],
       mu:sigma_finite_measure[T1,S1],
       nu:sigma_finite_measure[T2,S2]]: THEORY

BEGIN

  IMPORTING product_measure[T1,T2,S1,S2],
            integral[[T1,T2],sigma_times(S1,S2),m_times(mu,nu)]            

  g: VAR nn_integrable
  h: VAR nn_measurable[[T1,T2],sigma_times(S1,S2)]
  x: VAR T1
  y: VAR T2

  IMPORTING product_integral_def[T1,T2,S1,S2,mu,nu],
            fubini_tonelli_scaf[T1,T2,S1,S2,mu,nu]

  fubini_tonelli_1: THEOREM integrable?(h) <=> integrable1?(h)          % 7.4.7

  fubini_tonelli_2: THEOREM integrable?(h) <=> integrable2?(h)          % 7.4.7

  fubini_tonelli_3: THEOREM                                             % 7.4.7
     integral(g) = integral(integral1[T1,T2,S1,S2,mu,nu](g))

  fubini_tonelli_4: THEOREM                                             % 7.4.7
     integral(g) = integral(integral2[T1,T2,S1,S2,mu,nu](g))

END fubini_tonelli