let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
set h = (- 1) (#) f;
A4: (- 1) (#) f is_integrable_on M by A1, MESFUNC5:110;
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 A2, MESFUNC5:109;
A7: ex E3 being Element of S st
( E3 = dom ((- 1) (#) f) & (- 1) (#) f is_measurable_on E3 ) by A4, MESFUNC5:def 17;
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 Real by A9, XXREAL_0:14;
take E ; :: thesis: ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
A10: ((- 1) (#) f) | E = (- 1) (#) (f | E) by Th2;
g + (- f) is nonnegative by A3, MESFUNC2:8;
then A11: ((- 1) (#) 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 Real by A13, XXREAL_0:14;
A14: (R_EAL (- 1)) * (Integral (M,(f | E))) = (- 1) * c1 by EXTREAL1:1;
ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) by A2, MESFUNC5:def 17;
then ex A being Element of S st
( A = dom (((- 1) (#) f) + g) & ((- 1) (#) f) + g is_measurable_on A ) by A7, MESFUNC5:47;
then 0 <= (Integral (M,(((- 1) (#) f) | E))) + (Integral (M,(g | E))) by A6, A11, MESFUNC5:90;
then 0 <= ((R_EAL (- 1)) * (Integral (M,(f | E)))) + (Integral (M,(g | E))) by A12, A10, MESFUNC5:110;
then 0 <= (- c1) + c2 by A14, 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, MESFUNC1:def 6; :: thesis: verum