|
%------------------------------------------------------------------------------
% Fubini-Tonelli Theorems
%
% Author: David Lester, Manchester University, NIA, Universite Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Version 1.0 5/06/09 Initial Version
%------------------------------------------------------------------------------
fubini_tonelli[(IMPORTING subset_algebra_def, measure_def)
T1,T2: TYPE,
S1:sigma_algebra[T1],S2:sigma_algebra[T2],
mu:sigma_finite_measure[T1,S1],
nu:sigma_finite_measure[T2,S2]]: THEORY
BEGIN
IMPORTING product_measure[T1,T2,S1,S2],
integral[[T1,T2],sigma_times(S1,S2),m_times(mu,nu)]
g: VAR nn_integrable
h: VAR nn_measurable[[T1,T2],sigma_times(S1,S2)]
x: VAR T1
y: VAR T2
IMPORTING product_integral_def[T1,T2,S1,S2,mu,nu],
fubini_tonelli_scaf[T1,T2,S1,S2,mu,nu]
fubini_tonelli_1: THEOREM integrable?(h) <=> integrable1?(h) % 7.4.7
fubini_tonelli_2: THEOREM integrable?(h) <=> integrable2?(h) % 7.4.7
fubini_tonelli_3: THEOREM % 7.4.7
integral(g) = integral(integral1[T1,T2,S1,S2,mu,nu](g))
fubini_tonelli_4: THEOREM % 7.4.7
integral(g) = integral(integral2[T1,T2,S1,S2,mu,nu](g))
END fubini_tonelli
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
