%------------------------------------------------------------------------------
% Product of two sigam-finite measures
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Generalizing the results for finite measures to sigma-finite measures.
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------
product_measure[(IMPORTING subset_algebra_def)
                T1,T2:TYPE,
                S1:sigma_algebra[T1], S2:sigma_algebra[T2]]: THEORY
BEGIN

  IMPORTING product_sigma[T1,T2,S1,S2],
            measure_contraction[T1,S1],
            measure_contraction[T2,S2],
            measure_contraction[[T1,T2],sigma_times(S1,S2)],
            product_finite_measure[T1,T2,S1,S2],
            extended_nnreal@double_index[set[[T1,T2]]] % Proof Only

  mu: VAR sigma_finite_measure[T1,S1]
  nu: VAR sigma_finite_measure[T2,S2]
  X:  VAR (S1)
  Y:  VAR (S2)
  M:  VAR (sigma_times(S1,S2))
  z:  VAR [T1,T2]
  i,j,n:  VAR nat

  product_measure_approx(mu,nu)(i,j):finite_measure[[T1,T2],sigma_times(S1,S2)]
   = fm_times(fm_contraction[T1,S1](mu,A_of(mu)(i)),
              fm_contraction[T2,S2](nu,A_of(nu)(j)))

  m_times(mu,nu):sigma_finite_measure[[T1,T2],sigma_times(S1,S2)]      % 7.2.12
     = lambda M:
         x_sum(lambda i: x_sum(lambda j:
                to_measure(product_measure_approx(mu,nu)(i,j))(M)))

  m_times_alt: LEMMA
     x_eq(m_times(mu,nu)(M),
          x_sum(lambda j: x_sum(lambda i:
                           to_measure(product_measure_approx(mu,nu)(i,j))(M))))

  rectangle_measure: LEMMA
    x_eq(m_times(mu,nu)(cross_product(X,Y)),x_times(mu(X),nu(Y)))

  phi1(X):simple[[T1,T2],sigma_times(S1,S2)]= phi(cross_product(X,fullset[T2]))
  phi2(Y):simple[[T1,T2],sigma_times(S1,S2)]= phi(cross_product(fullset[T1],Y))

END product_measure