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, b 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 & f . x <= b ) ) holds
( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= b * (M . 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, b 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 & f . x <= b ) ) holds
( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= b * (M . E) )
let M be sigma_Measure of S; for f being PartFunc of X,ExtREAL
for E being Element of S
for a, b 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 & f . x <= b ) ) holds
( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= b * (M . E) )
let f be PartFunc of X,ExtREAL; for E being Element of S
for a, b 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 & f . x <= b ) ) holds
( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= b * (M . E) )
let E be Element of S; for a, b 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 & f . x <= b ) ) holds
( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= b * (M . E) )
let a, b 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 & f . x <= b ) ) implies ( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= b * (M . E) ) )
reconsider a1 = a, b1 = b as Element of REAL by XREAL_0:def 1;
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 & f . x <= b )
; ( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= b * (M . 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 (a1 (#) ((chi (E,X)) | E)) holds
(a1 (#) ((chi (E,X)) | E)) . x <= (f | E) . x
proof
let x be
Element of
X;
( x in dom (a1 (#) ((chi (E,X)) | E)) implies (a1 (#) ((chi (E,X)) | E)) . x <= (f | E) . x )
assume A6:
x in dom (a1 (#) ((chi (E,X)) | E))
;
(a1 (#) ((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;
(a1 (#) ((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
(a1 (#) ((chi (E,X)) | E)) . x <= (f | E) . x
by A9, XXREAL_3:81;
verum
end;
then A10:
(f | E) - (a1 (#) ((chi (E,X)) | E)) is nonnegative
by Th1;
chi (E,X) is_integrable_on M
by A3, Th24;
then A11:
(chi (E,X)) | E is_integrable_on M
by MESFUNC5:97;
then
a1 (#) ((chi (E,X)) | E) is_integrable_on M
by MESFUNC5:110;
then consider E1 being Element of S such that
A12:
E1 = (dom (f | E)) /\ (dom (a1 (#) ((chi (E,X)) | E)))
and
A13:
Integral (M,((a1 (#) ((chi (E,X)) | E)) | E1)) <= Integral (M,((f | E) | E1))
by A5, A10, Th3;
dom (f | E) = (dom f) /\ E
by RELAT_1:61;
then A14:
dom (f | E) = E
by A2, XBOOLE_1:28;
dom (a1 (#) ((chi (E,X)) | E)) = dom ((chi (E,X)) | E)
by MESFUNC1:def 6;
then
dom (a1 (#) ((chi (E,X)) | E)) = (dom (chi (E,X))) /\ E
by RELAT_1:61;
then
dom (a1 (#) ((chi (E,X)) | E)) = X /\ E
by FUNCT_3:def 3;
then A15:
dom (a1 (#) ((chi (E,X)) | E)) = E
by XBOOLE_1:28;
then A16:
(f | E) | E1 = f | E
by A12, A14, RELAT_1:69;
dom (b1 (#) ((chi (E,X)) | E)) = dom ((chi (E,X)) | E)
by MESFUNC1:def 6;
then
dom (b1 (#) ((chi (E,X)) | E)) = (dom (chi (E,X))) /\ E
by RELAT_1:61;
then
dom (b1 (#) ((chi (E,X)) | E)) = X /\ E
by FUNCT_3:def 3;
then A17:
dom (b1 (#) ((chi (E,X)) | E)) = E
by XBOOLE_1:28;
for x being Element of X st x in dom (f | E) holds
(f | E) . x <= (b1 (#) ((chi (E,X)) | E)) . x
proof
let x be
Element of
X;
( x in dom (f | E) implies (f | E) . x <= (b1 (#) ((chi (E,X)) | E)) . x )
assume A18:
x in dom (f | E)
;
(f | E) . x <= (b1 (#) ((chi (E,X)) | E)) . x
then A19:
x in dom ((chi (E,X)) | E)
by A14, A15, MESFUNC1:def 6;
then
x in (dom (chi (E,X))) /\ E
by RELAT_1:61;
then A20:
x in E
by XBOOLE_0:def 4;
then
f . x <= b
by A4;
then A21:
(f | E) . x <= b
by A20, FUNCT_1:49;
(b1 (#) ((chi (E,X)) | E)) . x =
b * (((chi (E,X)) | E) . x)
by A14, A17, A18, MESFUNC1:def 6
.=
b * ((chi (E,X)) . x)
by A19, FUNCT_1:47
.=
b * 1.
by A20, FUNCT_3:def 3
;
hence
(f | E) . x <= (b1 (#) ((chi (E,X)) | E)) . x
by A21, XXREAL_3:81;
verum
end;
then A22:
(b1 (#) ((chi (E,X)) | E)) - (f | E) is nonnegative
by Th1;
b1 (#) ((chi (E,X)) | E) is_integrable_on M
by A11, MESFUNC5:110;
then consider E2 being Element of S such that
A23:
E2 = (dom (f | E)) /\ (dom (b1 (#) ((chi (E,X)) | E)))
and
A24:
Integral (M,((f | E) | E2)) <= Integral (M,((b1 (#) ((chi (E,X)) | E)) | E2))
by A5, A22, Th3;
A25:
(b1 (#) ((chi (E,X)) | E)) | E2 = b1 (#) ((chi (E,X)) | E)
by A14, A17, A23, RELAT_1:69;
E = E /\ E
;
then A26:
Integral (M,((chi (E,X)) | E)) = M . E
by A3, Th25;
A27:
(f | E) | E2 = f | E
by A14, A17, A23, RELAT_1:69;
(a1 (#) ((chi (E,X)) | E)) | E1 = a1 (#) ((chi (E,X)) | E)
by A12, A14, A15, RELAT_1:69;
hence
( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= b * (M . E) )
by A11, A13, A24, A25, A16, A27, A26, MESFUNC5:110; verum