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 holds
ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (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 holds
ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (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 holds
ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (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 implies ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) )
assume that
A1:
f is_integrable_on M
and
A2:
g is_integrable_on M
; ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
A3:
|.g.| is_integrable_on M
by A2, MESFUNC5:100;
A4:
f + g is_integrable_on M
by A1, A2, MESFUNC5:108;
A5:
|.(f + g).| is_integrable_on M
by A4, MESFUNC5:100;
for x being Element of X st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x
by Th21;
then A6:
(|.f.| + |.g.|) - |.(f + g).| is nonnegative
by Th1;
set G = |.g.|;
set F = |.f.|;
A7: dom |.(f + g).| =
dom (f + g)
by MESFUNC1:def 10
.=
((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty})))
by MESFUNC1:def 3
;
A8:
|.f.| is_integrable_on M
by A1, MESFUNC5:100;
then
|.f.| + |.g.| is_integrable_on M
by A3, MESFUNC5:108;
then consider E being Element of S such that
A9:
E = (dom (|.f.| + |.g.|)) /\ (dom |.(f + g).|)
and
A10:
Integral (M,(|.(f + g).| | E)) <= Integral (M,((|.f.| + |.g.|) | E))
by A5, A6, Th3;
A11:
|.g.| | E is_integrable_on M
by A3, MESFUNC5:97;
|.f.| | E is_integrable_on M
by A8, MESFUNC5:97;
then consider E1 being Element of S such that
A12:
E1 = (dom (|.f.| | E)) /\ (dom (|.g.| | E))
and
A13:
Integral (M,((|.f.| | E) + (|.g.| | E))) = (Integral (M,((|.f.| | E) | E1))) + (Integral (M,((|.g.| | E) | E1)))
by A11, MESFUNC5:109;
take
E
; ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
dom (|.g.| | E) = (dom |.g.|) /\ E
by RELAT_1:61;
then A14:
dom (|.g.| | E) = (dom g) /\ E
by MESFUNC1:def 10;
A15:
dom (|.f.| + |.g.|) = (dom f) /\ (dom g)
by Th19;
then A16:
E = dom |.(f + g).|
by A9, A7, XBOOLE_1:28, XBOOLE_1:36;
dom (|.f.| | E) = (dom |.f.|) /\ E
by RELAT_1:61;
then
dom (|.f.| | E) = (dom f) /\ E
by MESFUNC1:def 10;
then
E1 = (((dom f) /\ E) /\ E) /\ (dom g)
by A12, A14, XBOOLE_1:16;
then
E1 = ((dom f) /\ (E /\ E)) /\ (dom g)
by XBOOLE_1:16;
then
E1 = ((dom f) /\ (dom g)) /\ E
by XBOOLE_1:16;
then A17:
E1 = E
by A9, A15, A7, XBOOLE_1:28, XBOOLE_1:36;
then A18:
(|.g.| | E) | E1 = |.g.| | E
by FUNCT_1:51;
(|.f.| | E) | E1 = |.f.| | E
by A17, FUNCT_1:51;
hence
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
by A10, A13, A16, A18, Th20, MESFUNC1:def 10; verum