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 f is_integrable_on M & g is_integrable_on M holds
Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g)))
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g)))
let M be sigma_Measure of S; for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g)))
let f, g be PartFunc of X,REAL; ( f is_integrable_on M & g is_integrable_on M implies Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g))) )
set f1 = R_EAL f;
set g1 = R_EAL g;
assume that
A1:
f is_integrable_on M
and
A2:
g is_integrable_on M
; Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g)))
A3:
R_EAL f is_integrable_on M
by A1;
then consider B being Element of S such that
A4:
B = dom (R_EAL f)
and
R_EAL f is B -measurable
;
A5:
B = dom |.(R_EAL f).|
by A4, MESFUNC1:def 10;
|.(R_EAL f).| is_integrable_on M
by A3, MESFUNC5:100;
then A6:
ex E being Element of S st
( E = dom |.(R_EAL f).| & |.(R_EAL f).| is E -measurable )
;
A7:
R_EAL g is_integrable_on M
by A2;
then consider C being Element of S such that
A8:
C = dom (R_EAL g)
and
R_EAL g is C -measurable
;
A9:
C = dom |.(R_EAL g).|
by A8, MESFUNC1:def 10;
consider E being Element of S such that
A10:
E = dom ((R_EAL f) + (R_EAL g))
and
A11:
Integral (M,(|.((R_EAL f) + (R_EAL g)).| | E)) <= (Integral (M,(|.(R_EAL f).| | E))) + (Integral (M,(|.(R_EAL g).| | E)))
by A3, A7, MESFUNC7:22;
dom |.((R_EAL f) + (R_EAL g)).| = E
by A10, MESFUNC1:def 10;
then
( (R_EAL f) + (R_EAL g) = R_EAL (f + g) & |.((R_EAL f) + (R_EAL g)).| | E = |.((R_EAL f) + (R_EAL g)).| )
by MESFUNC6:23, RELAT_1:68;
then A12:
Integral (M,(|.((R_EAL f) + (R_EAL g)).| | E)) = Integral (M,|.(f + g).|)
by MESFUNC6:1;
|.(R_EAL g).| is_integrable_on M
by A7, MESFUNC5:100;
then A13:
ex E being Element of S st
( E = dom |.(R_EAL g).| & |.(R_EAL g).| is E -measurable )
;
A14:
E = ((dom (R_EAL f)) /\ (dom (R_EAL g))) \ ((((R_EAL f) " {-infty}) /\ ((R_EAL g) " {+infty})) \/ (((R_EAL f) " {+infty}) /\ ((R_EAL g) " {-infty})))
by A10, MESFUNC1:def 3;
then
E c= dom (R_EAL g)
by XBOOLE_1:18, XBOOLE_1:36;
then
E c= dom |.(R_EAL g).|
by MESFUNC1:def 10;
then
Integral (M,(|.(R_EAL g).| | E)) <= Integral (M,(|.(R_EAL g).| | C))
by A9, A13, MESFUNC5:93;
then
Integral (M,(|.(R_EAL g).| | E)) <= Integral (M,|.(R_EAL g).|)
by A9, RELAT_1:68;
then A15:
Integral (M,(|.(R_EAL g).| | E)) <= Integral (M,|.g.|)
by MESFUNC6:1;
E c= dom (R_EAL f)
by A14, XBOOLE_1:18, XBOOLE_1:36;
then
E c= dom |.(R_EAL f).|
by MESFUNC1:def 10;
then
Integral (M,(|.(R_EAL f).| | E)) <= Integral (M,(|.(R_EAL f).| | B))
by A5, A6, MESFUNC5:93;
then
Integral (M,(|.(R_EAL f).| | E)) <= Integral (M,|.(R_EAL f).|)
by A5, RELAT_1:68;
then
Integral (M,(|.(R_EAL f).| | E)) <= Integral (M,|.f.|)
by MESFUNC6:1;
then
(Integral (M,(|.(R_EAL f).| | E))) + (Integral (M,(|.(R_EAL g).| | E))) <= (Integral (M,|.f.|)) + (Integral (M,|.g.|))
by A15, XXREAL_3:36;
hence
Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g)))
by A11, A12, XXREAL_0:2; verum