let X1, X2 be non empty set ; :: thesis: 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 PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) & ( for y being Element of X2 holds (Integral1 (M1,|.f.|)) . y < +infty ) holds
( ( for y being Element of X2 holds ProjPMap2 (f,y) is_integrable_on M1 ) & ( for V being Element of S2 holds Integral1 (M1,f) is V -measurable ) & Integral1 (M1,f) is_integrable_on M2 & Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral1 (M1,f) in L1_Functions M2 )
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) & ( for y being Element of X2 holds (Integral1 (M1,|.f.|)) . y < +infty ) holds
( ( for y being Element of X2 holds ProjPMap2 (f,y) is_integrable_on M1 ) & ( for V being Element of S2 holds Integral1 (M1,f) is V -measurable ) & Integral1 (M1,f) is_integrable_on M2 & Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral1 (M1,f) in L1_Functions M2 )
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) & ( for y being Element of X2 holds (Integral1 (M1,|.f.|)) . y < +infty ) holds
( ( for y being Element of X2 holds ProjPMap2 (f,y) is_integrable_on M1 ) & ( for V being Element of S2 holds Integral1 (M1,f) is V -measurable ) & Integral1 (M1,f) is_integrable_on M2 & Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral1 (M1,f) in L1_Functions M2 )
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) & ( for y being Element of X2 holds (Integral1 (M1,|.f.|)) . y < +infty ) holds
( ( for y being Element of X2 holds ProjPMap2 (f,y) is_integrable_on M1 ) & ( for V being Element of S2 holds Integral1 (M1,f) is V -measurable ) & Integral1 (M1,f) is_integrable_on M2 & Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral1 (M1,f) in L1_Functions M2 )
let M2 be sigma_Measure of S2; :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) & ( for y being Element of X2 holds (Integral1 (M1,|.f.|)) . y < +infty ) holds
( ( for y being Element of X2 holds ProjPMap2 (f,y) is_integrable_on M1 ) & ( for V being Element of S2 holds Integral1 (M1,f) is V -measurable ) & Integral1 (M1,f) is_integrable_on M2 & Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral1 (M1,f) in L1_Functions M2 )
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: ( M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) & ( for y being Element of X2 holds (Integral1 (M1,|.f.|)) . y < +infty ) implies ( ( for y being Element of X2 holds ProjPMap2 (f,y) is_integrable_on M1 ) & ( for V being Element of S2 holds Integral1 (M1,f) is V -measurable ) & Integral1 (M1,f) is_integrable_on M2 & Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral1 (M1,f) in L1_Functions M2 ) )
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: f is_integrable_on Prod_Measure (M1,M2) and
A4: for y being Element of X2 holds (Integral1 (M1,|.f.|)) . y < +infty ; :: thesis: ( ( for y being Element of X2 holds ProjPMap2 (f,y) is_integrable_on M1 ) & ( for V being Element of S2 holds Integral1 (M1,f) is V -measurable ) & Integral1 (M1,f) is_integrable_on M2 & Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral1 (M1,f) in L1_Functions M2 )
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
consider A being Element of sigma (measurable_rectangles (S1,S2)) such that
A5: ( A = dom f & f is A -measurable ) by A3, MESFUNC5:def 17;
A6: A = dom |.f.| by A5, MESFUNC1:def 10;
A7: now :: thesis: for x being Element of X2 holds ProjPMap2 (f,x) is_integrable_on M1
let x be Element of X2; :: thesis: ProjPMap2 (f,x) is_integrable_on M1
Y-section (A,x) = Measurable-Y-section (A,x) by MEASUR11:def 7;
then A8: dom (ProjPMap2 (|.f.|,x)) = Measurable-Y-section (A,x) by A6, MESFUN12:def 4;
A9: |.f.| is A -measurable by A5, MESFUNC2:27;
then A10: ProjPMap2 (|.f.|,x) is Measurable-Y-section (A,x) -measurable by A6, MESFUN12:47;
A11: ProjPMap2 (|.f.|,x) = |.(ProjPMap2 (f,x)).| by Th27;
then integral+ (M1,(max+ (ProjPMap2 (|.f.|,x)))) = integral+ (M1,(ProjPMap2 (|.f.|,x))) by MESFUN11:31
.= Integral (M1,(ProjPMap2 (|.f.|,x))) by A6, A8, A9, A11, MESFUNC5:88, MESFUN12:47
.= (Integral1 (M1,|.f.|)) . x by MESFUN12:def 7 ;
then A12: integral+ (M1,(max+ (ProjPMap2 (|.f.|,x)))) < +infty by A4;
integral+ (M1,(max- (ProjPMap2 (|.f.|,x)))) = 0 by A8, A10, A11, MESFUN11:53;
then A13: ProjPMap2 (|.f.|,x) is_integrable_on M1 by A6, A8, A9, A12, MESFUNC5:def 17, MESFUN12:47;
A14: dom (ProjPMap2 (f,x)) = Measurable-Y-section (A,x) by A8, A11, MESFUNC1:def 10;
ProjPMap2 (f,x) is Measurable-Y-section (A,x) -measurable by A5, MESFUN12:47;
hence ProjPMap2 (f,x) is_integrable_on M1 by A11, A13, A14, MESFUNC5:100; :: thesis: verum
end;
hence for x being Element of X2 holds ProjPMap2 (f,x) is_integrable_on M1 ; :: thesis: ( ( for V being Element of S2 holds Integral1 (M1,f) is V -measurable ) & Integral1 (M1,f) is_integrable_on M2 & Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral1 (M1,f) in L1_Functions M2 )
set G1 = Integral1 (M1,(max+ f));
set G2 = Integral1 (M1,(max- f));
set G = (Integral1 (M1,(max+ f))) - (Integral1 (M1,(max- f)));
A15: ( dom (Integral1 (M1,(max+ f))) = X2 & dom (Integral1 (M1,(max- f))) = X2 & dom (Integral1 (M1,f)) = X2 & dom (Integral1 (M1,|.f.|)) = X2 ) by FUNCT_2:def 1;
A16: now :: thesis: for x being object holds (Integral1 (M1,(max+ f))) . x < +infty
let x be object ; :: thesis: (Integral1 (M1,(max+ f))) . b1 < +infty
per cases ( x in dom (Integral1 (M1,(max+ f))) or not x in dom (Integral1 (M1,(max+ f))) ) ;
suppose x in dom (Integral1 (M1,(max+ f))) ; :: thesis: (Integral1 (M1,(max+ f))) . b1 < +infty
then reconsider x1 = x as Element of X2 ;
(Integral1 (M1,(max+ f))) . x = Integral (M1,(ProjPMap2 ((max+ f),x1))) by MESFUN12:def 7;
then A17: (Integral1 (M1,(max+ f))) . x = Integral (M1,(max+ (ProjPMap2 (f,x1)))) by MESFUN12:46;
A18: ProjPMap2 (f,x1) is_integrable_on M1 by A7;
then consider B being Element of S1 such that
A19: ( B = dom (ProjPMap2 (f,x1)) & ProjPMap2 (f,x1) is B -measurable ) by MESFUNC5:def 17;
A20: ( B = dom (max+ (ProjPMap2 (f,x1))) & max+ (ProjPMap2 (f,x1)) is B -measurable ) by A19, MESFUNC2:def 2, MESFUN11:10;
integral+ (M1,(max+ (ProjPMap2 (f,x1)))) < +infty by A18, MESFUNC5:def 17;
hence (Integral1 (M1,(max+ f))) . x < +infty by A17, A20, MESFUNC5:88, MESFUN11:5; :: thesis: verum
end;
end;
end;
now :: thesis: for x being object holds (Integral1 (M1,(max+ f))) . x > -infty
let x be object ; :: thesis: (Integral1 (M1,(max+ f))) . b1 > -infty
per cases ( x in dom (Integral1 (M1,(max+ f))) or not x in dom (Integral1 (M1,(max+ f))) ) ;
suppose x in dom (Integral1 (M1,(max+ f))) ; :: thesis: (Integral1 (M1,(max+ f))) . b1 > -infty
then reconsider x1 = x as Element of X2 ;
(Integral1 (M1,(max+ f))) . x = Integral (M1,(ProjPMap2 ((max+ f),x1))) by MESFUN12:def 7;
then A21: (Integral1 (M1,(max+ f))) . x = Integral (M1,(max+ (ProjPMap2 (f,x1)))) by MESFUN12:46;
ProjPMap2 (f,x1) is_integrable_on M1 by A7;
then consider B being Element of S1 such that
A22: ( B = dom (ProjPMap2 (f,x1)) & ProjPMap2 (f,x1) is B -measurable ) by MESFUNC5:def 17;
( B = dom (max+ (ProjPMap2 (f,x1))) & max+ (ProjPMap2 (f,x1)) is B -measurable ) by A22, MESFUNC2:def 2, MESFUN11:10;
hence (Integral1 (M1,(max+ f))) . x > -infty by A21, MESFUNC5:90, MESFUN11:5; :: thesis: verum
end;
end;
end;
then A23: ( Integral1 (M1,(max+ f)) is V158() & Integral1 (M1,(max+ f)) is V159() ) by A16, MESFUNC5:def 5, MESFUNC5:def 6;
then A24: dom ((Integral1 (M1,(max+ f))) - (Integral1 (M1,(max- f)))) = (dom (Integral1 (M1,(max+ f)))) /\ (dom (Integral1 (M1,(max- f)))) by MESFUN11:23;
TT: ( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral1 (M1,(max- f)) is_integrable_on M2 ) by A1, A2, A3, Th20;
then A25: ex A1 being Element of S2 st
( A1 = dom (Integral1 (M1,(max+ f))) & Integral1 (M1,(max+ f)) is A1 -measurable ) by MESFUNC5:def 17;
A26: ex A2 being Element of S2 st
( A2 = dom (Integral1 (M1,(max- f))) & Integral1 (M1,(max- f)) is A2 -measurable ) by TT, MESFUNC5:def 17;
now :: thesis: for x being object holds (Integral1 (M1,(max- f))) . x > -infty
let x be object ; :: thesis: (Integral1 (M1,(max- f))) . b1 > -infty
per cases ( x in dom (Integral1 (M1,(max- f))) or not x in dom (Integral1 (M1,(max- f))) ) ;
suppose x in dom (Integral1 (M1,(max- f))) ; :: thesis: (Integral1 (M1,(max- f))) . b1 > -infty
then reconsider x1 = x as Element of X2 ;
(Integral1 (M1,(max- f))) . x = Integral (M1,(ProjPMap2 ((max- f),x1))) by MESFUN12:def 7;
then A27: (Integral1 (M1,(max- f))) . x = Integral (M1,(max- (ProjPMap2 (f,x1)))) by MESFUN12:46;
ProjPMap2 (f,x1) is_integrable_on M1 by A7;
then consider B being Element of S1 such that
A28: ( B = dom (ProjPMap2 (f,x1)) & ProjPMap2 (f,x1) is B -measurable ) by MESFUNC5:def 17;
( B = dom (max- (ProjPMap2 (f,x1))) & max- (ProjPMap2 (f,x1)) is B -measurable ) by A28, MESFUNC2:def 3, MESFUN11:10;
hence (Integral1 (M1,(max- f))) . x > -infty by A27, MESFUNC5:90, MESFUN11:5; :: thesis: verum
end;
end;
end;
then Integral1 (M1,(max- f)) is V158() by MESFUNC5:def 5;
then A29: (Integral1 (M1,(max+ f))) - (Integral1 (M1,(max- f))) is XX2 -measurable by A15, A23, A24, A25, A26, MEASUR11:66;
now :: thesis: for x being Element of X2 st x in dom (Integral1 (M1,f)) holds
((Integral1 (M1,(max+ f))) - (Integral1 (M1,(max- f)))) . x = (Integral1 (M1,f)) . x
let x be Element of X2; :: thesis: ( x in dom (Integral1 (M1,f)) implies ((Integral1 (M1,(max+ f))) - (Integral1 (M1,(max- f)))) . x = (Integral1 (M1,f)) . x )
assume x in dom (Integral1 (M1,f)) ; :: thesis: ((Integral1 (M1,(max+ f))) - (Integral1 (M1,(max- f)))) . x = (Integral1 (M1,f)) . x
A30: (Integral1 (M1,f)) . x = Integral (M1,(ProjPMap2 (f,x))) by MESFUN12:def 7;
ProjPMap2 (f,x) is_integrable_on M1 by A7;
then B30: ex A being Element of S1 st
( A = dom (ProjPMap2 (f,x)) & ProjPMap2 (f,x) is A -measurable ) by MESFUNC5:def 17;
((Integral1 (M1,(max+ f))) - (Integral1 (M1,(max- f)))) . x = ((Integral1 (M1,(max+ f))) . x) - ((Integral1 (M1,(max- f))) . x) by A15, A24, MESFUNC1:def 4
.= (Integral (M1,(ProjPMap2 ((max+ f),x)))) - ((Integral1 (M1,(max- f))) . x) by MESFUN12:def 7
.= (Integral (M1,(ProjPMap2 ((max+ f),x)))) - (Integral (M1,(ProjPMap2 ((max- f),x)))) by MESFUN12:def 7
.= (Integral (M1,(max+ (ProjPMap2 (f,x))))) - (Integral (M1,(ProjPMap2 ((max- f),x)))) by MESFUN12:46
.= (Integral (M1,(max+ (ProjPMap2 (f,x))))) - (Integral (M1,(max- (ProjPMap2 (f,x))))) by MESFUN12:46 ;
hence ((Integral1 (M1,(max+ f))) - (Integral1 (M1,(max- f)))) . x = (Integral1 (M1,f)) . x by A30, B30, MESFUN11:54; :: thesis: verum
end;
then A31: Integral1 (M1,f) = (Integral1 (M1,(max+ f))) - (Integral1 (M1,(max- f))) by A15, A24, PARTFUN1:5;
hence for V being Element of S2 holds Integral1 (M1,f) is V -measurable by A29, MESFUNC1:30; :: thesis: ( Integral1 (M1,f) is_integrable_on M2 & Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral1 (M1,f) in L1_Functions M2 )
A32: ( X2 = dom (max+ (Integral1 (M1,f))) & X2 = dom (max- (Integral1 (M1,f))) ) by A15, MESFUNC2:def 2, MESFUNC2:def 3;
A33: ( max+ (Integral1 (M1,f)) is XX2 -measurable & max- (Integral1 (M1,f)) is XX2 -measurable ) by A15, A29, A31, MESFUNC2:25, MESFUNC2:26;
A34: Integral1 (M1,|.f.|) is_integrable_on M2 by A1, A2, A3, Th20;
now :: thesis: for x being Element of X2 st x in dom (max+ (Integral1 (M1,f))) holds
|.((max+ (Integral1 (M1,f))) . x).| <= (Integral1 (M1,|.f.|)) . x
let x be Element of X2; :: thesis: ( x in dom (max+ (Integral1 (M1,f))) implies |.((max+ (Integral1 (M1,f))) . x).| <= (Integral1 (M1,|.f.|)) . x )
assume x in dom (max+ (Integral1 (M1,f))) ; :: thesis: |.((max+ (Integral1 (M1,f))) . x).| <= (Integral1 (M1,|.f.|)) . x
then A35: x in dom |.(Integral1 (M1,f)).| by A15, A32, MESFUNC1:def 10;
(max+ (Integral1 (M1,f))) . x <= |.(Integral1 (M1,f)).| . x by Th29;
then (max+ (Integral1 (M1,f))) . x <= |.((Integral1 (M1,f)) . x).| by A35, MESFUNC1:def 10;
then A36: |.((max+ (Integral1 (M1,f))) . x).| <= |.((Integral1 (M1,f)) . x).| by EXTREAL1:3, MESFUNC2:12;
(Integral1 (M1,f)) . x = Integral (M1,(ProjPMap2 (f,x))) by MESFUN12:def 7;
then |.((Integral1 (M1,f)) . x).| <= Integral (M1,|.(ProjPMap2 (f,x)).|) by A7, MESFUNC5:101;
then |.((Integral1 (M1,f)) . x).| <= Integral (M1,(ProjPMap2 (|.f.|,x))) by Th27;
then |.((Integral1 (M1,f)) . x).| <= (Integral1 (M1,|.f.|)) . x by MESFUN12:def 7;
hence |.((max+ (Integral1 (M1,f))) . x).| <= (Integral1 (M1,|.f.|)) . x by A36, XXREAL_0:2; :: thesis: verum
end;
then A37: max+ (Integral1 (M1,f)) is_integrable_on M2 by A15, A32, A33, A34, MESFUNC5:102;
now :: thesis: for x being Element of X2 st x in dom (max- (Integral1 (M1,f))) holds
|.((max- (Integral1 (M1,f))) . x).| <= (Integral1 (M1,|.f.|)) . x
let x be Element of X2; :: thesis: ( x in dom (max- (Integral1 (M1,f))) implies |.((max- (Integral1 (M1,f))) . x).| <= (Integral1 (M1,|.f.|)) . x )
assume x in dom (max- (Integral1 (M1,f))) ; :: thesis: |.((max- (Integral1 (M1,f))) . x).| <= (Integral1 (M1,|.f.|)) . x
then A38: x in dom |.(Integral1 (M1,f)).| by A15, A32, MESFUNC1:def 10;
(max- (Integral1 (M1,f))) . x <= |.(Integral1 (M1,f)).| . x by Th29;
then (max- (Integral1 (M1,f))) . x <= |.((Integral1 (M1,f)) . x).| by A38, MESFUNC1:def 10;
then A39: |.((max- (Integral1 (M1,f))) . x).| <= |.((Integral1 (M1,f)) . x).| by EXTREAL1:3, MESFUNC2:13;
(Integral1 (M1,f)) . x = Integral (M1,(ProjPMap2 (f,x))) by MESFUN12:def 7;
then |.((Integral1 (M1,f)) . x).| <= Integral (M1,|.(ProjPMap2 (f,x)).|) by A7, MESFUNC5:101;
then |.((Integral1 (M1,f)) . x).| <= Integral (M1,(ProjPMap2 (|.f.|,x))) by Th27;
then |.((Integral1 (M1,f)) . x).| <= (Integral1 (M1,|.f.|)) . x by MESFUN12:def 7;
hence |.((max- (Integral1 (M1,f))) . x).| <= (Integral1 (M1,|.f.|)) . x by A39, XXREAL_0:2; :: thesis: verum
end;
then max- (Integral1 (M1,f)) is_integrable_on M2 by A15, A32, A33, A34, MESFUNC5:102;
then (max+ (Integral1 (M1,f))) - (max- (Integral1 (M1,f))) is_integrable_on M2 by A37, MESFUN10:12;
hence A40: Integral1 (M1,f) is_integrable_on M2 by MESFUNC2:23; :: thesis: ( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral1 (M1,f) in L1_Functions M2 )
A41: ( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;
A42: ( dom (max+ f) = A & dom (max- f) = A ) by A5, MESFUNC2:def 2, MESFUNC2:def 3;
A43: ( max+ f is A -measurable & max- f is A -measurable ) by A5, MESFUNC2:25, MESFUNC2:26;
then A44: Integral ((Prod_Measure (M1,M2)),(max- f)) = Integral (M2,(Integral1 (M1,(max- f)))) by A1, A2, A41, A42, MESFUN12:84;
Integral ((Prod_Measure (M1,M2)),f) = (Integral ((Prod_Measure (M1,M2)),(max+ f))) - (Integral ((Prod_Measure (M1,M2)),(max- f))) by A5, MESFUN11:54
.= (Integral (M2,((Integral1 (M1,(max+ f))) | XX2))) - (Integral (M2,((Integral1 (M1,(max- f))) | XX2))) by A1, A2, A41, A42, A43, A44, MESFUN12:84 ;
hence Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) by A15, A24, A31, TT, Th21; :: thesis: Integral1 (M1,f) in L1_Functions M2
now :: thesis: for y being set st y in rng (Integral1 (M1,f)) holds
y in REAL
let y be set ; :: thesis: ( y in rng (Integral1 (M1,f)) implies y in REAL )
assume y in rng (Integral1 (M1,f)) ; :: thesis: y in REAL
then consider x being Element of X2 such that
A45: ( x in dom (Integral1 (M1,f)) & y = (Integral1 (M1,f)) . x ) by PARTFUN1:3;
(Integral1 (M1,f)) . x = Integral (M1,(ProjPMap2 (f,x))) by MESFUN12:def 7;
then |.((Integral1 (M1,f)) . x).| <= Integral (M1,|.(ProjPMap2 (f,x)).|) by A7, MESFUNC5:101;
then |.((Integral1 (M1,f)) . x).| <= Integral (M1,(ProjPMap2 (|.f.|,x))) by Th27;
then |.((Integral1 (M1,f)) . x).| <= (Integral1 (M1,|.f.|)) . x by MESFUN12:def 7;
then |.((Integral1 (M1,f)) . x).| < +infty by A4, XXREAL_0:2;
hence y in REAL by A45, EXTREAL1:41; :: thesis: verum
end;
then rng (Integral1 (M1,f)) c= REAL ;
then reconsider F = Integral1 (M1,f) as PartFunc of X2,REAL by RELSET_1:6;
reconsider ND = {} as Element of S2 by MEASURE1:7;
A46: M2 . ND = 0 by VALUED_0:def 19;
ND ` = X2 \ {} by SUBSET_1:def 4
.= X2 ;
then A47: dom F = ND ` by FUNCT_2:def 1;
R_EAL F is_integrable_on M2 by A40, MESFUNC5:def 7;
then F is_integrable_on M2 by MESFUNC6:def 4;
then F in { f where f is PartFunc of X2,REAL : ex ND being Element of S2 st
( M2 . ND = 0 & dom f = ND ` & f is_integrable_on M2 ) } by A46, A47;
hence Integral1 (M1,f) in L1_Functions M2 by LPSPACE1:def 8; :: thesis: verum