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,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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ) ; :: thesis: 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 ;

now :: thesis: for x being Element of X st x in dom ((abs (f1 + g1)) to_power k) holds
|.(((abs (f1 + g1)) to_power k) . x).| <= ((2 to_power k) (#) (((abs f1) to_power k) + ((abs g1) to_power k))) . x

let x be Element of X; :: thesis: ( x in dom ((abs (f1 + g1)) to_power k) implies |.(((abs (f1 + g1)) to_power k) . x).| <= ((2 to_power k) (#) (((abs f1) to_power k) + ((abs g1) to_power k))) . x )
assume x in dom ((abs (f1 + g1)) to_power k) ; :: thesis: |.(((abs (f1 + g1)) to_power k) . x).| <= ((2 to_power k) (#) (((abs f1) to_power k) + ((abs g1) to_power k))) . x
then (abs ((abs (f1 + g1)) to_power k)) . x <= ((2 to_power k) (#) (((abs f1) to_power k) + ((abs g1) to_power k))) . x by A14, Th24, A3, A5, A15;
hence |.(((abs (f1 + g1)) to_power k) . x).| <= ((2 to_power k) (#) (((abs f1) to_power k) + ((abs g1) to_power k))) . x by VALUED_1:18; :: thesis: verum

end;

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; :: thesis: verum