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,COMPLEX st f in L1_CFunctions M & g in L1_CFunctions M holds
Integral (M,|.(f + g).|) <= (Integral (M,|.f.|)) + (Integral (M,|.g.|))
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f in L1_CFunctions M & g in L1_CFunctions M holds
Integral (M,|.(f + g).|) <= (Integral (M,|.f.|)) + (Integral (M,|.g.|))
let M be sigma_Measure of S; for f, g being PartFunc of X,COMPLEX st f in L1_CFunctions M & g in L1_CFunctions M holds
Integral (M,|.(f + g).|) <= (Integral (M,|.f.|)) + (Integral (M,|.g.|))
let f, g be PartFunc of X,COMPLEX; ( f in L1_CFunctions M & g in L1_CFunctions M implies Integral (M,|.(f + g).|) <= (Integral (M,|.f.|)) + (Integral (M,|.g.|)) )
assume that
A1:
f in L1_CFunctions M
and
A2:
g in L1_CFunctions M
; Integral (M,|.(f + g).|) <= (Integral (M,|.f.|)) + (Integral (M,|.g.|))
ex f1 being PartFunc of X,COMPLEX st
( f = f1 & ex NDf being Element of S st
( M . NDf = 0 & dom f1 = NDf ` & f1 is_integrable_on M ) )
by A1;
then consider NDf1 being Element of S such that
A3:
M . NDf1 = 0
and
A4:
( dom f = NDf1 ` & f is_integrable_on M )
;
R_EAL |.f.| is_integrable_on M
by A4, Th37, MESFUNC6:def 4;
then consider Ef being Element of S such that
A5:
Ef = dom (R_EAL |.f.|)
and
A6:
R_EAL |.f.| is Ef -measurable
;
ex g1 being PartFunc of X,COMPLEX st
( g = g1 & ex NDg being Element of S st
( M . NDg = 0 & dom g1 = NDg ` & g1 is_integrable_on M ) )
by A2;
then consider NDg1 being Element of S such that
A7:
M . NDg1 = 0
and
A8:
( dom g = NDg1 ` & g is_integrable_on M )
;
R_EAL |.g.| is_integrable_on M
by A8, Th37, MESFUNC6:def 4;
then consider Eg being Element of S such that
A9:
Eg = dom (R_EAL |.g.|)
and
A10:
R_EAL |.g.| is Eg -measurable
;
consider E being Element of S such that
A11:
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
by A4, A8, MESFUN7C:42;
A12:
dom |.(f + g).| = E
by A11, VALUED_1:def 11;
set NF = (NDf1 `) /\ NDg1;
set NG = (NDg1 `) /\ NDf1;
( NDf1 ` is Element of S & NDg1 ` is Element of S )
by MEASURE1:def 1;
then A13:
( (NDf1 `) /\ NDg1 is Element of S & (NDg1 `) /\ NDf1 is Element of S & Ef is Element of S & Eg is Element of S )
by MEASURE1:11;
A14:
Ef = NDf1 `
by A4, A5, VALUED_1:def 11;
A15:
Eg = NDg1 `
by A8, A9, VALUED_1:def 11;
then A16:
E = Ef /\ Eg
by A11, A14, A4, A8, VALUED_1:def 1;
A17: Ef \ Eg =
((X \ NDf1) \ X) \/ ((X \ NDf1) /\ NDg1)
by A14, A15, XBOOLE_1:52
.=
(X \ (NDf1 \/ X)) \/ ((X \ NDf1) /\ NDg1)
by XBOOLE_1:41
.=
(X \ X) \/ ((X \ NDf1) /\ NDg1)
by XBOOLE_1:12
.=
{} \/ ((X \ NDf1) /\ NDg1)
by XBOOLE_1:37
.=
(NDf1 `) /\ NDg1
;
A18:
E = Ef \ (Ef \ Eg)
by A16, XBOOLE_1:48;
A19: Eg \ Ef =
((X \ NDg1) \ X) \/ ((X \ NDg1) /\ NDf1)
by A14, A15, XBOOLE_1:52
.=
(X \ (NDg1 \/ X)) \/ ((X \ NDg1) /\ NDf1)
by XBOOLE_1:41
.=
(X \ X) \/ ((X \ NDg1) /\ NDf1)
by XBOOLE_1:12
.=
{} \/ ((X \ NDg1) /\ NDf1)
by XBOOLE_1:37
.=
(NDg1 `) /\ NDf1
;
A20:
E = Eg \ (Eg \ Ef)
by A16, XBOOLE_1:48;
( NDf1 is measure_zero of M & NDg1 is measure_zero of M )
by A3, A7, MEASURE1:def 7;
then
( (NDf1 `) /\ NDg1 is measure_zero of M & (NDg1 `) /\ NDf1 is measure_zero of M )
by A13, MEASURE1:36, XBOOLE_1:17;
then A21:
( M . ((NDf1 `) /\ NDg1) = 0 & M . ((NDg1 `) /\ NDf1) = 0 )
by MEASURE1:def 7;
A22:
Integral (M,(|.f.| | E)) = Integral (M,|.f.|)
by A18, A17, A6, MESFUNC6:def 1, A5, A21, MESFUNC6:89;
Integral (M,(|.g.| | E)) = Integral (M,|.g.|)
by A10, MESFUNC6:def 1, A9, A21, A20, A19, MESFUNC6:89;
hence
Integral (M,|.(f + g).|) <= (Integral (M,|.f.|)) + (Integral (M,|.g.|))
by A11, A12, RELAT_1:69, A22; verum