let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
let M be sigma_Measure of S; for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
let f, g be PartFunc of X,ExtREAL; ( f is_integrable_on M & g is_integrable_on M & g - f is nonnegative implies ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) )
assume that
A1:
f is_integrable_on M
and
A2:
g is_integrable_on M
and
A3:
g - f is nonnegative
; ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
set h = (- jj) (#) f;
A4:
(- jj) (#) f is_integrable_on M
by A1, MESFUNC5:110;
then consider E being Element of S such that
A5:
E = (dom ((- jj) (#) f)) /\ (dom g)
and
A6:
Integral (M,(((- jj) (#) f) + g)) = (Integral (M,(((- jj) (#) f) | E))) + (Integral (M,(g | E)))
by A2, MESFUNC5:109;
A7:
ex E3 being Element of S st
( E3 = dom ((- jj) (#) f) & (- jj) (#) f is E3 -measurable )
by A4;
A8:
g | E is_integrable_on M
by A2, MESFUNC5:97;
then A9:
Integral (M,(g | E)) < +infty
by MESFUNC5:96;
-infty < Integral (M,(g | E))
by A8, MESFUNC5:96;
then reconsider c2 = Integral (M,(g | E)) as Element of REAL by A9, XXREAL_0:14;
take
E
; ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
A10:
((- jj) (#) f) | E = (- jj) (#) (f | E)
by Th2;
g + (- f) is nonnegative
by A3, MESFUNC2:8;
then A11:
((- jj) (#) f) + g is nonnegative
by MESFUNC2:9;
A12:
f | E is_integrable_on M
by A1, MESFUNC5:97;
then A13:
Integral (M,(f | E)) < +infty
by MESFUNC5:96;
-infty < Integral (M,(f | E))
by A12, MESFUNC5:96;
then reconsider c1 = Integral (M,(f | E)) as Element of REAL by A13, XXREAL_0:14;
A14: (- jj) * (Integral (M,(f | E))) =
(- jj) * c1
by EXTREAL1:1
.=
- c1
;
ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable )
by A2;
then
ex A being Element of S st
( A = dom (((- jj) (#) f) + g) & ((- jj) (#) f) + g is A -measurable )
by A7, MESFUNC5:47;
then
0 <= (Integral (M,(((- jj) (#) f) | E))) + (Integral (M,(g | E)))
by A6, A11, MESFUNC5:90;
then
0 <= ((- jj) * (Integral (M,(f | E)))) + (Integral (M,(g | E)))
by A12, A10, MESFUNC5:110;
then
0 <= (- c1) + c2
by A14, XXREAL_3:def 2;
then
0 + c1 <= ((- c1) + c2) + c1
by XREAL_1:6;
hence
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
by A5, MESFUNC1:def 6; verum