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 A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
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 A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
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 A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
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 A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f)))
let M2 be sigma_Measure of S2; for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f)))
let A be Element of sigma (measurable_rectangles (S1,S2)); for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f)))
let f be PartFunc of [:X1,X2:],ExtREAL; ( M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )
assume that
A1:
M1 is sigma_finite
and
A2:
M2 is sigma_finite
and
A3:
f is nonnegative
and
A4:
A = dom f
and
A5:
f is A -measurable
; Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f)))
set S = sigma (measurable_rectangles (S1,S2));
reconsider XX1 = X1 as Element of S1 by MEASURE1:7;
reconsider EX1 = {} as Element of S1 by MEASURE1:7;
Integral ((Prod_Measure (M1,M2)),f) = integral+ ((Prod_Measure (M1,M2)),f)
by A3, A4, A5, MESFUNC5:88;
then consider F being Functional_Sequence of [:X1,X2:],ExtREAL, K being ExtREAL_sequence such that
A6:
( ( for n being Nat holds
( F . n is_simple_func_in sigma (measurable_rectangles (S1,S2)) & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for z being Element of [:X1,X2:] st z in dom f holds
(F . n) . z <= (F . m) . z ) & ( for z being Element of [:X1,X2:] st z in dom f holds
( F # z is convergent & lim (F # z) = f . z ) ) & ( for n being Nat holds K . n = integral' ((Prod_Measure (M1,M2)),(F . n)) ) )
and
K is convergent
and
A7:
Integral ((Prod_Measure (M1,M2)),f) = lim K
by A3, A4, A5, MESFUNC5:def 15;
dom (F . 0) = dom f
by A6;
then A8:
dom (lim F) = dom f
by MESFUNC8:def 9;
for z being Element of [:X1,X2:] st z in dom (lim F) holds
(lim F) . z = f . z
then A10:
lim F = f
by A8, PARTFUN1:5;
deffunc H1( Nat) -> Function of X1,ExtREAL = Integral2 (M2,(F . $1));
consider G being Functional_Sequence of X1,ExtREAL such that
A11:
for n being Nat holds G . n = H1(n)
from SEQFUNC:sch 1();
A12:
for n being Nat
for x being Element of X1 holds
( dom (ProjPMap1 ((F . n),x)) = Measurable-X-section (A,x) & ProjPMap1 ((F . n),x) is Measurable-X-section (A,x) -measurable & ProjPMap1 ((F . n),x) is nonnegative )
proof
let n be
Nat;
for x being Element of X1 holds
( dom (ProjPMap1 ((F . n),x)) = Measurable-X-section (A,x) & ProjPMap1 ((F . n),x) is Measurable-X-section (A,x) -measurable & ProjPMap1 ((F . n),x) is nonnegative )let x be
Element of
X1;
( dom (ProjPMap1 ((F . n),x)) = Measurable-X-section (A,x) & ProjPMap1 ((F . n),x) is Measurable-X-section (A,x) -measurable & ProjPMap1 ((F . n),x) is nonnegative )
A13:
dom (F . n) = A
by A4, A6;
then
dom (ProjPMap1 ((F . n),x)) = X-section (
A,
x)
by Def3;
hence
dom (ProjPMap1 ((F . n),x)) = Measurable-X-section (
A,
x)
by MEASUR11:def 6;
( ProjPMap1 ((F . n),x) is Measurable-X-section (A,x) -measurable & ProjPMap1 ((F . n),x) is nonnegative )
F . n is
A -measurable
by A6, MESFUNC2:34;
hence
ProjPMap1 (
(F . n),
x) is
Measurable-X-section (
A,
x)
-measurable
by A13, Th47;
ProjPMap1 ((F . n),x) is nonnegative
F . n is
nonnegative
by A6;
hence
ProjPMap1 (
(F . n),
x) is
nonnegative
by Th32;
verum
end;
A14:
for n being Nat holds
( dom (G . n) = XX1 & G . n is XX1 -measurable & G . n is nonnegative )
A16:
for x being Element of X1
for n, m being Nat st n <= m holds
for y being Element of X2 st y in Measurable-X-section (A,x) holds
(ProjPMap1 ((F . n),x)) . y <= (ProjPMap1 ((F . m),x)) . y
proof
let x be
Element of
X1;
for n, m being Nat st n <= m holds
for y being Element of X2 st y in Measurable-X-section (A,x) holds
(ProjPMap1 ((F . n),x)) . y <= (ProjPMap1 ((F . m),x)) . ylet n,
m be
Nat;
( n <= m implies for y being Element of X2 st y in Measurable-X-section (A,x) holds
(ProjPMap1 ((F . n),x)) . y <= (ProjPMap1 ((F . m),x)) . y )
assume A17:
n <= m
;
for y being Element of X2 st y in Measurable-X-section (A,x) holds
(ProjPMap1 ((F . n),x)) . y <= (ProjPMap1 ((F . m),x)) . y
hereby verum
let y be
Element of
X2;
( y in Measurable-X-section (A,x) implies (ProjPMap1 ((F . n),x)) . y <= (ProjPMap1 ((F . m),x)) . y )assume
y in Measurable-X-section (
A,
x)
;
(ProjPMap1 ((F . n),x)) . y <= (ProjPMap1 ((F . m),x)) . ythen
y in X-section (
A,
x)
by MEASUR11:def 6;
then
y in X-section (
(dom (F . n)),
x)
by A4, A6;
then
y in { y where y is Element of X2 : [x,y] in dom (F . n) }
by MEASUR11:def 4;
then A18:
ex
y1 being
Element of
X2 st
(
y1 = y &
[x,y1] in dom (F . n) )
;
then A19:
[x,y] in dom f
by A6;
then
[x,y] in dom (F . m)
by A6;
then
(
(ProjPMap1 ((F . n),x)) . y = (F . n) . (
x,
y) &
(ProjPMap1 ((F . m),x)) . y = (F . m) . (
x,
y) )
by A18, Def3;
hence
(ProjPMap1 ((F . n),x)) . y <= (ProjPMap1 ((F . m),x)) . y
by A6, A17, A19;
verum
end;
end;
A20:
for n, m being Nat st n <= m holds
for x being Element of X1 st x in XX1 holds
(G . n) . x <= (G . m) . x
proof
let n,
m be
Nat;
( n <= m implies for x being Element of X1 st x in XX1 holds
(G . n) . x <= (G . m) . x )
assume A21:
n <= m
;
for x being Element of X1 st x in XX1 holds
(G . n) . x <= (G . m) . x
hereby verum
let x be
Element of
X1;
( x in XX1 implies (G . n) . x <= (G . m) . x )assume
x in XX1
;
(G . n) . x <= (G . m) . xA22:
(
dom (ProjPMap1 ((F . n),x)) = Measurable-X-section (
A,
x) &
dom (ProjPMap1 ((F . m),x)) = Measurable-X-section (
A,
x) &
ProjPMap1 (
(F . n),
x) is
Measurable-X-section (
A,
x)
-measurable &
ProjPMap1 (
(F . m),
x) is
Measurable-X-section (
A,
x)
-measurable &
ProjPMap1 (
(F . n),
x) is
nonnegative &
ProjPMap1 (
(F . m),
x) is
nonnegative )
by A12;
for
y being
Element of
X2 st
y in dom (ProjPMap1 ((F . n),x)) holds
(ProjPMap1 ((F . n),x)) . y <= (ProjPMap1 ((F . m),x)) . y
by A16, A21, A22;
then
integral+ (
M2,
(ProjPMap1 ((F . n),x)))
<= integral+ (
M2,
(ProjPMap1 ((F . m),x)))
by A22, MESFUNC5:85;
then
Integral (
M2,
(ProjPMap1 ((F . n),x)))
<= integral+ (
M2,
(ProjPMap1 ((F . m),x)))
by A22, MESFUNC5:88;
then A23:
Integral (
M2,
(ProjPMap1 ((F . n),x)))
<= Integral (
M2,
(ProjPMap1 ((F . m),x)))
by A22, MESFUNC5:88;
(G . n) . x = (Integral2 (M2,(F . n))) . x
by A11;
then A24:
(G . n) . x = Integral (
M2,
(ProjPMap1 ((F . n),x)))
by Def8;
(G . m) . x = (Integral2 (M2,(F . m))) . x
by A11;
hence
(G . n) . x <= (G . m) . x
by A23, A24, Def8;
verum
end;
end;
A25:
for x being Element of X1 st x in XX1 holds
( G # x is convergent & lim (G # x) = Integral (M2,(ProjPMap1 (f,x))) )
proof
let x be
Element of
X1;
( x in XX1 implies ( G # x is convergent & lim (G # x) = Integral (M2,(ProjPMap1 (f,x))) ) )
assume
x in XX1
;
( G # x is convergent & lim (G # x) = Integral (M2,(ProjPMap1 (f,x))) )
defpred S1[
Element of
NAT ,
object ]
means $2
= ProjPMap1 (
(F . $1),
x);
A26:
for
n being
Element of
NAT ex
f being
Element of
PFuncs (
X2,
ExtREAL) st
S1[
n,
f]
consider FX being
sequence of
(PFuncs (X2,ExtREAL)) such that A27:
for
n being
Element of
NAT holds
S1[
n,
FX . n]
from FUNCT_2:sch 3(A26);
A28:
for
n being
Nat holds
dom (FX . n) = Measurable-X-section (
A,
x)
for
m,
n being
Nat holds
dom (FX . m) = dom (FX . n)
then reconsider FX =
FX as
with_the_same_dom Functional_Sequence of
X2,
ExtREAL by MESFUNC8:def 2;
A29:
dom (FX . 0) = Measurable-X-section (
A,
x)
by A28;
A30:
for
n being
Nat holds
FX . n is
Measurable-X-section (
A,
x)
-measurable
ProjPMap1 (
(F . 0),
x) is
nonnegative
by A12;
then A32:
FX . 0 is
nonnegative
by A27;
A33:
for
n,
m being
Nat st
n <= m holds
for
y being
Element of
X2 st
y in Measurable-X-section (
A,
x) holds
(FX . n) . y <= (FX . m) . y
A36:
dom (ProjPMap1 (f,x)) = X-section (
A,
x)
by A4, Def3;
A37:
for
y being
Element of
X2 st
y in Measurable-X-section (
A,
x) holds
(
FX # y is
convergent &
(ProjPMap1 (f,x)) . y = lim (FX # y) )
proof
let y be
Element of
X2;
( y in Measurable-X-section (A,x) implies ( FX # y is convergent & (ProjPMap1 (f,x)) . y = lim (FX # y) ) )
reconsider z =
[x,y] as
Element of
[:X1,X2:] by ZFMISC_1:def 2;
assume
y in Measurable-X-section (
A,
x)
;
( FX # y is convergent & (ProjPMap1 (f,x)) . y = lim (FX # y) )
then
y in X-section (
A,
x)
by MEASUR11:def 6;
then A38:
[x,y] in dom f
by A4, Th25;
then A39:
(
F # z is
convergent &
lim (F # z) = f . z )
by A6;
A40:
for
n being
Element of
NAT holds
(FX # y) . n = (F # z) . n
hence
FX # y is
convergent
by A39, FUNCT_2:63;
(ProjPMap1 (f,x)) . y = lim (FX # y)
(ProjPMap1 (f,x)) . y = f . (
x,
y)
by A38, Def3;
hence
(ProjPMap1 (f,x)) . y = lim (FX # y)
by A39, A40, FUNCT_2:63;
verum
end;
then
for
y being
Element of
X2 st
y in Measurable-X-section (
A,
x) holds
FX # y is
convergent
;
then consider I being
ExtREAL_sequence such that A42:
( ( for
n being
Nat holds
I . n = Integral (
M2,
(FX . n)) ) &
I is
convergent &
Integral (
M2,
(lim FX))
= lim I )
by A29, A30, A32, A33, MESFUNC9:52;
A43:
for
n being
Element of
NAT holds
(G # x) . n = I . n
hence
G # x is
convergent
by A42, FUNCT_2:def 8;
lim (G # x) = Integral (M2,(ProjPMap1 (f,x)))
A44:
G # x = I
by A43, FUNCT_2:def 8;
A45:
dom (lim FX) = Measurable-X-section (
A,
x)
by A29, MESFUNC8:def 9;
for
y being
Element of
X2 st
y in dom (lim FX) holds
(lim FX) . y = (ProjPMap1 (f,x)) . y
hence
lim (G # x) = Integral (
M2,
(ProjPMap1 (f,x)))
by A44, A45, A36, A42, PARTFUN1:5, MEASUR11:def 6;
verum
end;
then A47:
for x being Element of X1 st x in XX1 holds
G # x is convergent
;
then A48:
G is with_the_same_dom
by MESFUNC8:def 2;
G . 0 = Integral2 (M2,(F . 0))
by A11;
then
XX1 = dom (G . 0)
by FUNCT_2:def 1;
then consider J being ExtREAL_sequence such that
A49:
( ( for n being Nat holds J . n = Integral (M1,(G . n)) ) & J is convergent & Integral (M1,(lim G)) = lim J )
by A14, A20, A47, A48, MESFUNC9:52;
dom (lim G) = dom (G . 0)
by MESFUNC8:def 9;
then
dom (lim G) = dom (Integral2 (M2,(F . 0)))
by A11;
then
dom (lim G) = XX1
by FUNCT_2:def 1;
then A50:
dom (lim G) = dom (Integral2 (M2,(lim F)))
by FUNCT_2:def 1;
for x being Element of X1 st x in dom (lim G) holds
(lim G) . x = (Integral2 (M2,(lim F))) . x
then A51:
lim G = Integral2 (M2,(lim F))
by A50, PARTFUN1:5;
for n being Element of NAT holds K . n = J . n
proof
let n be
Element of
NAT ;
K . n = J . n
A52:
A = dom (F . n)
by A4, A6;
A53:
(
F . n is
nonnegative &
F . n is_simple_func_in sigma (measurable_rectangles (S1,S2)) )
by A6;
K . n = integral' (
(Prod_Measure (M1,M2)),
(F . n))
by A6;
then
K . n = Integral (
(Prod_Measure (M1,M2)),
(F . n))
by A53, MESFUNC5:89;
then
K . n = Integral (
M1,
(Integral2 (M2,(F . n))))
by A1, A2, A52, A53, Lm15;
then
K . n = Integral (
M1,
(G . n))
by A11;
hence
K . n = J . n
by A49;
verum
end;
hence
Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f)))
by A7, A10, A49, A51, FUNCT_2:def 8; verum