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 PartFunc of [:X1,X2:],ExtREAL
for SX1 being Element of S1 st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) & X1 = SX1 holds
ex U being Element of S1 st
( M1 . U = 0 & ( for x being Element of X1 st x in U ` holds
ProjPMap1 (f,x) is_integrable_on M2 ) & (Integral2 (M2,|.f.|)) | (U `) is PartFunc of X1,REAL & Integral2 (M2,f) is SX1 \ U -measurable & (Integral2 (M2,f)) | (U `) is_integrable_on M1 & (Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) )
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 PartFunc of [:X1,X2:],ExtREAL
for SX1 being Element of S1 st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) & X1 = SX1 holds
ex U being Element of S1 st
( M1 . U = 0 & ( for x being Element of X1 st x in U ` holds
ProjPMap1 (f,x) is_integrable_on M2 ) & (Integral2 (M2,|.f.|)) | (U `) is PartFunc of X1,REAL & Integral2 (M2,f) is SX1 \ U -measurable & (Integral2 (M2,f)) | (U `) is_integrable_on M1 & (Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) )
let S2 be 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
for SX1 being Element of S1 st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) & X1 = SX1 holds
ex U being Element of S1 st
( M1 . U = 0 & ( for x being Element of X1 st x in U ` holds
ProjPMap1 (f,x) is_integrable_on M2 ) & (Integral2 (M2,|.f.|)) | (U `) is PartFunc of X1,REAL & Integral2 (M2,f) is SX1 \ U -measurable & (Integral2 (M2,f)) | (U `) is_integrable_on M1 & (Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) )
let M1 be sigma_Measure of S1; for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for SX1 being Element of S1 st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) & X1 = SX1 holds
ex U being Element of S1 st
( M1 . U = 0 & ( for x being Element of X1 st x in U ` holds
ProjPMap1 (f,x) is_integrable_on M2 ) & (Integral2 (M2,|.f.|)) | (U `) is PartFunc of X1,REAL & Integral2 (M2,f) is SX1 \ U -measurable & (Integral2 (M2,f)) | (U `) is_integrable_on M1 & (Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) )
let M2 be sigma_Measure of S2; for f being PartFunc of [:X1,X2:],ExtREAL
for SX1 being Element of S1 st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) & X1 = SX1 holds
ex U being Element of S1 st
( M1 . U = 0 & ( for x being Element of X1 st x in U ` holds
ProjPMap1 (f,x) is_integrable_on M2 ) & (Integral2 (M2,|.f.|)) | (U `) is PartFunc of X1,REAL & Integral2 (M2,f) is SX1 \ U -measurable & (Integral2 (M2,f)) | (U `) is_integrable_on M1 & (Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) )
let f be PartFunc of [:X1,X2:],ExtREAL; for SX1 being Element of S1 st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) & X1 = SX1 holds
ex U being Element of S1 st
( M1 . U = 0 & ( for x being Element of X1 st x in U ` holds
ProjPMap1 (f,x) is_integrable_on M2 ) & (Integral2 (M2,|.f.|)) | (U `) is PartFunc of X1,REAL & Integral2 (M2,f) is SX1 \ U -measurable & (Integral2 (M2,f)) | (U `) is_integrable_on M1 & (Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) )
let SX1 be Element of S1; ( M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on Prod_Measure (M1,M2) & X1 = SX1 implies ex U being Element of S1 st
( M1 . U = 0 & ( for x being Element of X1 st x in U ` holds
ProjPMap1 (f,x) is_integrable_on M2 ) & (Integral2 (M2,|.f.|)) | (U `) is PartFunc of X1,REAL & Integral2 (M2,f) is SX1 \ U -measurable & (Integral2 (M2,f)) | (U `) is_integrable_on M1 & (Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) ) )
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:
X1 = SX1
; ex U being Element of S1 st
( M1 . U = 0 & ( for x being Element of X1 st x in U ` holds
ProjPMap1 (f,x) is_integrable_on M2 ) & (Integral2 (M2,|.f.|)) | (U `) is PartFunc of X1,REAL & Integral2 (M2,f) is SX1 \ U -measurable & (Integral2 (M2,f)) | (U `) is_integrable_on M1 & (Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) )
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.| & A = dom (max+ f) & A = dom (max- f) )
by A5, MESFUNC1:def 10, MESFUNC2:def 2, MESFUNC2:def 3;
A7:
( |.f.| is A -measurable & max+ f is A -measurable & max- f is A -measurable )
by A5, MESFUNC2:25, MESFUNC2:26, MESFUNC2:27;
A8:
( Integral2 (M2,|.f.|) is_integrable_on M1 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral2 (M2,(max- f)) is_integrable_on M1 )
by A1, A2, A3, Th20;
A9:
( max+ f is nonnegative & max- f is nonnegative )
by MESFUN11:5;
Integral2 (M2,|.f.|) is_a.e.finite M1
by A8, Th19;
then consider U being Element of S1 such that
A10:
( M1 . U = 0 & (Integral2 (M2,|.f.|)) | (U `) is PartFunc of X1,REAL )
;
A11:
U ` = SX1 \ U
by A4, SUBSET_1:def 4;
then A12:
( (Integral2 (M2,|.f.|)) | (U `) is_integrable_on M1 & (Integral2 (M2,(max+ f))) | (U `) is_integrable_on M1 & (Integral2 (M2,(max- f))) | (U `) is_integrable_on M1 )
by A8, MESFUNC5:97;
A13:
( dom (Integral2 (M2,f)) = X1 & dom (Integral2 (M2,(max+ f))) = X1 & dom (Integral2 (M2,(max- f))) = X1 & dom (Integral2 (M2,|.f.|)) = X1 )
by FUNCT_2:def 1;
take
U
; ( M1 . U = 0 & ( for x being Element of X1 st x in U ` holds
ProjPMap1 (f,x) is_integrable_on M2 ) & (Integral2 (M2,|.f.|)) | (U `) is PartFunc of X1,REAL & Integral2 (M2,f) is SX1 \ U -measurable & (Integral2 (M2,f)) | (U `) is_integrable_on M1 & (Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) )
thus
M1 . U = 0
by A10; ( ( for x being Element of X1 st x in U ` holds
ProjPMap1 (f,x) is_integrable_on M2 ) & (Integral2 (M2,|.f.|)) | (U `) is PartFunc of X1,REAL & Integral2 (M2,f) is SX1 \ U -measurable & (Integral2 (M2,f)) | (U `) is_integrable_on M1 & (Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) )
thus A14:
for x being Element of X1 st x in U ` holds
ProjPMap1 (f,x) is_integrable_on M2
( (Integral2 (M2,|.f.|)) | (U `) is PartFunc of X1,REAL & Integral2 (M2,f) is SX1 \ U -measurable & (Integral2 (M2,f)) | (U `) is_integrable_on M1 & (Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) )proof
let x be
Element of
X1;
( x in U ` implies ProjPMap1 (f,x) is_integrable_on M2 )
assume A15:
x in U `
;
ProjPMap1 (f,x) is_integrable_on M2
then A16:
x in dom ((Integral2 (M2,|.f.|)) | (U `))
by A13, RELAT_1:57;
X-section (
A,
x)
= Measurable-X-section (
A,
x)
by MEASUR11:def 6;
then A17:
(
dom (ProjPMap1 (|.f.|,x)) = Measurable-X-section (
A,
x) &
dom (ProjPMap1 (f,x)) = Measurable-X-section (
A,
x) )
by A5, A6, MESFUN12:def 3;
A18:
(
ProjPMap1 (
|.f.|,
x) is
Measurable-X-section (
A,
x)
-measurable &
ProjPMap1 (
f,
x) is
Measurable-X-section (
A,
x)
-measurable )
by A5, A6, A7, MESFUN12:47;
A19:
ProjPMap1 (
|.f.|,
x)
= |.(ProjPMap1 (f,x)).|
by Th27;
then integral+ (
M2,
(max+ (ProjPMap1 (|.f.|,x)))) =
integral+ (
M2,
(ProjPMap1 (|.f.|,x)))
by MESFUN11:31
.=
Integral (
M2,
(ProjPMap1 (|.f.|,x)))
by A6, A7, A17, A19, MESFUN12:47, MESFUNC5:88
.=
(Integral2 (M2,|.f.|)) . x
by MESFUN12:def 8
.=
((Integral2 (M2,|.f.|)) | (U `)) . x
by A15, FUNCT_1:49
;
then A20:
integral+ (
M2,
(max+ (ProjPMap1 (|.f.|,x))))
< +infty
by A10, A16, PARTFUN1:4, XXREAL_0:9;
integral+ (
M2,
(max- (ProjPMap1 (|.f.|,x))))
< +infty
by A17, A18, A19, MESFUN11:53;
then
|.(ProjPMap1 (f,x)).| is_integrable_on M2
by A6, A7, A17, A19, A20, MESFUN12:47, MESFUNC5:def 17;
hence
ProjPMap1 (
f,
x)
is_integrable_on M2
by A17, A18, MESFUNC5:100;
verum
end;
thus
(Integral2 (M2,|.f.|)) | (U `) is PartFunc of X1,REAL
by A10; ( Integral2 (M2,f) is SX1 \ U -measurable & (Integral2 (M2,f)) | (U `) is_integrable_on M1 & (Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) )
set G1 = (Integral2 (M2,(max+ f))) | (U `);
set G2 = (Integral2 (M2,(max- f))) | (U `);
reconsider G = ((Integral2 (M2,(max+ f))) | (U `)) - ((Integral2 (M2,(max- f))) | (U `)) as PartFunc of X1,ExtREAL ;
A21:
( dom ((Integral2 (M2,(max+ f))) | (U `)) = U ` & dom ((Integral2 (M2,(max- f))) | (U `)) = U ` )
by A13, RELAT_1:62;
A22:
now for x being object holds ((Integral2 (M2,(max+ f))) | (U `)) . x < +infty let x be
object ;
((Integral2 (M2,(max+ f))) | (U `)) . b1 < +infty per cases
( x in dom ((Integral2 (M2,(max+ f))) | (U `)) or not x in dom ((Integral2 (M2,(max+ f))) | (U `)) )
;
suppose A23:
x in dom ((Integral2 (M2,(max+ f))) | (U `))
;
((Integral2 (M2,(max+ f))) | (U `)) . b1 < +infty then reconsider x1 =
x as
Element of
X1 ;
A24:
((Integral2 (M2,(max+ f))) | (U `)) . x =
(Integral2 (M2,(max+ f))) . x
by A21, A23, FUNCT_1:49
.=
Integral (
M2,
(ProjPMap1 ((max+ f),x1)))
by MESFUN12:def 8
.=
Integral (
M2,
(max+ (ProjPMap1 (f,x1))))
by MESFUN12:45
;
A25:
ProjPMap1 (
f,
x1)
is_integrable_on M2
by A14, A21, A23;
then consider B being
Element of
S2 such that A26:
(
B = dom (ProjPMap1 (f,x1)) &
ProjPMap1 (
f,
x1) is
B -measurable )
by MESFUNC5:def 17;
A27:
(
B = dom (max+ (ProjPMap1 (f,x1))) &
max+ (ProjPMap1 (f,x1)) is
B -measurable )
by A26, MESFUNC2:def 2, MESFUN11:10;
integral+ (
M2,
(max+ (ProjPMap1 (f,x1))))
< +infty
by A25, MESFUNC5:def 17;
hence
((Integral2 (M2,(max+ f))) | (U `)) . x < +infty
by A24, A27, MESFUNC5:88, MESFUN11:5;
verum end; end; end;
now for x being object holds ((Integral2 (M2,(max+ f))) | (U `)) . x > -infty let x be
object ;
((Integral2 (M2,(max+ f))) | (U `)) . b1 > -infty per cases
( x in dom ((Integral2 (M2,(max+ f))) | (U `)) or not x in dom ((Integral2 (M2,(max+ f))) | (U `)) )
;
suppose A28:
x in dom ((Integral2 (M2,(max+ f))) | (U `))
;
((Integral2 (M2,(max+ f))) | (U `)) . b1 > -infty then reconsider x1 =
x as
Element of
X1 ;
A29:
((Integral2 (M2,(max+ f))) | (U `)) . x =
(Integral2 (M2,(max+ f))) . x
by A21, A28, FUNCT_1:49
.=
Integral (
M2,
(ProjPMap1 ((max+ f),x1)))
by MESFUN12:def 8
.=
Integral (
M2,
(max+ (ProjPMap1 (f,x1))))
by MESFUN12:45
;
ProjPMap1 (
f,
x1)
is_integrable_on M2
by A14, A21, A28;
then consider B being
Element of
S2 such that A30:
(
B = dom (ProjPMap1 (f,x1)) &
ProjPMap1 (
f,
x1) is
B -measurable )
by MESFUNC5:def 17;
(
B = dom (max+ (ProjPMap1 (f,x1))) &
max+ (ProjPMap1 (f,x1)) is
B -measurable )
by A30, MESFUNC2:def 2, MESFUN11:10;
hence
((Integral2 (M2,(max+ f))) | (U `)) . x > -infty
by A29, MESFUNC5:90, MESFUN11:5;
verum end; end; end;
then A31:
( (Integral2 (M2,(max+ f))) | (U `) is V158() & (Integral2 (M2,(max+ f))) | (U `) is V159() )
by A22, MESFUNC5:def 5, MESFUNC5:def 6;
then A32:
dom G = (dom ((Integral2 (M2,(max+ f))) | (U `))) /\ (dom ((Integral2 (M2,(max- f))) | (U `)))
by MESFUN11:23;
A33:
ex A1 being Element of S1 st
( A1 = dom ((Integral2 (M2,(max+ f))) | (U `)) & (Integral2 (M2,(max+ f))) | (U `) is A1 -measurable )
by A12, MESFUNC5:def 17;
A34:
ex A2 being Element of S1 st
( A2 = dom ((Integral2 (M2,(max- f))) | (U `)) & (Integral2 (M2,(max- f))) | (U `) is A2 -measurable )
by A12, MESFUNC5:def 17;
now for x being object holds ((Integral2 (M2,(max- f))) | (U `)) . x > -infty let x be
object ;
((Integral2 (M2,(max- f))) | (U `)) . b1 > -infty per cases
( x in dom ((Integral2 (M2,(max- f))) | (U `)) or not x in dom ((Integral2 (M2,(max- f))) | (U `)) )
;
suppose A35:
x in dom ((Integral2 (M2,(max- f))) | (U `))
;
((Integral2 (M2,(max- f))) | (U `)) . b1 > -infty then reconsider x1 =
x as
Element of
X1 ;
A36:
((Integral2 (M2,(max- f))) | (U `)) . x =
(Integral2 (M2,(max- f))) . x
by A21, A35, FUNCT_1:49
.=
Integral (
M2,
(ProjPMap1 ((max- f),x1)))
by MESFUN12:def 8
.=
Integral (
M2,
(max- (ProjPMap1 (f,x1))))
by MESFUN12:45
;
ProjPMap1 (
f,
x1)
is_integrable_on M2
by A14, A21, A35;
then consider B being
Element of
S2 such that A37:
(
B = dom (ProjPMap1 (f,x1)) &
ProjPMap1 (
f,
x1) is
B -measurable )
by MESFUNC5:def 17;
(
B = dom (max- (ProjPMap1 (f,x1))) &
max- (ProjPMap1 (f,x1)) is
B -measurable )
by A37, MESFUNC2:def 3, MESFUN11:10;
hence
((Integral2 (M2,(max- f))) | (U `)) . x > -infty
by A36, MESFUNC5:90, MESFUN11:5;
verum end; end; end;
then
(Integral2 (M2,(max- f))) | (U `) is V158()
by MESFUNC5:def 5;
then A38:
G is SX1 \ U -measurable
by A11, A21, A31, A32, A33, A34, MEASUR11:66;
A39:
( dom ((Integral2 (M2,f)) | (U `)) = U ` & dom (G | (U `)) = U ` & dom ((Integral2 (M2,|.f.|)) | (U `)) = U ` )
by A13, A21, A32, RELAT_1:62;
then A40:
( U ` = dom (max+ ((Integral2 (M2,f)) | (U `))) & U ` = dom (max- ((Integral2 (M2,f)) | (U `))) )
by MESFUNC2:def 2, MESFUNC2:def 3;
A41:
now for x being Element of X1 st x in dom ((Integral2 (M2,f)) | (U `)) holds
((Integral2 (M2,f)) | (U `)) . x = (G | (U `)) . xlet x be
Element of
X1;
( x in dom ((Integral2 (M2,f)) | (U `)) implies ((Integral2 (M2,f)) | (U `)) . x = (G | (U `)) . x )assume A42:
x in dom ((Integral2 (M2,f)) | (U `))
;
((Integral2 (M2,f)) | (U `)) . x = (G | (U `)) . xthen A43:
x in U `
by A13, RELAT_1:62;
then A44:
((Integral2 (M2,f)) | (U `)) . x =
(Integral2 (M2,f)) . x
by FUNCT_1:49
.=
Integral (
M2,
(ProjPMap1 (f,x)))
by MESFUN12:def 8
;
X-section (
A,
x)
= Measurable-X-section (
A,
x)
by MEASUR11:def 6;
then B17:
(
dom (ProjPMap1 (|.f.|,x)) = Measurable-X-section (
A,
x) &
dom (ProjPMap1 (f,x)) = Measurable-X-section (
A,
x) )
by A5, A6, MESFUN12:def 3;
x in dom G
by A21, A32, A42, RELAT_1:57;
then (G | (U `)) . x =
(((Integral2 (M2,(max+ f))) | (U `)) . x) - (((Integral2 (M2,(max- f))) | (U `)) . x)
by A21, A32, MESFUNC1:def 4
.=
((Integral2 (M2,(max+ f))) . x) - (((Integral2 (M2,(max- f))) | (U `)) . x)
by A43, FUNCT_1:49
.=
((Integral2 (M2,(max+ f))) . x) - ((Integral2 (M2,(max- f))) . x)
by A43, FUNCT_1:49
.=
(Integral (M2,(ProjPMap1 ((max+ f),x)))) - ((Integral2 (M2,(max- f))) . x)
by MESFUN12:def 8
.=
(Integral (M2,(ProjPMap1 ((max+ f),x)))) - (Integral (M2,(ProjPMap1 ((max- f),x))))
by MESFUN12:def 8
.=
(Integral (M2,(max+ (ProjPMap1 (f,x))))) - (Integral (M2,(ProjPMap1 ((max- f),x))))
by MESFUN12:45
.=
(Integral (M2,(max+ (ProjPMap1 (f,x))))) - (Integral (M2,(max- (ProjPMap1 (f,x)))))
by MESFUN12:45
.=
Integral (
M2,
(ProjPMap1 (f,x)))
by A5, B17, MESFUN12:47, MESFUN11:54
;
hence
((Integral2 (M2,f)) | (U `)) . x = (G | (U `)) . x
by A44;
verum end;
hence
Integral2 (M2,f) is SX1 \ U -measurable
by A11, A13, A21, A32, A38, A39, PARTFUN1:5, MESFUN12:36; ( (Integral2 (M2,f)) | (U `) is_integrable_on M1 & (Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) )
(Integral2 (M2,f)) | (U `) is SX1 \ U -measurable
by A13, A21, A32, A38, A41, RELAT_1:62, PARTFUN1:5;
then A45:
( max+ ((Integral2 (M2,f)) | (U `)) is SX1 \ U -measurable & max- ((Integral2 (M2,f)) | (U `)) is SX1 \ U -measurable )
by A11, A39, MESFUNC2:25, MESFUNC2:26;
now for y being set st y in rng ((Integral2 (M2,f)) | (U `)) holds
y in REAL let y be
set ;
( y in rng ((Integral2 (M2,f)) | (U `)) implies y in REAL )assume
y in rng ((Integral2 (M2,f)) | (U `))
;
y in REAL then consider x being
Element of
X1 such that A47:
(
x in dom ((Integral2 (M2,f)) | (U `)) &
y = ((Integral2 (M2,f)) | (U `)) . x )
by PARTFUN1:3;
A48:
(
x in dom (Integral2 (M2,f)) &
x in U ` )
by A47, RELAT_1:57;
then
x in dom ((Integral2 (M2,|.f.|)) | (U `))
by A13, RELAT_1:57;
then A49:
((Integral2 (M2,|.f.|)) | (U `)) . x < +infty
by A10, PARTFUN1:4, XXREAL_0:9;
(Integral2 (M2,f)) . x = Integral (
M2,
(ProjPMap1 (f,x)))
by MESFUN12:def 8;
then
|.((Integral2 (M2,f)) . x).| <= Integral (
M2,
|.(ProjPMap1 (f,x)).|)
by A14, A48, MESFUNC5:101;
then
|.((Integral2 (M2,f)) . x).| <= Integral (
M2,
(ProjPMap1 (|.f.|,x)))
by Th27;
then
|.((Integral2 (M2,f)) . x).| <= (Integral2 (M2,|.f.|)) . x
by MESFUN12:def 8;
then
|.((Integral2 (M2,f)) . x).| <= ((Integral2 (M2,|.f.|)) | (U `)) . x
by A48, FUNCT_1:49;
then
|.(((Integral2 (M2,f)) | (U `)) . x).| <= ((Integral2 (M2,|.f.|)) | (U `)) . x
by A47, FUNCT_1:47;
then
|.(((Integral2 (M2,f)) | (U `)) . x).| < +infty
by A49, XXREAL_0:2;
hence
y in REAL
by A47, EXTREAL1:41;
verum end;
then A50:
rng ((Integral2 (M2,f)) | (U `)) c= REAL
;
now for x being Element of X1 st x in dom (max+ ((Integral2 (M2,f)) | (U `))) holds
|.((max+ ((Integral2 (M2,f)) | (U `))) . x).| <= ((Integral2 (M2,|.f.|)) | (U `)) . xlet x be
Element of
X1;
( x in dom (max+ ((Integral2 (M2,f)) | (U `))) implies |.((max+ ((Integral2 (M2,f)) | (U `))) . x).| <= ((Integral2 (M2,|.f.|)) | (U `)) . x )assume A51:
x in dom (max+ ((Integral2 (M2,f)) | (U `)))
;
|.((max+ ((Integral2 (M2,f)) | (U `))) . x).| <= ((Integral2 (M2,|.f.|)) | (U `)) . xthen A52:
(
x in dom (Integral2 (M2,f)) &
x in U ` )
by A13, A39, MESFUNC2:def 2;
then A53:
x in dom (max+ (Integral2 (M2,f)))
by MESFUNC2:def 2;
A54:
x in dom |.(Integral2 (M2,f)).|
by A52, MESFUNC1:def 10;
(max+ ((Integral2 (M2,f)) | (U `))) . x =
max (
(((Integral2 (M2,f)) | (U `)) . x),
0)
by A51, MESFUNC2:def 2
.=
max (
((Integral2 (M2,f)) . x),
0)
by A39, A40, A51, FUNCT_1:47
.=
(max+ (Integral2 (M2,f))) . x
by A53, MESFUNC2:def 2
;
then
(max+ ((Integral2 (M2,f)) | (U `))) . x <= |.(Integral2 (M2,f)).| . x
by Th29;
then
(max+ ((Integral2 (M2,f)) | (U `))) . x <= |.((Integral2 (M2,f)) . x).|
by A54, MESFUNC1:def 10;
then A55:
|.((max+ ((Integral2 (M2,f)) | (U `))) . x).| <= |.((Integral2 (M2,f)) . x).|
by EXTREAL1:3, MESFUNC2:12;
(Integral2 (M2,f)) . x = Integral (
M2,
(ProjPMap1 (f,x)))
by MESFUN12:def 8;
then
|.((Integral2 (M2,f)) . x).| <= Integral (
M2,
|.(ProjPMap1 (f,x)).|)
by A14, A40, A51, MESFUNC5:101;
then
|.((Integral2 (M2,f)) . x).| <= Integral (
M2,
(ProjPMap1 (|.f.|,x)))
by Th27;
then
|.((Integral2 (M2,f)) . x).| <= (Integral2 (M2,|.f.|)) . x
by MESFUN12:def 8;
then
|.((Integral2 (M2,f)) . x).| <= ((Integral2 (M2,|.f.|)) | (U `)) . x
by A40, A51, FUNCT_1:49;
hence
|.((max+ ((Integral2 (M2,f)) | (U `))) . x).| <= ((Integral2 (M2,|.f.|)) | (U `)) . x
by A55, XXREAL_0:2;
verum end;
then A56:
max+ ((Integral2 (M2,f)) | (U `)) is_integrable_on M1
by A11, A12, A39, A45, A40, MESFUNC5:102;
now for x being Element of X1 st x in dom (max- ((Integral2 (M2,f)) | (U `))) holds
|.((max- ((Integral2 (M2,f)) | (U `))) . x).| <= ((Integral2 (M2,|.f.|)) | (U `)) . xlet x be
Element of
X1;
( x in dom (max- ((Integral2 (M2,f)) | (U `))) implies |.((max- ((Integral2 (M2,f)) | (U `))) . x).| <= ((Integral2 (M2,|.f.|)) | (U `)) . x )assume A57:
x in dom (max- ((Integral2 (M2,f)) | (U `)))
;
|.((max- ((Integral2 (M2,f)) | (U `))) . x).| <= ((Integral2 (M2,|.f.|)) | (U `)) . xthen A58:
(
x in dom (Integral2 (M2,f)) &
x in U ` )
by A13, A39, MESFUNC2:def 3;
then A59:
x in dom (max- (Integral2 (M2,f)))
by MESFUNC2:def 3;
A60:
x in dom |.(Integral2 (M2,f)).|
by A58, MESFUNC1:def 10;
(max- ((Integral2 (M2,f)) | (U `))) . x =
max (
(- (((Integral2 (M2,f)) | (U `)) . x)),
0)
by A57, MESFUNC2:def 3
.=
max (
(- ((Integral2 (M2,f)) . x)),
0)
by A39, A40, A57, FUNCT_1:47
.=
(max- (Integral2 (M2,f))) . x
by A59, MESFUNC2:def 3
;
then
(max- ((Integral2 (M2,f)) | (U `))) . x <= |.(Integral2 (M2,f)).| . x
by Th29;
then
(max- ((Integral2 (M2,f)) | (U `))) . x <= |.((Integral2 (M2,f)) . x).|
by A60, MESFUNC1:def 10;
then A61:
|.((max- ((Integral2 (M2,f)) | (U `))) . x).| <= |.((Integral2 (M2,f)) . x).|
by EXTREAL1:3, MESFUNC2:13;
(Integral2 (M2,f)) . x = Integral (
M2,
(ProjPMap1 (f,x)))
by MESFUN12:def 8;
then
|.((Integral2 (M2,f)) . x).| <= Integral (
M2,
|.(ProjPMap1 (f,x)).|)
by A14, A40, A57, MESFUNC5:101;
then
|.((Integral2 (M2,f)) . x).| <= Integral (
M2,
(ProjPMap1 (|.f.|,x)))
by Th27;
then
|.((Integral2 (M2,f)) . x).| <= (Integral2 (M2,|.f.|)) . x
by MESFUN12:def 8;
then
|.((Integral2 (M2,f)) . x).| <= ((Integral2 (M2,|.f.|)) | (U `)) . x
by A40, A57, FUNCT_1:49;
hence
|.((max- ((Integral2 (M2,f)) | (U `))) . x).| <= ((Integral2 (M2,|.f.|)) | (U `)) . x
by A61, XXREAL_0:2;
verum end;
then
max- ((Integral2 (M2,f)) | (U `)) is_integrable_on M1
by A11, A12, A39, A45, A40, MESFUNC5:102;
then
(max+ ((Integral2 (M2,f)) | (U `))) - (max- ((Integral2 (M2,f)) | (U `))) is_integrable_on M1
by A56, MESFUN10:12;
hence A62:
(Integral2 (M2,f)) | (U `) is_integrable_on M1
by MESFUNC2:23; ( (Integral2 (M2,f)) | (U `) in L1_Functions M1 & ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) ) )
reconsider F = (Integral2 (M2,f)) | (U `) as PartFunc of X1,REAL by A50, RELSET_1:6;
R_EAL F is_integrable_on M1
by A62, MESFUNC5:def 7;
then
F is_integrable_on M1
by MESFUNC6:def 4;
then
F in { f where f is PartFunc of X1,REAL : ex ND being Element of S1 st
( M1 . ND = 0 & dom f = ND ` & f is_integrable_on M1 ) }
by A10, A39;
hence
(Integral2 (M2,f)) | (U `) in L1_Functions M1
by LPSPACE1:def 8; ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) )
consider g1 being PartFunc of X1,ExtREAL such that
A64:
( dom g1 = dom (Integral2 (M2,(max+ f))) & g1 | (U `) = (Integral2 (M2,(max+ f))) | (U `) & g1 is_integrable_on M1 & Integral (M1,g1) = Integral (M1,((Integral2 (M2,(max+ f))) | (U `))) )
by A8, A10, A11, A13, Th23, MESFUNC5:97;
consider g2 being PartFunc of X1,ExtREAL such that
A65:
( dom g2 = dom (Integral2 (M2,(max- f))) & g2 | (U `) = (Integral2 (M2,(max- f))) | (U `) & g2 is_integrable_on M1 & Integral (M1,g2) = Integral (M1,((Integral2 (M2,(max- f))) | (U `))) )
by A8, A10, A11, A13, Th23, MESFUNC5:97;
consider g being PartFunc of X1,ExtREAL such that
A66:
( dom g = dom (Integral2 (M2,f)) & g | (U `) = (Integral2 (M2,f)) | (U `) & g is_integrable_on M1 & Integral (M1,g) = Integral (M1,((Integral2 (M2,f)) | (U `))) )
by A10, A13, A62, Th23;
reconsider g = g as Function of X1,ExtREAL by A13, A66, FUNCT_2:def 1;
A67:
( dom (g | (U `)) = (dom g) /\ (U `) & dom (g1 | (U `)) = (dom g1) /\ (U `) & dom (g2 | (U `)) = (dom g2) /\ (U `) )
by RELAT_1:61;
now for x being Element of X1 st x in dom (g2 | (U `)) holds
|.((g2 | (U `)) . x).| < +infty let x be
Element of
X1;
( x in dom (g2 | (U `)) implies |.((g2 | (U `)) . x).| < +infty )assume A72:
x in dom (g2 | (U `))
;
|.((g2 | (U `)) . x).| < +infty then A68:
x in U `
by RELAT_1:57;
A69:
ProjPMap1 (
f,
x)
is_integrable_on M2
by A14, A72, RELAT_1:57;
then consider DP being
Element of
S2 such that A70:
(
DP = dom (ProjPMap1 (f,x)) &
ProjPMap1 (
f,
x) is
DP -measurable )
by MESFUNC5:def 17;
A71:
(
DP = dom (max- (ProjPMap1 (f,x))) &
max- (ProjPMap1 (f,x)) is
DP -measurable )
by A70, MESFUNC2:def 3, MESFUNC2:26;
A73:
max- (ProjPMap1 (f,x)) is
nonnegative
by MESFUN11:5;
A74:
(g2 | (U `)) . x =
(Integral2 (M2,(max- f))) . x
by A65, A68, FUNCT_1:49
.=
Integral (
M2,
(ProjPMap1 ((max- f),x)))
by MESFUN12:def 8
.=
Integral (
M2,
(max- (ProjPMap1 (f,x))))
by MESFUN12:45
.=
integral+ (
M2,
(max- (ProjPMap1 (f,x))))
by A71, MESFUNC5:88, MESFUN11:5
;
then
(g2 | (U `)) . x < +infty
by A69, MESFUNC5:def 17;
hence
|.((g2 | (U `)) . x).| < +infty
by A71, A73, A74, MESFUNC5:79, EXTREAL1:def 1;
verum end;
then
g2 | (U `) is V70()
by MESFUNC2:def 1;
then A75:
dom ((g1 | (U `)) - (g2 | (U `))) = ((dom g1) /\ (U `)) /\ ((dom g2) /\ (U `))
by A67, MESFUNC2:2;
then A76:
dom ((g1 | (U `)) - (g2 | (U `))) = dom (g | (U `))
by A13, A64, A65, A66, RELAT_1:61;
( dom (g1 | (U `)) = U ` & dom (g2 | (U `)) = U ` )
by A13, A64, A65, RELAT_1:62;
then A77:
U ` = (dom (g1 | (U `))) /\ (dom (g2 | (U `)))
;
A78:
( g1 | (U `) is_integrable_on M1 & g2 | (U `) is_integrable_on M1 )
by A11, A64, A65, MESFUNC5:97;
now for x being Element of X1 st x in dom (g | (U `)) holds
(g | (U `)) . x = ((g1 | (U `)) - (g2 | (U `))) . xlet x be
Element of
X1;
( x in dom (g | (U `)) implies (g | (U `)) . x = ((g1 | (U `)) - (g2 | (U `))) . x )assume A79:
x in dom (g | (U `))
;
(g | (U `)) . x = ((g1 | (U `)) - (g2 | (U `))) . xthen A80:
x in U `
by RELAT_1:57;
then A81:
(g | (U `)) . x = (Integral2 (M2,f)) . x
by A66, FUNCT_1:49;
ProjPMap1 (
f,
x)
is_integrable_on M2
by A14, A79, RELAT_1:57;
then A82:
ex
A being
Element of
S2 st
(
A = dom (ProjPMap1 (f,x)) &
ProjPMap1 (
f,
x) is
A -measurable )
by MESFUNC5:def 17;
(
(Integral2 (M2,(max+ f))) . x = Integral (
M2,
(ProjPMap1 ((max+ f),x))) &
(Integral2 (M2,(max- f))) . x = Integral (
M2,
(ProjPMap1 ((max- f),x))) )
by MESFUN12:def 8;
then
(
(Integral2 (M2,(max+ f))) . x = Integral (
M2,
(max+ (ProjPMap1 (f,x)))) &
(Integral2 (M2,(max- f))) . x = Integral (
M2,
(max- (ProjPMap1 (f,x)))) )
by MESFUN12:45;
then ((Integral2 (M2,(max+ f))) . x) - ((Integral2 (M2,(max- f))) . x) =
Integral (
M2,
(ProjPMap1 (f,x)))
by A82, MESFUN11:54
.=
(Integral2 (M2,f)) . x
by MESFUN12:def 8
;
then (g | (U `)) . x =
(((Integral2 (M2,(max+ f))) | (U `)) . x) - ((Integral2 (M2,(max- f))) . x)
by A80, A81, FUNCT_1:49
.=
((g1 | (U `)) . x) - ((g2 | (U `)) . x)
by A64, A65, A80, FUNCT_1:49
;
hence
(g | (U `)) . x = ((g1 | (U `)) - (g2 | (U `))) . x
by A76, A79, MESFUNC1:def 4;
verum end;
then A83:
g | (U `) = (g1 | (U `)) - (g2 | (U `))
by A13, A64, A65, A66, A75, RELAT_1:61, PARTFUN1:5;
A84:
( Integral2 (M2,(max+ f)) is SX1 -measurable & Integral2 (M2,(max- f)) is SX1 -measurable )
by A2, A6, A7, MESFUN11:5, MESFUN12:60;
A85: Integral ((Prod_Measure (M1,M2)),(max+ f)) =
Integral (M1,(Integral2 (M2,(max+ f))))
by A1, A2, A6, A7, A9, MESFUN12:84
.=
Integral (M1,((Integral2 (M2,(max+ f))) | (SX1 \ U)))
by A4, A10, A13, A84, MESFUNC5:95
.=
Integral (M1,(g1 | (U `)))
by A4, A64, SUBSET_1:def 4
;
A86: Integral ((Prod_Measure (M1,M2)),(max- f)) =
Integral (M1,(Integral2 (M2,(max- f))))
by A1, A2, A6, A7, A9, MESFUN12:84
.=
Integral (M1,((Integral2 (M2,(max- f))) | (SX1 \ U)))
by A4, A10, A13, A84, MESFUNC5:95
.=
Integral (M1,(g2 | (U `)))
by A4, A65, SUBSET_1:def 4
;
Integral ((Prod_Measure (M1,M2)),f) = (Integral (M1,((g1 | (U `)) | (U `)))) - (Integral (M1,((g2 | (U `)) | (U `))))
by A5, A85, A86, MESFUN11:54;
then
Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(g | (U `)))
by A77, A78, A83, Th21;
hence
ex g being Function of X1,ExtREAL st
( g is_integrable_on M1 & g | (U `) = (Integral2 (M2,f)) | (U `) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,g) )
by A66; verum