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