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 E being Element of sigma (measurable_rectangles (S1,S2))
for r being Real st M1 is sigma_finite & M2 is sigma_finite holds
( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
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 E being Element of sigma (measurable_rectangles (S1,S2))
for r being Real st M1 is sigma_finite & M2 is sigma_finite holds
( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
let S2 be SigmaField of X2; for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for r being Real st M1 is sigma_finite & M2 is sigma_finite holds
( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
let M1 be sigma_Measure of S1; for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for r being Real st M1 is sigma_finite & M2 is sigma_finite holds
( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
let M2 be sigma_Measure of S2; for E being Element of sigma (measurable_rectangles (S1,S2))
for r being Real st M1 is sigma_finite & M2 is sigma_finite holds
( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
let E be Element of sigma (measurable_rectangles (S1,S2)); for r being Real st M1 is sigma_finite & M2 is sigma_finite holds
( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
let r be Real; ( M1 is sigma_finite & M2 is sigma_finite implies ( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) ) )
assume that
A1:
M1 is sigma_finite
and
A2:
M2 is sigma_finite
; ( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
set S = sigma (measurable_rectangles (S1,S2));
set M = Prod_Measure (M1,M2);
reconsider XX12 = [:X1,X2:] 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;
A3:
chi (r,E,[:X1,X2:]) = r (#) (chi (E,[:X1,X2:]))
by Th1;
A4:
chi (E,[:X1,X2:]) is_simple_func_in sigma (measurable_rectangles (S1,S2))
by Th12;
A5:
chi (E,[:X1,X2:]) is XX12 -measurable
by Th12, MESFUNC2:34;
A6:
dom (chi (E,[:X1,X2:])) = XX12
by FUNCT_2:def 1;
A7:
Integral1 (M1,(chi (E,[:X1,X2:]))) = X-vol (E,M1)
by A1, Th64;
A8:
X-vol (E,M1) is XX2 -measurable
by A1, MEASUR11:def 14;
A9:
dom (Integral1 (M1,(chi (E,[:X1,X2:])))) = XX2
by FUNCT_2:def 1;
A10: Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) =
Integral ((Prod_Measure (M1,M2)),(r (#) (chi (E,[:X1,X2:]))))
by Th1
.=
r * (integral' ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:]))))
by Th12, MESFUN11:59
.=
r * (Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:]))))
by A4, MESFUNC5:89
;
then A14: Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) =
r * (Integral (M2,(Integral1 (M1,(chi (E,[:X1,X2:]))))))
by A1, A2, Th82
.=
Integral (M2,(r (#) (X-vol (E,M1))))
by A7, A8, A9, Lm1
;
hence
Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:])))))
by A3, A5, A6, A7, Th78; ( Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
reconsider C = (chi (E,[:X1,X2:])) | E as PartFunc of [:X1,X2:],ExtREAL ;
A11:
dom C = E
by A6, RELAT_1:62;
A12: (chi (r,E,[:X1,X2:])) | E =
(r (#) (chi (E,[:X1,X2:]))) | E
by Th1
.=
r (#) C
by MESFUN11:2
;
A13: Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) =
Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:])))))
by Th81
.=
Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:])))
by A3, A5, A6, A7, A14, Th78
;
C is E -measurable
by A4, MESFUNC2:34, MESFUNC5:34;
then A15: Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) =
r * (Integral ((Prod_Measure (M1,M2)),C))
by A11, A12, Lm1, MESFUNC5:15
.=
r * ((Prod_Measure (M1,M2)) . E)
by MESFUNC9:14
.=
r * (Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:]))))
by MESFUNC9:14
.=
Integral ((Prod_Measure (M1,M2)),(r (#) (chi (E,[:X1,X2:]))))
by A4, A6, Lm1, MESFUNC2:34
;
hence
Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E))))
by A13, Th1; ( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
B7:
Integral2 (M2,(chi (E,[:X1,X2:]))) = Y-vol (E,M2)
by A2, Th65;
B8:
Y-vol (E,M2) is XX1 -measurable
by A2, MEASUR11:def 13;
B9:
dom (Integral2 (M2,(chi (E,[:X1,X2:])))) = XX1
by FUNCT_2:def 1;
B14: Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) =
r * (Integral (M1,(Integral2 (M2,(chi (E,[:X1,X2:]))))))
by A1, A2, A10, Th82
.=
Integral (M1,(r (#) (Y-vol (E,M2))))
by B7, B8, B9, Lm1
;
hence
Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:])))))
by A3, A5, A6, B7, Th78; Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E))))
Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) =
Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:])))))
by Th81
.=
Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:])))
by A3, A5, A6, B7, B14, Th78
;
hence
Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E))))
by A15, Th1; verum