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 M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) )
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 M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) )
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 M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) )
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 M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) )
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 M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) )
let A be Element of sigma (measurable_rectangles (S1,S2)); for f being PartFunc of [:X1,X2:],ExtREAL st M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) )
let f be PartFunc of [:X1,X2:],ExtREAL; ( M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable implies ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) ) )
assume that
A1:
M2 is sigma_finite
and
A3:
( f is nonnegative & A = dom f & f is A -measurable )
; ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) )
set S = sigma (measurable_rectangles (S1,S2));
reconsider XX1 = X1 as Element of S1 by MEASURE1:7;
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
reconsider M = product_sigma_Measure (M1,M2) as sigma_Measure of (sigma (measurable_rectangles (S1,S2))) by MEASUR11:8;
reconsider XX12 = [:X1,X2:] as Element of sigma (measurable_rectangles (S1,S2)) by MEASURE1:7;
consider F being Functional_Sequence of [:X1,X2:],ExtREAL such that
A4:
for n being Nat holds
( F . n is_simple_func_in sigma (measurable_rectangles (S1,S2)) & dom (F . n) = dom f )
and
A5:
for n being Nat holds F . n is nonnegative
and
A6:
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
and
A7:
for z being Element of [:X1,X2:] st z in dom f holds
( F # z is convergent & lim (F # z) = f . z )
by A3, MESFUNC5:64;
then A8:
F is with_the_same_dom
by MESFUNC8:def 2;
defpred S1[ Nat, object ] means ex Fx being Function of X1,ExtREAL st
( $2 = Fx & dom Fx = X1 & ( for x1 being Element of X1 st x1 in dom Fx holds
Fx . x1 = Integral (M2,(ProjPMap1 ((F . $1),x1))) ) );
A10:
for n being Element of NAT ex FI2 being Element of PFuncs (X1,ExtREAL) st S1[n,FI2]
proof
let n be
Element of
NAT ;
ex FI2 being Element of PFuncs (X1,ExtREAL) st S1[n,FI2]
deffunc H1(
Element of
X1)
-> Element of
ExtREAL =
Integral (
M2,
(ProjPMap1 ((F . n),$1)));
consider FI2 being
Function such that A11:
(
dom FI2 = X1 & ( for
x1 being
Element of
X1 holds
FI2 . x1 = H1(
x1) ) )
from FUNCT_1:sch 4();
A12:
for
x2 being
object st
x2 in X1 holds
FI2 . x2 in ExtREAL
then
FI2 is
Function of
X1,
ExtREAL
by A11, FUNCT_2:3;
then reconsider FI2 =
FI2 as
Element of
PFuncs (
X1,
ExtREAL)
by PARTFUN1:45;
take
FI2
;
S1[n,FI2]
reconsider Fx =
FI2 as
Function of
X1,
ExtREAL by A12, A11, FUNCT_2:3;
for
x1 being
Element of
X1 st
x1 in dom Fx holds
Fx . x1 = Integral (
M2,
(ProjPMap1 ((F . n),x1)))
by A11;
hence
ex
Fx being
Function of
X1,
ExtREAL st
(
FI2 = Fx &
dom Fx = X1 & ( for
x1 being
Element of
X1 st
x1 in dom Fx holds
Fx . x1 = Integral (
M2,
(ProjPMap1 ((F . n),x1))) ) )
by A11;
verum
end;
consider FI2 being Function of NAT,(PFuncs (X1,ExtREAL)) such that
A13:
for n being Element of NAT holds S1[n,FI2 . n]
from FUNCT_2:sch 3(A10);
A14:
for n being Nat holds dom (FI2 . n) = X1
A15:
for n being Nat
for x1 being Element of X1 st x1 in dom (FI2 . n) holds
(FI2 . n) . x1 = Integral (M2,(ProjPMap1 ((F . n),x1)))
A16:
for x1 being Element of X1
for y1 being Element of X2 st y1 in dom (ProjPMap1 (f,x1)) holds
( (ProjPMap1 (F,x1)) # y1 is convergent & lim ((ProjPMap1 (F,x1)) # y1) = (ProjPMap1 (f,x1)) . y1 )
proof
let x1 be
Element of
X1;
for y1 being Element of X2 st y1 in dom (ProjPMap1 (f,x1)) holds
( (ProjPMap1 (F,x1)) # y1 is convergent & lim ((ProjPMap1 (F,x1)) # y1) = (ProjPMap1 (f,x1)) . y1 )let y1 be
Element of
X2;
( y1 in dom (ProjPMap1 (f,x1)) implies ( (ProjPMap1 (F,x1)) # y1 is convergent & lim ((ProjPMap1 (F,x1)) # y1) = (ProjPMap1 (f,x1)) . y1 ) )
reconsider z1 =
[x1,y1] as
Element of
[:X1,X2:] by ZFMISC_1:def 2;
assume
y1 in dom (ProjPMap1 (f,x1))
;
( (ProjPMap1 (F,x1)) # y1 is convergent & lim ((ProjPMap1 (F,x1)) # y1) = (ProjPMap1 (f,x1)) . y1 )
then
y1 in X-section (
A,
x1)
by A3, Def3;
then A17:
z1 in dom f
by A3, Th25;
then A18:
F # z1 is
convergent
by A7;
A19:
for
n being
Element of
NAT holds
(F # z1) . n = ((ProjPMap1 (F,x1)) # y1) . n
hence
(ProjPMap1 (F,x1)) # y1 is
convergent
by A18, FUNCT_2:def 8;
lim ((ProjPMap1 (F,x1)) # y1) = (ProjPMap1 (f,x1)) . y1
F # z1 = (ProjPMap1 (F,x1)) # y1
by A19, FUNCT_2:def 8;
then
lim ((ProjPMap1 (F,x1)) # y1) = f . (
x1,
y1)
by A7, A17;
hence
lim ((ProjPMap1 (F,x1)) # y1) = (ProjPMap1 (f,x1)) . y1
by A17, Def3;
verum
end;
A21:
for x being Element of X1 holds
( lim (ProjPMap1 (F,x)) = ProjPMap1 (f,x) & FI2 # x is convergent & lim (FI2 # x) = Integral (M2,(lim (ProjPMap1 (F,x)))) )
proof
let x be
Element of
X1;
( lim (ProjPMap1 (F,x)) = ProjPMap1 (f,x) & FI2 # x is convergent & lim (FI2 # x) = Integral (M2,(lim (ProjPMap1 (F,x)))) )
dom (lim (ProjPMap1 (F,x))) = dom ((ProjPMap1 (F,x)) . 0)
by MESFUNC8:def 9;
then
dom (lim (ProjPMap1 (F,x))) = dom (ProjPMap1 ((F . 0),x))
by Def5;
then
dom (lim (ProjPMap1 (F,x))) = X-section (
(dom (F . 0)),
x)
by Def3;
then
dom (lim (ProjPMap1 (F,x))) = X-section (
(dom f),
x)
by A4;
then A22:
dom (lim (ProjPMap1 (F,x))) = dom (ProjPMap1 (f,x))
by Def3;
for
y being
Element of
X2 st
y in dom (lim (ProjPMap1 (F,x))) holds
(lim (ProjPMap1 (F,x))) . y = (ProjPMap1 (f,x)) . y
proof
let y be
Element of
X2;
( y in dom (lim (ProjPMap1 (F,x))) implies (lim (ProjPMap1 (F,x))) . y = (ProjPMap1 (f,x)) . y )
assume A23:
y in dom (lim (ProjPMap1 (F,x)))
;
(lim (ProjPMap1 (F,x))) . y = (ProjPMap1 (f,x)) . y
then
(lim (ProjPMap1 (F,x))) . y = lim ((ProjPMap1 (F,x)) # y)
by MESFUNC8:def 9;
hence
(lim (ProjPMap1 (F,x))) . y = (ProjPMap1 (f,x)) . y
by A16, A22, A23;
verum
end;
hence
lim (ProjPMap1 (F,x)) = ProjPMap1 (
f,
x)
by A22, PARTFUN1:5;
( FI2 # x is convergent & lim (FI2 # x) = Integral (M2,(lim (ProjPMap1 (F,x)))) )
A24:
(ProjPMap1 (F,x)) . 0 = ProjPMap1 (
(F . 0),
x)
by Def5;
then
dom ((ProjPMap1 (F,x)) . 0) = X-section (
(dom (F . 0)),
x)
by Def3;
then
dom ((ProjPMap1 (F,x)) . 0) = X-section (
A,
x)
by A4, A3;
then A25:
dom ((ProjPMap1 (F,x)) . 0) = Measurable-X-section (
A,
x)
by MEASUR11:def 6;
F . 0 is
nonnegative
by A5;
then A26:
(ProjPMap1 (F,x)) . 0 is
nonnegative
by A24, Th32;
A27:
for
n being
Nat holds
(ProjPMap1 (F,x)) . n is
Measurable-X-section (
A,
x)
-measurable
A29:
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,x)) . n) . y <= ((ProjPMap1 (F,x)) . m) . y
proof
let n,
m be
Nat;
( n <= m implies for y being Element of X2 st y in Measurable-X-section (A,x) holds
((ProjPMap1 (F,x)) . n) . y <= ((ProjPMap1 (F,x)) . m) . y )
assume A30:
n <= m
;
for y being Element of X2 st y in Measurable-X-section (A,x) holds
((ProjPMap1 (F,x)) . n) . y <= ((ProjPMap1 (F,x)) . m) . y
let y be
Element of
X2;
( y in Measurable-X-section (A,x) implies ((ProjPMap1 (F,x)) . n) . y <= ((ProjPMap1 (F,x)) . m) . y )
assume A31:
y in Measurable-X-section (
A,
x)
;
((ProjPMap1 (F,x)) . n) . y <= ((ProjPMap1 (F,x)) . m) . y
then
y in dom (ProjPMap1 ((F . 0),x))
by A25, Def5;
then
y in X-section (
(dom (F . 0)),
x)
by Def3;
then
y in X-section (
(dom f),
x)
by A4;
then A32:
[x,y] in dom f
by Th25;
A33:
(
dom ((ProjPMap1 (F,x)) . n) = dom ((ProjPMap1 (F,x)) . 0) &
dom ((ProjPMap1 (F,x)) . m) = dom ((ProjPMap1 (F,x)) . 0) )
by A8, Th58, MESFUNC8:def 2;
(
(ProjPMap1 (F,x)) . n = ProjPMap1 (
(F . n),
x) &
(ProjPMap1 (F,x)) . m = ProjPMap1 (
(F . m),
x) )
by Def5;
then
(
((ProjPMap1 (F,x)) . n) . y = (F . n) . (
x,
y) &
((ProjPMap1 (F,x)) . m) . y = (F . m) . (
x,
y) )
by A25, A31, A33, Th26;
hence
((ProjPMap1 (F,x)) . n) . y <= ((ProjPMap1 (F,x)) . m) . y
by A6, A30, A32;
verum
end;
for
y being
Element of
X2 st
y in Measurable-X-section (
A,
x) holds
(ProjPMap1 (F,x)) # y is
convergent
then consider J being
ExtREAL_sequence such that A34:
for
n being
Nat holds
J . n = Integral (
M2,
((ProjPMap1 (F,x)) . n))
and A35:
J is
convergent
and A36:
Integral (
M2,
(lim (ProjPMap1 (F,x))))
= lim J
by A8, A25, A26, A27, A29, Th58, MESFUNC9:52;
for
n being
Element of
NAT holds
J . n = (FI2 # x) . n
hence
(
FI2 # x is
convergent &
lim (FI2 # x) = Integral (
M2,
(lim (ProjPMap1 (F,x)))) )
by A35, A36, FUNCT_2:63;
verum
end;
dom (lim FI2) = dom (FI2 . 0)
by MESFUNC8:def 9;
then A38:
dom (lim FI2) = X1
by A14;
then reconsider I2 = lim FI2 as Function of X1,ExtREAL by FUNCT_2:def 1;
take
I2
; ( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) )
for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x)))
hence
for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x)))
; for V being Element of S1 holds I2 is V -measurable
thus
for V being Element of S1 holds I2 is V -measurable
verum