let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being b_{3} -measurable PartFunc of X,ExtREAL

for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds

er * (M . (great_eq_dom (f,er))) <= Integral (M,f)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for E being Element of S

for f being b_{2} -measurable PartFunc of X,ExtREAL

for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds

er * (M . (great_eq_dom (f,er))) <= Integral (M,f)

let M be sigma_Measure of S; :: thesis: for E being Element of S

for f being b_{1} -measurable PartFunc of X,ExtREAL

for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds

er * (M . (great_eq_dom (f,er))) <= Integral (M,f)

let E be Element of S; :: thesis: for f being E -measurable PartFunc of X,ExtREAL

for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds

er * (M . (great_eq_dom (f,er))) <= Integral (M,f)

let f be E -measurable PartFunc of X,ExtREAL; :: thesis: for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds

er * (M . (great_eq_dom (f,er))) <= Integral (M,f)

let er be ExtReal; :: thesis: ( dom f = E & f is nonnegative & er >= 0 implies er * (M . (great_eq_dom (f,er))) <= Integral (M,f) )

assume that

A1: dom f = E and

A2: f is nonnegative and

A3: er >= 0 ; :: thesis: er * (M . (great_eq_dom (f,er))) <= Integral (M,f)

A4: great_eq_dom (f,er) c= E by A1, MESFUNC1:def 14;

A5: great_eq_dom (f,+infty) = eq_dom (f,+infty) by Th10;

( er in REAL or er = +infty ) by A3, XXREAL_0:14;

then E /\ (great_eq_dom (f,er)) is Element of S by A1, A5, MESFUNC1:27, MESFUNC1:33;

then reconsider Er = great_eq_dom (f,er) as Element of S by A4, XBOOLE_1:28;

dom (chi (er,Er,X)) = X by FUNCT_2:def 1;

then A6: ( Er = dom (f | Er) & Er = dom ((chi (er,Er,X)) | Er) ) by A1, A4, RELAT_1:62;

( f is Er -measurable & Er = Er /\ (dom f) ) by A1, A4, XBOOLE_1:28, MESFUNC1:30;

then A7: f | Er is Er -measurable by MESFUNC5:42;

A8: f | Er is nonnegative by A2, MESFUNC5:15;

A9: (chi (er,Er,X)) | Er is Er -measurable by MESFUN12:15;

chi (er,Er,X) is V97() by A3, MESFUN12:17;

then A10: (chi (er,Er,X)) | Er is nonnegative by MESFUNC5:15;

for x being Element of X st x in dom ((chi (er,Er,X)) | Er) holds

((chi (er,Er,X)) | Er) . x <= (f | Er) . x

then Integral (M,((chi (er,Er,X)) | Er)) <= integral+ (M,(f | Er)) by A6, A10, MESFUNC5:88, MESFUN12:15;

then A14: er * (M . Er) <= integral+ (M,(f | Er)) by MESFUN12:50;

integral+ (M,(f | Er)) <= integral+ (M,(f | E)) by A1, A2, A4, MESFUNC5:83;

then integral+ (M,(f | Er)) <= Integral (M,f) by A1, A2, MESFUNC5:88;

hence er * (M . (great_eq_dom (f,er))) <= Integral (M,f) by A14, XXREAL_0:2; :: thesis: verum

for M being sigma_Measure of S

for E being Element of S

for f being b

for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds

er * (M . (great_eq_dom (f,er))) <= Integral (M,f)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for E being Element of S

for f being b

for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds

er * (M . (great_eq_dom (f,er))) <= Integral (M,f)

let M be sigma_Measure of S; :: thesis: for E being Element of S

for f being b

for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds

er * (M . (great_eq_dom (f,er))) <= Integral (M,f)

let E be Element of S; :: thesis: for f being E -measurable PartFunc of X,ExtREAL

for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds

er * (M . (great_eq_dom (f,er))) <= Integral (M,f)

let f be E -measurable PartFunc of X,ExtREAL; :: thesis: for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds

er * (M . (great_eq_dom (f,er))) <= Integral (M,f)

