let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
( M . (eq_dom (f,+infty)) = 0 & M . (eq_dom (f,-infty)) = 0 & f is_a.e.finite M & ( for r being Real st r > 0 holds
M . (great_eq_dom (|.f.|,r)) < +infty ) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
( M . (eq_dom (f,+infty)) = 0 & M . (eq_dom (f,-infty)) = 0 & f is_a.e.finite M & ( for r being Real st r > 0 holds
M . (great_eq_dom (|.f.|,r)) < +infty ) )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
( M . (eq_dom (f,+infty)) = 0 & M . (eq_dom (f,-infty)) = 0 & f is_a.e.finite M & ( for r being Real st r > 0 holds
M . (great_eq_dom (|.f.|,r)) < +infty ) )
let f be PartFunc of X,ExtREAL; :: thesis: ( f is_integrable_on M implies ( M . (eq_dom (f,+infty)) = 0 & M . (eq_dom (f,-infty)) = 0 & f is_a.e.finite M & ( for r being Real st r > 0 holds
M . (great_eq_dom (|.f.|,r)) < +infty ) ) )
assume A2: f is_integrable_on M ; :: thesis: ( M . (eq_dom (f,+infty)) = 0 & M . (eq_dom (f,-infty)) = 0 & f is_a.e.finite M & ( for r being Real st r > 0 holds
M . (great_eq_dom (|.f.|,r)) < +infty ) )
consider E being Element of S such that
A3: ( E = dom f & f is E -measurable ) by A2, MESFUNC5:def 17;
eq_dom (f,+infty) c= E by A3, MESFUNC1:def 15;
then eq_dom (f,+infty) = E /\ (eq_dom (f,+infty)) by XBOOLE_1:28;
then reconsider E0 = eq_dom (f,+infty) as Element of S by A3, MESFUNC1:33;
eq_dom (f,-infty) c= E by A3, MESFUNC1:def 15;
then eq_dom (f,-infty) = E /\ (eq_dom (f,-infty)) by XBOOLE_1:28;
then reconsider E1 = eq_dom (f,-infty) as Element of S by A3, MESFUNC1:34;
A4: ( E0 c= E & E1 c= E ) by A3, MESFUNC1:def 15;
then A5: ( E0 = E /\ E0 & E1 = E /\ E1 & E0 \/ E1 c= E ) by XBOOLE_1:8, XBOOLE_1:28;
A6: ( dom (max+ f) = E & dom (max- f) = E & dom |.f.| = E ) by A3, MESFUNC1:def 10, MESFUNC2:def 2, MESFUNC2:def 3;
then A7: ( dom (f | E0) = E0 & dom ((max+ f) | E0) = E0 & dom (f | E1) = E1 & dom ((max- f) | E1) = E1 ) by A3, A4, RELAT_1:62;
A8: ( max+ f is E -measurable & max- f is E -measurable & |.f.| is E -measurable ) by A3, MESFUNC2:25, MESFUNC2:26, MESFUNC2:27;
then A9: ( max+ f is E0 -measurable & max- f is E1 -measurable ) by A4, MESFUNC1:30;
A10: ( (max+ f) | E0 is nonnegative & (max- f) | E1 is nonnegative ) by MESFUNC5:15, MESFUN11:5;
A11: ( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;
then integral+ (M,((max+ f) | E0)) <= integral+ (M,((max+ f) | E)) by A3, A4, A6, MESFUNC2:25, MESFUNC5:83;
then integral+ (M,((max+ f) | E0)) < +infty by A2, A6, MESFUNC5:def 17, XXREAL_0:2;
then A12: Integral (M,((max+ f) | E0)) < +infty by A5, A6, A7, A9, A10, MESFUNC5:42, MESFUNC5:88;
A13: now :: thesis: for x being Element of X st x in dom (f | E0) holds
(f | E0) . x = +infty
let x be Element of X; :: thesis: ( x in dom (f | E0) implies (f | E0) . x = +infty )
assume A14: x in dom (f | E0) ; :: thesis: (f | E0) . x = +infty
then x in E0 by RELAT_1:57;
then ( x in dom f & f . x = +infty ) by MESFUNC1:def 15;
hence (f | E0) . x = +infty by A14, FUNCT_1:47; :: thesis: verum
end;
now :: thesis: for x being Element of X st x in dom (f | E0) holds
(f | E0) . x = ((max+ f) | E0) . x
let x be Element of X; :: thesis: ( x in dom (f | E0) implies (f | E0) . x = ((max+ f) | E0) . x )
assume A15: x in dom (f | E0) ; :: thesis: (f | E0) . x = ((max+ f) | E0) . x
then A16: (f | E0) . x = +infty by A13;
then A17: ( x in dom f & f . x = +infty ) by A15, RELAT_1:57, FUNCT_1:47;
then x in dom (max+ f) by MESFUNC2:def 2;
then (max+ f) . x = max (+infty,0) by A17, MESFUNC2:def 2;
then (max+ f) . x = +infty by XXREAL_0:def 10;
hence (f | E0) . x = ((max+ f) | E0) . x by A7, A15, A16, FUNCT_1:47; :: thesis: verum
end;
then A18: Integral (M,(f | E0)) < +infty by A7, A12, PARTFUN1:5;
dom (chi (+infty,E0,X)) = X by FUNCT_2:def 1;
then A19: dom ((chi (+infty,E0,X)) | E0) = E0 by RELAT_1:62;
now :: thesis: for x being Element of X st x in dom (f | E0) holds
(f | E0) . x = ((chi (+infty,E0,X)) | E0) . x
let x be Element of X; :: thesis: ( x in dom (f | E0) implies (f | E0) . x = ((chi (+infty,E0,X)) | E0) . x )
assume A20: x in dom (f | E0) ; :: thesis: (f | E0) . x = ((chi (+infty,E0,X)) | E0) . x
then A21: x in E0 by RELAT_1:57;
then ((chi (+infty,E0,X)) | E0) . x = (chi (+infty,E0,X)) . x by FUNCT_1:49;
then ((chi (+infty,E0,X)) | E0) . x = +infty by A21, MESFUN12:def 1;
hence (f | E0) . x = ((chi (+infty,E0,X)) | E0) . x by A13, A20; :: thesis: verum
end;
then f | E0 = (chi (+infty,E0,X)) | E0 by A3, A4, A19, RELAT_1:62, PARTFUN1:5;
then A22: Integral (M,(f | E0)) = +infty * (M . E0) by MESFUN12:50;
A23: now :: thesis: not M . E0 <> 0
assume M . E0 <> 0 ; :: thesis: contradiction
then M . E0 > 0 by SUPINF_2:51;
hence contradiction by A18, A22, XXREAL_3:def 5; :: thesis: verum
end;
hence M . (eq_dom (f,+infty)) = 0 ; :: thesis: ( M . (eq_dom (f,-infty)) = 0 & f is_a.e.finite M & ( for r being Real st r > 0 holds
M . (great_eq_dom (|.f.|,r)) < +infty ) )
A24: Integral (M,(- ((max- f) | E1))) = - (Integral (M,((max- f) | E1))) by A5, A6, A7, A9, MESFUNC5:42, MESFUN11:52;
integral+ (M,((max- f) | E1)) <= integral+ (M,((max- f) | E)) by A3, A4, A6, A11, MESFUNC2:26, MESFUNC5:83;
then integral+ (M,((max- f) | E1)) < +infty by A2, A6, MESFUNC5:def 17, XXREAL_0:2;
then Integral (M,((max- f) | E1)) < +infty by A5, A6, A7, A9, A10, MESFUNC5:42, MESFUNC5:88;
then A25: Integral (M,(- ((max- f) | E1))) > -infty by A24, XXREAL_3:6, XXREAL_3:38;
A26: now :: thesis: for x being Element of X st x in dom (f | E1) holds
(f | E1) . x = -infty
let x be Element of X; :: thesis: ( x in dom (f | E1) implies (f | E1) . x = -infty )
assume d7: x in dom (f | E1) ; :: thesis: (f | E1) . x = -infty
then x in E1 by RELAT_1:57;
then ( x in dom f & f . x = -infty ) by MESFUNC1:def 15;
hence (f | E1) . x = -infty by d7, FUNCT_1:47; :: thesis: verum
end;
A27: dom (- ((max- f) | E1)) = E1 by A7, MESFUNC1:def 7;
now :: thesis: for x being Element of X st x in dom (f | E1) holds
(f | E1) . x = (- ((max- f) | E1)) . x
let x be Element of X; :: thesis: ( x in dom (f | E1) implies (f | E1) . x = (- ((max- f) | E1)) . x )
assume A28: x in dom (f | E1) ; :: thesis: (f | E1) . x = (- ((max- f) | E1)) . x
then x in E1 by RELAT_1:57;
then A29: ( x in dom f & f . x = -infty ) by MESFUNC1:def 15;
then A30: (f | E1) . x = - +infty by A28, FUNCT_1:47, XXREAL_3:6;
x in dom (max- f) by A29, MESFUNC2:def 3;
then (max- f) . x = max ((- -infty),0) by A29, MESFUNC2:def 3;
then (max- f) . x = +infty by XXREAL_0:def 10, XXREAL_3:5;
then (f | E1) . x = - (((max- f) | E1) . x) by A7, A28, A30, FUNCT_1:47;
hence (f | E1) . x = (- ((max- f) | E1)) . x by A7, A27, A28, MESFUNC1:def 7; :: thesis: verum
end;
then A31: Integral (M,(f | E1)) > -infty by A3, A4, A25, A27, RELAT_1:62, PARTFUN1:5;
dom (chi (-infty,E1,X)) = X by FUNCT_2:def 1;
then A32: dom ((chi (-infty,E1,X)) | E1) = E1 by RELAT_1:62;
now :: thesis: for x being Element of X st x in dom (f | E1) holds
(f | E1) . x = ((chi (-infty,E1,X)) | E1) . x
let x be Element of X; :: thesis: ( x in dom (f | E1) implies (f | E1) . x = ((chi (-infty,E1,X)) | E1) . x )
assume A33: x in dom (f | E1) ; :: thesis: (f | E1) . x = ((chi (-infty,E1,X)) | E1) . x
then A34: x in E1 by RELAT_1:57;
then ((chi (-infty,E1,X)) | E1) . x = (chi (-infty,E1,X)) . x by FUNCT_1:49;
then ((chi (-infty,E1,X)) | E1) . x = -infty by A34, MESFUN12:def 1;
hence (f | E1) . x = ((chi (-infty,E1,X)) | E1) . x by A26, A33; :: thesis: verum
end;
then f | E1 = (chi (-infty,E1,X)) | E1 by A3, A4, A32, RELAT_1:62, PARTFUN1:5;
then A35: Integral (M,(f | E1)) = -infty * (M . E1) by MESFUN12:50;
A36: now :: thesis: not M . E1 <> 0
assume M . E1 <> 0 ; :: thesis: contradiction
then M . E1 > 0 by SUPINF_2:51;
hence contradiction by A31, A35, XXREAL_3:def 5; :: thesis: verum
end;
hence M . (eq_dom (f,-infty)) = 0 ; :: thesis: ( f is_a.e.finite M & ( for r being Real st r > 0 holds
M . (great_eq_dom (|.f.|,r)) < +infty ) )
set E2 = E0 \/ E1;
M . (E0 \/ E1) <= (M . E0) + (M . E1) by MEASURE1:33;
then ( M . (E0 \/ E1) <= 0 & M . (E0 \/ E1) >= 0 ) by A23, A36, SUPINF_2:51;
then A37: M . (E0 \/ E1) = 0 ;
now :: thesis: for r being ExtReal st r in rng (f | ((E0 \/ E1) `)) holds
r in REAL
let r be ExtReal; :: thesis: ( r in rng (f | ((E0 \/ E1) `)) implies r in REAL )
assume r in rng (f | ((E0 \/ E1) `)) ; :: thesis: r in REAL
then consider x being object such that
A38: ( x in dom (f | ((E0 \/ E1) `)) & r = (f | ((E0 \/ E1) `)) . x ) by FUNCT_1:def 3;
A39: ( x in dom f & x in (E0 \/ E1) ` ) by A38, RELAT_1:57;
then x in X \ (E0 \/ E1) by SUBSET_1:def 4;
then ( x in X & not x in E0 \/ E1 ) by XBOOLE_0:def 5;
then ( not x in E0 & not x in E1 ) by XBOOLE_0:def 3;
then ( f . x <> +infty & f . x <> -infty ) by A39, MESFUNC1:def 15;
then ( r <> +infty & r <> -infty ) by A38, FUNCT_1:47;
hence r in REAL by XXREAL_0:14; :: thesis: verum
end;
then rng (f | ((E0 \/ E1) `)) c= REAL ;
then f | ((E0 \/ E1) `) is PartFunc of X,REAL by RELSET_1:6;
hence f is_a.e.finite M by A3, A4, A37, XBOOLE_1:8; :: thesis: for r being Real st r > 0 holds
M . (great_eq_dom (|.f.|,r)) < +infty
|.f.| is_integrable_on M by A2, A3, MESFUNC5:100;
then A40: Integral (M,|.f.|) < +infty by MESFUNC5:96;
thus for r being Real st r > 0 holds
M . (great_eq_dom (|.f.|,r)) < +infty :: thesis: verum
proof
let r be Real; :: thesis: ( r > 0 implies M . (great_eq_dom (|.f.|,r)) < +infty )
assume A41: r > 0 ; :: thesis: M . (great_eq_dom (|.f.|,r)) < +infty
then r * (M . (great_eq_dom (|.f.|,r))) <= Integral (M,|.f.|) by A6, A8, Th14;
then r * (M . (great_eq_dom (|.f.|,r))) < +infty by A40, XXREAL_0:2;
then (r * (M . (great_eq_dom (|.f.|,r)))) / r < +infty / r by A41, XXREAL_3:80;
then M . (great_eq_dom (|.f.|,r)) < +infty / r by A41, XXREAL_3:88;
hence M . (great_eq_dom (|.f.|,r)) < +infty by A41, XXREAL_3:83; :: thesis: verum
end;