let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S
for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
a <= f . x ) holds
a * (M . E) <= Integral (M,(f | E))
let S be SigmaField of X; for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S
for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
a <= f . x ) holds
a * (M . E) <= Integral (M,(f | E))
let M be sigma_Measure of S; for f being PartFunc of X,ExtREAL
for E being Element of S
for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
a <= f . x ) holds
a * (M . E) <= Integral (M,(f | E))
let f be PartFunc of X,ExtREAL; for E being Element of S
for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
a <= f . x ) holds
a * (M . E) <= Integral (M,(f | E))
let E be Element of S; for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
a <= f . x ) holds
a * (M . E) <= Integral (M,(f | E))
let a be Real; ( f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
a <= f . x ) implies a * (M . E) <= Integral (M,(f | E)) )
assume that
A1:
f is_integrable_on M
and
A2:
E c= dom f
and
A3:
M . E < +infty
and
A4:
for x being Element of X st x in E holds
a <= f . x
; a * (M . E) <= Integral (M,(f | E))
set C = chi (E,X);
A5:
f | E is_integrable_on M
by A1, MESFUNC5:97;
for x being Element of X st x in dom (a (#) ((chi (E,X)) | E)) holds
(a (#) ((chi (E,X)) | E)) . x <= (f | E) . x
proof
let x be
Element of
X;
( x in dom (a (#) ((chi (E,X)) | E)) implies (a (#) ((chi (E,X)) | E)) . x <= (f | E) . x )
assume A6:
x in dom (a (#) ((chi (E,X)) | E))
;
(a (#) ((chi (E,X)) | E)) . x <= (f | E) . x
then A7:
x in dom ((chi (E,X)) | E)
by MESFUNC1:def 6;
then
x in (dom (chi (E,X))) /\ E
by RELAT_1:61;
then A8:
x in E
by XBOOLE_0:def 4;
then
a <= f . x
by A4;
then A9:
a <= (f | E) . x
by A8, FUNCT_1:49;
(a (#) ((chi (E,X)) | E)) . x =
a * (((chi (E,X)) | E) . x)
by A6, MESFUNC1:def 6
.=
a * ((chi (E,X)) . x)
by A7, FUNCT_1:47
.=
a * 1.
by A8, FUNCT_3:def 3
;
hence
(a (#) ((chi (E,X)) | E)) . x <= (f | E) . x
by A9, XXREAL_3:81;
verum
end;
then A10:
(f | E) - (a (#) ((chi (E,X)) | E)) is nonnegative
by MESFUNC7:1;
dom (a (#) ((chi (E,X)) | E)) = dom ((chi (E,X)) | E)
by MESFUNC1:def 6;
then
dom (a (#) ((chi (E,X)) | E)) = (dom (chi (E,X))) /\ E
by RELAT_1:61;
then
dom (a (#) ((chi (E,X)) | E)) = X /\ E
by FUNCT_3:def 3;
then A11:
dom (a (#) ((chi (E,X)) | E)) = E
by XBOOLE_1:28;
E = E /\ E
;
then A12:
Integral (M,((chi (E,X)) | E)) = M . E
by A3, MESFUNC7:25;
reconsider a = a as Real ;
chi (E,X) is_integrable_on M
by A3, MESFUNC7:24;
then A13:
(chi (E,X)) | E is_integrable_on M
by MESFUNC5:97;
then
a (#) ((chi (E,X)) | E) is_integrable_on M
by MESFUNC5:110;
then consider E1 being Element of S such that
A14:
E1 = (dom (f | E)) /\ (dom (a (#) ((chi (E,X)) | E)))
and
A15:
Integral (M,((a (#) ((chi (E,X)) | E)) | E1)) <= Integral (M,((f | E) | E1))
by A5, A10, MESFUNC7:3;
dom (f | E) = (dom f) /\ E
by RELAT_1:61;
then
dom (f | E) = E
by A2, XBOOLE_1:28;
then
( (a (#) ((chi (E,X)) | E)) | E1 = a (#) ((chi (E,X)) | E) & (f | E) | E1 = f | E )
by A14, A11;
hence
a * (M . E) <= Integral (M,(f | E))
by A13, A15, A12, MESFUNC5:110; verum