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,REAL st ex A being Element of S st
( A = (dom f) /\ (dom g) & f is A -measurable & g is A -measurable ) & 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,REAL st ex A being Element of S st
( A = (dom f) /\ (dom g) & f is A -measurable & g is A -measurable ) & 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,REAL st ex A being Element of S st
( A = (dom f) /\ (dom g) & f is A -measurable & g is A -measurable ) & 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,REAL; ( ex A being Element of S st
( A = (dom f) /\ (dom g) & f is A -measurable & g is A -measurable ) & 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:
ex A being Element of S st
( A = (dom f) /\ (dom g) & f is A -measurable & g is A -measurable )
and
A2:
f is_integrable_on M
and
A3:
g is_integrable_on M
and
A4:
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 = (- 1) (#) f;
(- 1) (#) f is_integrable_on M
by A2, MESFUNC6:102;
then consider E being Element of S such that
A5:
E = (dom ((- 1) (#) f)) /\ (dom g)
and
A6:
Integral (M,(((- 1) (#) f) + g)) = (Integral (M,(((- 1) (#) f) | E))) + (Integral (M,(g | E)))
by A3, MESFUNC6:101;
A7:
f | E is_integrable_on M
by A2, MESFUNC6:91;
then A8:
Integral (M,(f | E)) < +infty
by MESFUNC6:90;
-infty < Integral (M,(f | E))
by A7, MESFUNC6:90;
then reconsider c1 = Integral (M,(f | E)) as Element of REAL by A8, XXREAL_0:14;
A9:
(- 1) * (Integral (M,(f | E))) = (- 1) * c1
by EXTREAL1:1;
A10:
g | E is_integrable_on M
by A3, MESFUNC6:91;
then A11:
Integral (M,(g | E)) < +infty
by MESFUNC6:90;
-infty < Integral (M,(g | E))
by A10, MESFUNC6:90;
then reconsider c2 = Integral (M,(g | E)) as Element of REAL by A11, XXREAL_0:14;
take
E
; ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
A12:
((- 1) (#) f) | E = (- 1) (#) (f | E)
by Th41;
consider A being Element of S such that
A13:
A = (dom f) /\ (dom g)
and
A14:
f is A -measurable
and
A15:
g is A -measurable
by A1;
dom ((- 1) (#) f) = dom f
by VALUED_1:def 5;
then A16:
dom (((- 1) (#) f) + g) = A
by A13, VALUED_1:def 1;
(- 1) (#) f is A -measurable
by A13, A14, MESFUNC6:21, XBOOLE_1:17;
then
0 <= (Integral (M,(((- 1) (#) f) | E))) + (Integral (M,(g | E)))
by A4, A6, A15, A16, MESFUNC6:26, MESFUNC6:84;
then
0 <= ((- 1) * (Integral (M,(f | E)))) + (Integral (M,(g | E)))
by A7, A12, MESFUNC6:102;
then
0 <= (- c1) + c2
by A9, SUPINF_2:1;
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, VALUED_1:def 5; verum