Quelle  fubini.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[(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 fubini_tonelli[T1,T2,S1,S2,mu,nu]

  f: VAR integrable[[T1,T2],sigma_times(S1,S2),m_times(mu,nu)]
  x: VAR T1
  y: VAR T2

  integrable_is_integrable1: LEMMA integrable1?(f)
  integrable_is_integrable2: LEMMA integrable2?(f)

  fubini1: LEMMA integral(f) = integral(integral1[T1,T2,S1,S2,mu,nu](f))
  fubini2: LEMMA integral(f) = integral(integral2[T1,T2,S1,S2,mu,nu](f))

END fubini