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) holds
( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 & Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 )
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) holds
( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 & Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 )
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) holds
( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 & Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 )
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) holds
( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 & Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 )
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) holds
( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 & Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 )
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) implies ( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 & Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 ) )
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: f is_integrable_on Prod_Measure (M1,M2) ; :: thesis: ( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 & Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 )
reconsider XX1 = X1 as Element of S1 by MEASURE1:7;
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
set PM = Prod_Measure (M1,M2);
consider E being Element of sigma (measurable_rectangles (S1,S2)) such that
A4: ( E = dom f & f is E -measurable ) by A3, MESFUNC5:def 17;
A5: ( max+ f is E -measurable & max- f is E -measurable & |.f.| is E -measurable ) by A4, MESFUNC2:27, MESFUN11:10;
A6: ( dom (max+ f) = E & dom (max- f) = E & dom |.f.| = E ) by A4, MESFUNC1:def 10, MESFUNC2:def 2, MESFUNC2:def 3;
A7: ( max+ f is nonnegative & max- f is nonnegative & |.f.| is nonnegative ) by MESFUN11:5;
then A8: ( Integral1 (M1,(max+ f)) is nonnegative & Integral2 (M2,(max+ f)) is nonnegative & Integral1 (M1,(max- f)) is nonnegative & Integral2 (M2,(max- f)) is nonnegative & Integral1 (M1,|.f.|) is nonnegative & Integral2 (M2,|.f.|) is nonnegative ) by A5, A6, MESFUN12:66;
A9: ( Integral1 (M1,(max+ f)) is XX2 -measurable & Integral1 (M1,(max- f)) is XX2 -measurable & Integral1 (M1,|.f.|) is XX2 -measurable & Integral2 (M2,(max+ f)) is XX1 -measurable & Integral2 (M2,(max- f)) is XX1 -measurable & Integral2 (M2,|.f.|) is XX1 -measurable ) by A1, A2, A5, A6, MESFUN11:5, MESFUN12:59, MESFUN12:60;
A10: ( dom (Integral1 (M1,(max+ f))) = XX2 & dom (Integral2 (M2,(max+ f))) = XX1 & dom (Integral1 (M1,(max- f))) = XX2 & dom (Integral2 (M2,(max- f))) = XX1 & dom (Integral1 (M1,|.f.|)) = XX2 & dom (Integral2 (M2,|.f.|)) = XX1 ) by FUNCT_2:def 1;
( integral+ ((Prod_Measure (M1,M2)),(max+ f)) = Integral ((Prod_Measure (M1,M2)),(max+ f)) & integral+ ((Prod_Measure (M1,M2)),(max- f)) = Integral ((Prod_Measure (M1,M2)),(max- f)) ) by A5, A6, MESFUN11:5, MESFUNC5:88;
then ( integral+ ((Prod_Measure (M1,M2)),(max+ f)) = Integral (M2,(Integral1 (M1,(max+ f)))) & integral+ ((Prod_Measure (M1,M2)),(max+ f)) = Integral (M1,(Integral2 (M2,(max+ f)))) & integral+ ((Prod_Measure (M1,M2)),(max- f)) = Integral (M2,(Integral1 (M1,(max- f)))) & integral+ ((Prod_Measure (M1,M2)),(max- f)) = Integral (M1,(Integral2 (M2,(max- f)))) ) by A1, A2, A5, A6, A7, MESFUN12:84;
then A11: ( Integral (M2,(Integral1 (M1,(max+ f)))) < +infty & Integral (M1,(Integral2 (M2,(max+ f)))) < +infty & Integral (M2,(Integral1 (M1,(max- f)))) < +infty & Integral (M1,(Integral2 (M2,(max- f)))) < +infty ) by A3, MESFUNC5:def 17;
( Integral1 (M1,(max+ f)) = max+ (Integral1 (M1,(max+ f))) & Integral2 (M2,(max+ f)) = max+ (Integral2 (M2,(max+ f))) & Integral1 (M1,(max- f)) = max+ (Integral1 (M1,(max- f))) & Integral2 (M2,(max- f)) = max+ (Integral2 (M2,(max- f))) ) by A8, MESFUN11:31;
then A12: ( integral+ (M2,(max+ (Integral1 (M1,(max+ f))))) < +infty & integral+ (M1,(max+ (Integral2 (M2,(max+ f))))) < +infty & integral+ (M2,(max+ (Integral1 (M1,(max- f))))) < +infty & integral+ (M1,(max+ (Integral2 (M2,(max- f))))) < +infty ) by A8, A9, A10, A11, MESFUNC5:88;
( integral+ (M2,(max- (Integral1 (M1,(max+ f))))) = 0 & integral+ (M1,(max- (Integral2 (M2,(max+ f))))) = 0 & integral+ (M2,(max- (Integral1 (M1,(max- f))))) = 0 & integral+ (M1,(max- (Integral2 (M2,(max- f))))) = 0 ) by A8, A9, A10, MESFUN11:53;
hence ( Integral1 (M1,(max+ f)) is_integrable_on M2 & Integral2 (M2,(max+ f)) is_integrable_on M1 & Integral1 (M1,(max- f)) is_integrable_on M2 & Integral2 (M2,(max- f)) is_integrable_on M1 ) by A9, A10, A12, MESFUNC5:def 17; :: thesis: ( Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 )
A13: |.f.| is_integrable_on Prod_Measure (M1,M2) by A3, A4, MESFUNC5:100;
max+ |.f.| = |.f.| by MESFUN11:31;
then integral+ ((Prod_Measure (M1,M2)),(max+ |.f.|)) = Integral ((Prod_Measure (M1,M2)),|.f.|) by A6, A4, MESFUNC2:27, MESFUNC5:88;
then ( integral+ ((Prod_Measure (M1,M2)),(max+ |.f.|)) = Integral (M2,(Integral1 (M1,|.f.|))) & integral+ ((Prod_Measure (M1,M2)),(max+ |.f.|)) = Integral (M1,(Integral2 (M2,|.f.|))) ) by A1, A2, A5, A6, MESFUN12:84;
then A15: ( Integral (M2,(Integral1 (M1,|.f.|))) < +infty & Integral (M1,(Integral2 (M2,|.f.|))) < +infty ) by A13, MESFUNC5:def 17;
( Integral1 (M1,|.f.|) = max+ (Integral1 (M1,|.f.|)) & Integral2 (M2,|.f.|) = max+ (Integral2 (M2,|.f.|)) ) by A8, MESFUN11:31;
then A16: ( integral+ (M2,(max+ (Integral1 (M1,|.f.|)))) < +infty & integral+ (M1,(max+ (Integral2 (M2,|.f.|)))) < +infty ) by A8, A9, A10, A15, MESFUNC5:88;
( integral+ (M2,(max- (Integral1 (M1,|.f.|)))) = 0 & integral+ (M1,(max- (Integral2 (M2,|.f.|)))) = 0 ) by A8, A9, A10, MESFUN11:53;
hence ( Integral1 (M1,|.f.|) is_integrable_on M2 & Integral2 (M2,|.f.|) is_integrable_on M1 ) by A9, A10, A16, MESFUNC5:def 17; :: thesis: verum