let X1, X2 be non empty set ; for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
let S1 be SigmaField of X1; for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
let S2 be SigmaField of X2; for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
let M1 be sigma_Measure of S1; for M2 being sigma_Measure of S2
for f being empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
let M2 be sigma_Measure of S2; for f being empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
let f be empty PartFunc of [:X1,X2:],ExtREAL; for A being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
let A be Element of sigma (measurable_rectangles (S1,S2)); ( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
reconsider EMP = {} as Element of sigma (measurable_rectangles (S1,S2)) by MEASURE1:7;
reconsider XX1 = X1 as Element of S1 by MEASURE1:7;
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
A2:
f is_simple_func_in sigma (measurable_rectangles (S1,S2))
by Th19;
A3:
f is EMP -measurable
by Th19, MESFUNC2:34;
A5:
for x being object st x in dom f holds
0 <= f . x
;
then A6:
f is nonnegative
by SUPINF_2:52;
A4:
dom f = EMP
;
then
integral' ((Prod_Measure (M1,M2)),f) = 0
by MESFUNC5:def 14;
then A7:
Integral ((Prod_Measure (M1,M2)),f) = 0
by A2, A6, MESFUNC5:89;
A8:
( dom (Integral1 (M1,f)) = XX2 & dom (Integral2 (M2,f)) = XX1 )
by FUNCT_2:def 1;
A10:
( Integral1 (M1,f) is V112() & Integral2 (M2,f) is V112() )
by A3, A4, A6, Th66;
hereby ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )
assume
M1 is
sigma_finite
;
Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f)))then A9:
Integral1 (
M1,
f) is
XX2 -measurable
by A3, A5, Th59, SUPINF_2:52;
for
y being
Element of
X2 st
y in dom (Integral1 (M1,f)) holds
(Integral1 (M1,f)) . y = 0
proof
let y be
Element of
X2;
( y in dom (Integral1 (M1,f)) implies (Integral1 (M1,f)) . y = 0 )
assume
y in dom (Integral1 (M1,f))
;
(Integral1 (M1,f)) . y = 0
A11:
(
ProjPMap2 (
f,
y)
is_simple_func_in S1 &
ProjPMap2 (
f,
y) is
nonnegative )
by A6, A2, Th31, Th32;
dom f = {} [:X1,X2:]
;
then dom (ProjPMap2 (f,y)) =
Y-section (
({} [:X1,X2:]),
y)
by Def4
.=
{}
by MEASUR11:24
;
then
integral' (
M1,
(ProjPMap2 (f,y)))
= 0
by MESFUNC5:def 14;
then
Integral (
M1,
(ProjPMap2 (f,y)))
= 0
by A11, MESFUNC5:89;
hence
(Integral1 (M1,f)) . y = 0
by Def7;
verum
end; then
integral+ (
M2,
(Integral1 (M1,f)))
= 0
by A8, A9, MESFUNC5:87;
hence
Integral (
(Prod_Measure (M1,M2)),
f)
= Integral (
M2,
(Integral1 (M1,f)))
by A7, A8, A9, A10, MESFUNC5:88;
verum
end;
assume
M2 is sigma_finite
; Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f)))
then B9:
Integral2 (M2,f) is XX1 -measurable
by A3, A5, Th60, SUPINF_2:52;
for x being Element of X1 st x in dom (Integral2 (M2,f)) holds
(Integral2 (M2,f)) . x = 0
proof
let x be
Element of
X1;
( x in dom (Integral2 (M2,f)) implies (Integral2 (M2,f)) . x = 0 )
assume
x in dom (Integral2 (M2,f))
;
(Integral2 (M2,f)) . x = 0
B11:
(
ProjPMap1 (
f,
x)
is_simple_func_in S2 &
ProjPMap1 (
f,
x) is
nonnegative )
by A6, A2, Th31, Th32;
dom f = {} [:X1,X2:]
;
then dom (ProjPMap1 (f,x)) =
X-section (
({} [:X1,X2:]),
x)
by Def3
.=
{}
by MEASUR11:24
;
then
integral' (
M2,
(ProjPMap1 (f,x)))
= 0
by MESFUNC5:def 14;
then
Integral (
M2,
(ProjPMap1 (f,x)))
= 0
by B11, MESFUNC5:89;
hence
(Integral2 (M2,f)) . x = 0
by Def8;
verum
end;
then
integral+ (M1,(Integral2 (M2,f))) = 0
by A8, B9, MESFUNC5:87;
hence
Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f)))
by A7, A8, B9, A10, MESFUNC5:88; verum