let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being b3 -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; for M being sigma_Measure of S
for E being Element of S
for f being b2 -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; for E being Element of S
for f being b1 -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; 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; 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; ( 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
; 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
let x be
Element of
X;
( 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)
;
((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;
verum
end;
then
integral+ (M,((chi (er,Er,X)) | Er)) <= integral+ (M,(f | Er))
by A6, A7, A8, A9, A10, MESFUNC5:85;
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; verum