%------------------------------------------------------------------------------ % Fubini-Tonelli Theorems for finite measures % % Author: David Lester, Manchester University, NIA, Université Perpignan % % All references are to SK Berberian "Fundamentals of Real Analysis", % Springer, 1991 % % Properties of iterated integration with finite measures and measurable % functions % % Version 1.0 1/5/07 Initial Version %------------------------------------------------------------------------------
finite_fubini_tonelli[(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 finite_fubini_scaf[T1,T2,S1,S2,mu,nu],
product_integral_def[T1,T2,S1,S2,to_measure(mu),to_measure(nu)],
integral_convergence, % Proof only
indefinite_integral % Proof only
g: VAR nn_integrable[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]
h: VAR nn_measurable[[T1,T2],sigma_times(S1,S2)]
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
