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
for k being positive Real st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) holds
f + g in Lp_Functions (M,k)
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for k being positive Real st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) holds
f + g in Lp_Functions (M,k)
let M be sigma_Measure of S; for f, g being PartFunc of X,REAL
for k being positive Real st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) holds
f + g in Lp_Functions (M,k)
let f, g be PartFunc of X,REAL; for k being positive Real st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) holds
f + g in Lp_Functions (M,k)
let k be positive Real; ( f in Lp_Functions (M,k) & g in Lp_Functions (M,k) implies f + g in Lp_Functions (M,k) )
set W = Lp_Functions (M,k);
assume A1:
( f in Lp_Functions (M,k) & g in Lp_Functions (M,k) )
; f + g in Lp_Functions (M,k)
then consider f1 being PartFunc of X,REAL such that
A2:
( f1 = f & ex Ef1 being Element of S st
( M . (Ef1 `) = 0 & dom f1 = Ef1 & f1 is Ef1 -measurable & (abs f1) to_power k is_integrable_on M ) )
;
consider Ef being Element of S such that
A3:
( M . (Ef `) = 0 & dom f1 = Ef & f1 is Ef -measurable & (abs f1) to_power k is_integrable_on M )
by A2;
consider g1 being PartFunc of X,REAL such that
A4:
( g1 = g & ex Eg1 being Element of S st
( M . (Eg1 `) = 0 & dom g1 = Eg1 & g1 is Eg1 -measurable & (abs g1) to_power k is_integrable_on M ) )
by A1;
consider Eg being Element of S such that
A5:
( M . (Eg `) = 0 & dom g1 = Eg & g1 is Eg -measurable & (abs g1) to_power k is_integrable_on M )
by A4;
A6:
dom (f1 + g1) = Ef /\ Eg
by A3, A5, VALUED_1:def 1;
set Efg = Ef /\ Eg;
set s = (abs (f1 + g1)) to_power k;
set t = (2 to_power k) (#) (((abs f1) to_power k) + ((abs g1) to_power k));
A7:
(Ef /\ Eg) ` = (X \ Ef) \/ (X \ Eg)
by XBOOLE_1:54;
( Ef ` is Element of S & Eg ` is Element of S )
by MEASURE1:34;
then
( Ef ` is measure_zero of M & Eg ` is measure_zero of M )
by A3, A5, MEASURE1:def 7;
then
(Ef `) \/ (Eg `) is measure_zero of M
by MEASURE1:37;
then A8:
M . ((Ef /\ Eg) `) = 0
by A7, MEASURE1:def 7;
( f1 is Ef /\ Eg -measurable & g1 is Ef /\ Eg -measurable )
by A3, A5, MESFUNC6:16, XBOOLE_1:17;
then A9:
f1 + g1 is Ef /\ Eg -measurable
by MESFUNC6:26;
then A10:
abs (f1 + g1) is Ef /\ Eg -measurable
by A6, MESFUNC6:48;
((abs f1) to_power k) + ((abs g1) to_power k) is_integrable_on M
by A1, A2, A4, Th22;
then A11:
(2 to_power k) (#) (((abs f1) to_power k) + ((abs g1) to_power k)) is_integrable_on M
by MESFUNC6:102;
A12:
( dom (abs f1) = dom f1 & dom (abs g1) = dom g1 & dom (abs (f1 + g1)) = dom (f1 + g1) )
by VALUED_1:def 11;
then A13:
(abs (f1 + g1)) to_power k is Ef /\ Eg -measurable
by A6, A10, MESFUN6C:29;
A14:
abs ((abs (f1 + g1)) to_power k) = (abs (f1 + g1)) to_power k
by Th14;
A15:
dom ((abs (f1 + g1)) to_power k) = Ef /\ Eg
by A6, A12, MESFUN6C:def 4;
A16: dom ((2 to_power k) (#) (((abs f1) to_power k) + ((abs g1) to_power k))) =
dom (((abs f1) to_power k) + ((abs g1) to_power k))
by VALUED_1:def 5
.=
(dom ((abs f1) to_power k)) /\ (dom ((abs g1) to_power k))
by VALUED_1:def 1
.=
(dom (abs f1)) /\ (dom ((abs g1) to_power k))
by MESFUN6C:def 4
.=
(dom (abs f1)) /\ (dom (abs g1))
by MESFUN6C:def 4
.=
dom (f1 + g1)
by A12, VALUED_1:def 1
.=
dom ((abs (f1 + g1)) to_power k)
by A12, MESFUN6C:def 4
;
then
(abs (f1 + g1)) to_power k is_integrable_on M
by A13, A15, A16, A11, MESFUNC6:96;
hence
f + g in Lp_Functions (M,k)
by A2, A4, A8, A6, A9; verum