Quelle  product_finite_measure.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Product of two finite measures
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% How to get a finite measure for sets of [T1,T2], given mu and nu
% (finite measures for T1 and T2 respectively).
%
% Suppose that mu=nu and T1=T2=real. Then fm_times(mu,nu) has to be able to
% calculate the measure (i.e. area) of a circle; not just for rectangles.
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

product_finite_measure[(IMPORTING subset_algebra_def)
                       T1,T2:TYPE, 
                       S1:sigma_algebra[T1], S2:sigma_algebra[T2]]: THEORY

BEGIN

  IMPORTING product_sigma_def[T1,T2],
            product_sigma[T1,T2,S1,S2],
            measure_def[T1,S1],
            measure_def[T2,S2],
            measure_def[[T1,T2],sigma_times(S1,S2)],
            integral,
            finite_measure,
            monotone_classes,        % Proof only
            integral_convergence     % Proof only

  M: VAR (sigma_times(S1,S2))
  x: VAR T1
  y: VAR T2
  X: VAR (S1)
  Y: VAR (S2)
  E: VAR sequence[(sigma_times(S1,S2))]
  mu: VAR finite_measure[T1,S1]
  nu: VAR finite_measure[T2,S2]

  x_section_bounded: LEMMA 0 <= (nu o x_section(M))(x) AND        % SKB 7.2.9
                           (nu o x_section(M))(x) <= nu(fullset[T2])
  y_section_bounded: LEMMA 0 <= (mu o y_section(M))(y) AND        % SKB 7.2.9
                           (mu o y_section(M))(y) <= mu(fullset[T1])

  x_section_measurable: LEMMA measurable_function?[T1,S1](nu o x_section(M))
  y_section_measurable: LEMMA measurable_function?[T2,S2](mu o y_section(M))
                                                                   % SKB 7.2.10
  x_section_integrable: LEMMA
    integrable?[T1,S1,to_measure(mu)](nu o x_section(M))
  y_section_integrable: LEMMA
    integrable?[T2,S2,to_measure(nu)](mu o y_section(M))

  rectangle_measure1: LEMMA M = cross_product(X,Y) =>
        integral[T1,S1,to_measure(mu)](nu o x_section(M)) = mu(X)*nu(Y)
  rectangle_measure2: LEMMA M = cross_product(X,Y) =>
        integral[T2,S2,to_measure(nu)](mu o y_section(M)) = mu(X)*nu(Y)

  fm_times(mu,nu):finite_measure[[T1,T2],sigma_times(S1,S2)]
    = lambda M: integral[T1,S1,to_measure(mu)](nu o x_section(M))

  fm_times_alt: LEMMA finite_measure?[[T1,T2],sigma_times(S1,S2)]
       (lambda M: integral[T2,S2,to_measure(nu)](mu o y_section(M)))

  finite_product_alt: THEOREM                                      % SKB 7.2.11
    fm_times(mu,nu)(M) = integral[T2,S2,to_measure(nu)](mu o y_section(M))

END product_finite_measure