Quelle  finite_fubini.pvs

%------------------------------------------------------------------------------
% Fubini's Theorems for finite measures
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Interchanging the order of integration for finite measures.
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

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

BEGIN

  IMPORTING
   sigma_algebra[T1,S1],
   sigma_algebra[T2,S2],
   finite_fubini_tonelli[T1,T2,S1,S2,mu,nu],
   finite_integral[[T1,T2],sigma_times(S1,S2),fm_times(mu,nu)], % Proof Only
   finite_integral[T1,S1,mu], % Proof Only
   finite_integral[T2,S2,nu]  % Proof Only

  f: VAR integrable[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]

  finite_integrable_is_integrable1: LEMMA integrable1?(f)               % 7.3.7
  finite_integrable_is_integrable2: LEMMA integrable2?(f)               % 7.3.7

  finite_fubini1: COROLLARY integral(f) = integral(integral1(f))        % 7.3.7
  finite_fubini2: COROLLARY integral(f) = integral(integral2(f))        % 7.3.7

  h: VAR bounded_measurable[[T1,T2],sigma_times(S1,S2)]
  x: VAR T1
  y: VAR T2

  integrable_x_section: LEMMA integrable?(lambda y: h(x,y))             % 7.3.8
  integrable_y_section: LEMMA integrable?(lambda x: h(x,y))             % 7.3.8

  integrable_integral_x_section: LEMMA                                  % 7.3.8
    integrable?(lambda x: integral(lambda y: h(x,y)))
  integrable_integral_y_section: LEMMA                                  % 7.3.8
    integrable?(lambda y: integral(lambda x: h(x,y)))

  integral_integral_x_section: LEMMA                                    % 7.3.8
    integral(lambda x: integral(lambda y: h(x,y))) = integral(h)
  integral_integral_y_section: LEMMA                                    % 7.3.8
    integral(lambda y: integral(lambda x: h(x,y))) = integral(h)

END finite_fubini