let er be ExtReal; :: thesis: ( dom f = E & f is nonnegative & er >= 0 implies er * (M . (great_eq_dom (f,er))) <= Integral (M,f) )

assume that

A1: dom f = E and

A2: f is nonnegative and

A3: er >= 0 ; :: thesis: er * (M . (great_eq_dom (f,er))) <= Integral (M,f)

A4: great_eq_dom (f,er) c= E by A1, MESFUNC1:def 14;

A5: great_eq_dom (f,+infty) = eq_dom (f,+infty) by Th10;

( er in REAL or er = +infty ) by A3, XXREAL_0:14;

then E /\ (great_eq_dom (f,er)) is Element of S by A1, A5, MESFUNC1:27, MESFUNC1:33;

then reconsider Er = great_eq_dom (f,er) as Element of S by A4, XBOOLE_1:28;

dom (chi (er,Er,X)) = X by FUNCT_2:def 1;

then A6: ( Er = dom (f | Er) & Er = dom ((chi (er,Er,X)) | Er) ) by A1, A4, RELAT_1:62;

( f is Er -measurable & Er = Er /\ (dom f) ) by A1, A4, XBOOLE_1:28, MESFUNC1:30;

then A7: f | Er is Er -measurable by MESFUNC5:42;

A8: f | Er is nonnegative by A2, MESFUNC5:15;

A9: (chi (er,Er,X)) | Er is Er -measurable by MESFUN12:15;

chi (er,Er,X) is V97() by A3, MESFUN12:17;

then A10: (chi (er,Er,X)) | Er is nonnegative by MESFUNC5:15;

for x being Element of X st x in dom ((chi (er,Er,X)) | Er) holds

((chi (er,Er,X)) | Er) . x <= (f | Er) . x

proof

then
integral+ (M,((chi (er,Er,X)) | Er)) <= integral+ (M,(f | Er))
by A6, A7, A8, A9, A10, MESFUNC5:85;
let x be Element of X; :: thesis: ( x in dom ((chi (er,Er,X)) | Er) implies ((chi (er,Er,X)) | Er) . x <= (f | Er) . x )

assume A11: x in dom ((chi (er,Er,X)) | Er) ; :: thesis: ((chi (er,Er,X)) | Er) . x <= (f | Er) . x

then ((chi (er,Er,X)) | Er) . x = (chi (er,Er,X)) . x by FUNCT_1:47;

then A12: ((chi (er,Er,X)) | Er) . x = er by A6, A11, MESFUN12:def 1;

A13: (f | Er) . x = f . x by A6, A11, FUNCT_1:47;

x in great_eq_dom (f,er) by A11, RELAT_1:57;

hence ((chi (er,Er,X)) | Er) . x <= (f | Er) . x by A12, A13, MESFUNC1:def 14; :: thesis: verum

end;assume A11: x in dom ((chi (er,Er,X)) | Er) ; :: thesis: ((chi (er,Er,X)) | Er) . x <= (f | Er) . x

then ((chi (er,Er,X)) | Er) . x = (chi (er,Er,X)) . x by FUNCT_1:47;

then A12: ((chi (er,Er,X)) | Er) . x = er by A6, A11, MESFUN12:def 1;

A13: (f | Er) . x = f . x by A6, A11, FUNCT_1:47;

x in great_eq_dom (f,er) by A11, RELAT_1:57;

hence ((chi (er,Er,X)) | Er) . x <= (f | Er) . x by A12, A13, MESFUNC1:def 14; :: thesis: verum

then Integral (M,((chi (er,Er,X)) | Er)) <= integral+ (M,(f | Er)) by A6, A10, MESFUNC5:88, MESFUN12:15;

then A14: er * (M . Er) <= integral+ (M,(f | Er)) by MESFUN12:50;

integral+ (M,(f | Er)) <= integral+ (M,(f | E)) by A1, A2, A4, MESFUNC5:83;

then integral+ (M,(f | Er)) <= Integral (M,f) by A1, A2, MESFUNC5:88;

hence er * (M . (great_eq_dom (f,er))) <= Integral (M,f) by A14, XXREAL_0:2; :: thesis: verum