|
%------------------------------------------------------------------------------
% 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
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
