|
%------------------------------------------------------------------------------
% Auxilliary results required by 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
%
% Properties of iterated integration with finite measures and simple functions
%
% Version 1.0 1/5/07 Initial Version
%------------------------------------------------------------------------------
finite_fubini_scaf[(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 product_sigma[T1,T2,S1,S2],
measure_def[T1,S1],
measure_def[T2,S2],
measure_def[[T1,T2],sigma_times(S1,S2)],
product_finite_measure[T1,T2,S1,S2]
IMPORTING nn_integral[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]
g: VAR nn_integrable
i: VAR isf
n: VAR nn_isf
E: VAR (sigma_times(S1,S2))
IMPORTING integral[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]
f: VAR integrable
h: VAR nn_measurable[[T1,T2],sigma_times(S1,S2)]
m: VAR measurable_function[[T1,T2],sigma_times(S1,S2)]
x: VAR T1
y: VAR T2
IMPORTING integral[T1,S1,to_measure(mu)],
integral[T2,S2,to_measure(nu)]
measurable_x_section: LEMMA measurable_function?[T2,S2](lambda y: m(x,y))
measurable_y_section: LEMMA measurable_function?[T1,S1](lambda x: m(x,y))
isf_x_section: LEMMA isf?(lambda y: i(x,y)) % 7.3.4 (i)
isf_y_section: LEMMA isf?(lambda x: i(x,y)) % 7.3.4 (i)
integral_phi1: LEMMA % 7.3.4 (i)
(lambda x: isf_integral[T2,S2,to_measure(nu)](lambda y: phi(E)(x,y))) =
nu o x_section(E)
integral_phi2: LEMMA % 7.3.4 (i)
(lambda y: isf_integral[T1,S1,to_measure(mu)](lambda x: phi(E)(x,y))) =
o[T2,(S1),nnreal](mu,y_section(E))
integral_phi3: LEMMA % 7.3.4 (i)
isf_integral(phi(E))
= integral(lambda x: isf_integral(lambda y: phi(E)(x,y)))
integral_phi4: LEMMA % 7.3.4 (i)
isf_integral(phi(E))
= integral(lambda y: isf_integral(lambda x: phi(E)(x,y)))
isf_integral_x: LEMMA integrable?(lambda x: isf_integral(lambda y: i(x,y)))
isf_integral_y: LEMMA integrable?(lambda y: isf_integral(lambda x: i(x,y)))
isf_fubini_tonelli_3: LEMMA
isf_integral(i) = integral(lambda x: isf_integral(lambda y: i(x,y)))
isf_fubini_tonelli_4: LEMMA
isf_integral(i) = integral(lambda y: isf_integral(lambda x: i(x,y)))
END finite_fubini_scaf
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
