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 m, n being positive Real st (1 / m) + (1 / n) = 1 & f in Lp_Functions M,m & g in Lp_Functions M,m holds
ex r1, r2, r3 being Real st
( r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) & r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for m, n being positive Real st (1 / m) + (1 / n) = 1 & f in Lp_Functions M,m & g in Lp_Functions M,m holds
ex r1, r2, r3 being Real st
( r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) & r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL
for m, n being positive Real st (1 / m) + (1 / n) = 1 & f in Lp_Functions M,m & g in Lp_Functions M,m holds
ex r1, r2, r3 being Real st
( r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) & r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) )
let f, g be PartFunc of X,REAL ; :: thesis: for m, n being positive Real st (1 / m) + (1 / n) = 1 & f in Lp_Functions M,m & g in Lp_Functions M,m holds
ex r1, r2, r3 being Real st
( r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) & r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) )
let m, n be positive Real; :: thesis: ( (1 / m) + (1 / n) = 1 & f in Lp_Functions M,m & g in Lp_Functions M,m implies ex r1, r2, r3 being Real st
( r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) & r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) ) )
assume A1: ( (1 / m) + (1 / n) = 1 & f in Lp_Functions M,m & g in Lp_Functions M,m ) ; :: thesis: ex r1, r2, r3 being Real st
( r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) & r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) )
then ((m + n) * ((m * n) " )) * (m * n) = 1 * (m * n) by XCMPLX_1:213;
then (m + n) * (((m * n) " ) * (m * n)) = m * n ;
then (m + n) * 1 = m * n by XCMPLX_0:def 7;
then A3: m = n * (m - 1) ;
A2: 1 - 1 < m - 1 by A1, Lm300, XREAL_1:16;
then A3b: m - 1 > 0 ;
ex f1 being PartFunc of X,REAL st
( f = f1 & ex NDf being Element of S st
( M . (NDf ` ) = 0 & dom f1 = NDf & f1 is_measurable_on NDf & (abs f1) to_power m is_integrable_on M ) ) by A1;
then consider EDf being Element of S such that
A6: ( M . (EDf ` ) = 0 & dom f = EDf & f is_measurable_on EDf ) ;
ex g1 being PartFunc of X,REAL st
( g = g1 & ex NDg being Element of S st
( M . (NDg ` ) = 0 & dom g1 = NDg & g1 is_measurable_on NDg & (abs g1) to_power m is_integrable_on M ) ) by A1;
then consider EDg being Element of S such that
A8: ( M . (EDg ` ) = 0 & dom g = EDg & g is_measurable_on EDg ) ;
set E = EDf /\ EDg;
A4: f + g in Lp_Functions M,m by A1, Th01aLp;
then A9: ex h1 being PartFunc of X,REAL st
( f + g = h1 & ex NDfg being Element of S st
( M . (NDfg ` ) = 0 & dom h1 = NDfg & h1 is_measurable_on NDfg & (abs h1) to_power m is_integrable_on M ) ) ;
B13: dom (f + g) = EDf /\ EDg by A6, A8, VALUED_1:def 1;
then A13: abs (f + g) is_measurable_on EDf /\ EDg by A9, MESFUNC6:48;
reconsider s1 = Integral M,((abs f) to_power m) as Real by A1, Lm15;
reconsider s2 = Integral M,((abs g) to_power m) as Real by A1, Lm15;
reconsider s3 = Integral M,((abs (f + g)) to_power m) as Real by A4, Lm15;
set t = (abs (f + g)) to_power (m - 1);
B27: dom ((abs (f + g)) to_power (m - 1)) = dom (abs (f + g)) by MESFUN6C:def 6;
then A27: dom ((abs (f + g)) to_power (m - 1)) = EDf /\ EDg by B13, VALUED_1:def 11;
then A34: (abs (f + g)) to_power (m - 1) is_measurable_on EDf /\ EDg by A2, A13, B27, MESFUN6C:29;
A31: ((abs (f + g)) to_power (m - 1)) to_power n = (abs (f + g)) to_power m by A3, A2, LmPW004;
A34a: abs ((abs (f + g)) to_power (m - 1)) = (abs (f + g)) to_power (m - 1) by Lm002b, A3b;
then B34: (abs (f + g)) to_power (m - 1) in Lp_Functions M,n by B13, A27, A31, A9, A34;
then reconsider s4 = Integral M,((abs ((abs (f + g)) to_power (m - 1))) to_power n) as Real by Lm15;
( ((abs (f + g)) to_power (m - 1)) (#) f is_integrable_on M & ((abs (f + g)) to_power (m - 1)) (#) g is_integrable_on M ) by A1, B34, Th001a;
then reconsider u1 = Integral M,(abs (((abs (f + g)) to_power (m - 1)) (#) f)), u2 = Integral M,(abs (((abs (f + g)) to_power (m - 1)) (#) g)) as Real by LPSPACE1:44;
A36: ( dom (abs f) = EDf & dom (abs g) = EDg ) by A6, A8, VALUED_1:def 11;
( dom (((abs (f + g)) to_power (m - 1)) (#) (abs f)) = (dom ((abs (f + g)) to_power (m - 1))) /\ (dom (abs f)) & dom (((abs (f + g)) to_power (m - 1)) (#) (abs g)) = (dom ((abs (f + g)) to_power (m - 1))) /\ (dom (abs g)) ) by VALUED_1:def 4;
then A41: ( dom (((abs (f + g)) to_power (m - 1)) (#) (abs f)) = EDf /\ EDg & dom (((abs (f + g)) to_power (m - 1)) (#) (abs g)) = EDf /\ EDg ) by A27, A36, XBOOLE_1:17, XBOOLE_1:28;
A48: ( abs (((abs (f + g)) to_power (m - 1)) (#) f) = ((abs (f + g)) to_power (m - 1)) (#) (abs f) & abs (((abs (f + g)) to_power (m - 1)) (#) g) = ((abs (f + g)) to_power (m - 1)) (#) (abs g) & abs (((abs (f + g)) to_power (m - 1)) (#) (f + g)) = ((abs (f + g)) to_power (m - 1)) (#) (abs (f + g)) ) by A34a, RFUNCT_1:36;
( ((abs (f + g)) to_power (m - 1)) (#) f is_integrable_on M & ((abs (f + g)) to_power (m - 1)) (#) g is_integrable_on M & ((abs (f + g)) to_power (m - 1)) (#) (f + g) is_integrable_on M ) by A1, B34, A4, Th001a;
then A49: ( ((abs (f + g)) to_power (m - 1)) (#) (abs f) is_integrable_on M & ((abs (f + g)) to_power (m - 1)) (#) (abs g) is_integrable_on M & ((abs (f + g)) to_power (m - 1)) (#) (abs (f + g)) is_integrable_on M ) by A48, LPSPACE1:44;
set F = ((abs (f + g)) to_power (m - 1)) (#) (abs (f + g));
set G = (((abs (f + g)) to_power (m - 1)) (#) (abs f)) + (((abs (f + g)) to_power (m - 1)) (#) (abs g));
C50: dom (((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))) = (EDf /\ EDg) /\ (EDf /\ EDg) by B27, A27, VALUED_1:def 4;
B51: dom ((((abs (f + g)) to_power (m - 1)) (#) (abs f)) + (((abs (f + g)) to_power (m - 1)) (#) (abs g))) = (EDf /\ EDg) /\ (EDf /\ EDg) by A41, VALUED_1:def 1;
R_EAL (((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))) is_integrable_on M by A49, MESFUNC6:def 9;
then ex E1 being Element of S st
( E1 = dom (R_EAL (((abs (f + g)) to_power (m - 1)) (#) (abs (f + g)))) & R_EAL (((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))) is_measurable_on E1 ) by MESFUNC5:def 17;
then A52: ((abs (f + g)) to_power (m - 1)) (#) (abs (f + g)) is_measurable_on EDf /\ EDg by C50, MESFUNC6:def 6;
A53: (((abs (f + g)) to_power (m - 1)) (#) (abs f)) + (((abs (f + g)) to_power (m - 1)) (#) (abs g)) is_integrable_on M by A49, MESFUNC6:100;
for x being Element of X st x in dom (((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))) holds
abs ((((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))) . x) <= ((((abs (f + g)) to_power (m - 1)) (#) (abs f)) + (((abs (f + g)) to_power (m - 1)) (#) (abs g))) . x

proof

let x be Element of X; :: thesis: ( x in dom (((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))) implies abs ((((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))) . x) <= ((((abs (f + g)) to_power (m - 1)) (#) (abs f)) + (((abs (f + g)) to_power (m - 1)) (#) (abs g))) . x )
assume A55: x in dom (((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))) ; :: thesis: abs ((((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))) . x) <= ((((abs (f + g)) to_power (m - 1)) (#) (abs f)) + (((abs (f + g)) to_power (m - 1)) (#) (abs g))) . x
then abs ((f . x) + (g . x)) = abs ((f + g) . x) by B13, C50, VALUED_1:def 1;
then A62: ( abs ((f . x) + (g . x)) = (abs (f + g)) . x & abs (f . x) = (abs f) . x & abs (g . x) = (abs g) . x ) by VALUED_1:18;
(R_EAL (f . x)) + (R_EAL (g . x)) = (f . x) + (g . x) by SUPINF_2:1;
then A59: ( |.(R_EAL (f . x)).| = abs (f . x) & |.(R_EAL (g . x)).| = abs (g . x) & |.((R_EAL (f . x)) + (R_EAL (g . x))).| = abs ((f . x) + (g . x)) ) by EXTREAL2:49;
A68: ( ((abs (f + g)) to_power (m - 1)) . x >= 0 & (abs (f + g)) . x >= 0 ) by A2, MESFUNC6:51;
|.((R_EAL (f . x)) + (R_EAL (g . x))).| <= |.(R_EAL (f . x)).| + |.(R_EAL (g . x)).| by EXTREAL2:61;
then abs ((f . x) + (g . x)) <= (abs (f . x)) + (abs (g . x)) by A59, SUPINF_2:1;
then A69: (((abs (f + g)) to_power (m - 1)) . x) * ((abs (f + g)) . x) <= (((abs (f + g)) to_power (m - 1)) . x) * (((abs f) . x) + ((abs g) . x)) by A62, A68, XREAL_1:66;
( (((abs (f + g)) to_power (m - 1)) . x) * ((abs f) . x) = (((abs (f + g)) to_power (m - 1)) (#) (abs f)) . x & (((abs (f + g)) to_power (m - 1)) . x) * ((abs g) . x) = (((abs (f + g)) to_power (m - 1)) (#) (abs g)) . x ) by VALUED_1:5;
then (((abs (f + g)) to_power (m - 1)) . x) * (((abs f) . x) + ((abs g) . x)) = ((((abs (f + g)) to_power (m - 1)) (#) (abs f)) . x) + ((((abs (f + g)) to_power (m - 1)) (#) (abs g)) . x) ;
then A66: (((abs (f + g)) to_power (m - 1)) . x) * (((abs f) . x) + ((abs g) . x)) = ((((abs (f + g)) to_power (m - 1)) (#) (abs f)) + (((abs (f + g)) to_power (m - 1)) (#) (abs g))) . x by C50, B51, A55, VALUED_1:def 1;
(((abs (f + g)) to_power (m - 1)) . x) * ((abs (f + g)) . x) = (((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))) . x by VALUED_1:5;
hence abs ((((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))) . x) <= ((((abs (f + g)) to_power (m - 1)) (#) (abs f)) + (((abs (f + g)) to_power (m - 1)) (#) (abs g))) . x by A66, A69, A68, ABSVALUE:def 1; :: thesis: verum

end;

then A71: Integral M,(abs (((abs (f + g)) to_power (m - 1)) (#) (abs (f + g)))) <= Integral M,((((abs (f + g)) to_power (m - 1)) (#) (abs f)) + (((abs (f + g)) to_power (m - 1)) (#) (abs g))) by C50, B51, A52, A53, MESFUNC6:96;
A73: ex E1 being Element of S st
( E1 = (EDf /\ EDg) /\ (EDf /\ EDg) & Integral M,((((abs (f + g)) to_power (m - 1)) (#) (abs f)) + (((abs (f + g)) to_power (m - 1)) (#) (abs g))) = (Integral M,((((abs (f + g)) to_power (m - 1)) (#) (abs f)) | E1)) + (Integral M,((((abs (f + g)) to_power (m - 1)) (#) (abs g)) | E1)) ) by A41, A49, MESFUNC6:101;
( Integral M,((((abs (f + g)) to_power (m - 1)) (#) (abs f)) | (EDf /\ EDg)) = Integral M,(((abs (f + g)) to_power (m - 1)) (#) (abs f)) & Integral M,((((abs (f + g)) to_power (m - 1)) (#) (abs g)) | (EDf /\ EDg)) = Integral M,(((abs (f + g)) to_power (m - 1)) (#) (abs g)) ) by A41, RELAT_1:98;
then A87: Integral M,((((abs (f + g)) to_power (m - 1)) (#) (abs f)) + (((abs (f + g)) to_power (m - 1)) (#) (abs g))) = u1 + u2 by A48, A73, SUPINF_2:1;
set v1 = (s4 to_power (1 / n)) * (s1 to_power (1 / m));
set v2 = (s4 to_power (1 / n)) * (s2 to_power (1 / m));
( ex r4 being Real st
( r4 = Integral M,((abs ((abs (f + g)) to_power (m - 1))) to_power n) & ex r1 being Real st
( r1 = Integral M,((abs f) to_power m) & Integral M,(abs (((abs (f + g)) to_power (m - 1)) (#) f)) <= (r4 to_power (1 / n)) * (r1 to_power (1 / m)) ) ) & ex r4 being Real st
( r4 = Integral M,((abs ((abs (f + g)) to_power (m - 1))) to_power n) & ex r2 being Real st
( r2 = Integral M,((abs g) to_power m) & Integral M,(abs (((abs (f + g)) to_power (m - 1)) (#) g)) <= (r4 to_power (1 / n)) * (r2 to_power (1 / m)) ) ) ) by A1, B34, Th001;
then A88: u1 + u2 <= ((s4 to_power (1 / n)) * (s1 to_power (1 / m))) + ((s4 to_power (1 / n)) * (s2 to_power (1 / m))) by XREAL_1:9;
((abs (f + g)) to_power (m - 1)) (#) (abs (f + g)) = ((abs (f + g)) to_power (m - 1)) (#) ((abs (f + g)) to_power 1) by LmPW006
.= (abs (f + g)) to_power ((m - 1) + 1) by LmPW005, A2 ;
then Integral M,(abs (((abs (f + g)) to_power (m - 1)) (#) (abs (f + g)))) = s3 by Lm002b;
then A92: s3 <= ((s3 to_power (1 / n)) * (s1 to_power (1 / m))) + ((s3 to_power (1 / n)) * (s2 to_power (1 / m))) by A31, A34a, A71, A87, A88, XXREAL_0:2;

per cases ( s3 = 0 or s3 > 0 ) by A4, Lm15;

suppose s3 = 0 ; :: thesis: ex r1, r2, r3 being Real st
( r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) & r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) )

then A96: s3 to_power (1 / m) = 0 by POWER:def 2;
( s1 to_power (1 / m) >= 0 & s2 to_power (1 / m) >= 0 ) by A1, Lm15, LmPW001;
then s3 to_power (1 / m) <= (s1 to_power (1 / m)) + (s2 to_power (1 / m)) by A96;
hence ex r1, r2, r3 being Real st
( r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) & r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) ) ; :: thesis: verum

end;

suppose A98: s3 > 0 ; :: thesis: ex r1, r2, r3 being Real st
( r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) & r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) )

then A99: s3 to_power (1 / n) > 0 by POWER:39;
set w1 = s3 to_power (1 / n);
(1 / (s3 to_power (1 / n))) * (((s3 to_power (1 / n)) * (s1 to_power (1 / m))) + ((s3 to_power (1 / n)) * (s2 to_power (1 / m)))) = ((1 / (s3 to_power (1 / n))) * (s3 to_power (1 / n))) * ((s1 to_power (1 / m)) + (s2 to_power (1 / m))) ;
then A101: (1 / (s3 to_power (1 / n))) * (((s3 to_power (1 / n)) * (s1 to_power (1 / m))) + ((s3 to_power (1 / n)) * (s2 to_power (1 / m)))) = 1 * ((s1 to_power (1 / m)) + (s2 to_power (1 / m))) by A99, XCMPLX_1:107;
(1 / (s3 to_power (1 / n))) * s3 = (s3 to_power (- (1 / n))) * s3 by A98, POWER:33
.= (s3 to_power (- (1 / n))) * (s3 to_power 1) by POWER:30
.= s3 to_power ((- (1 / n)) + 1) by A98, POWER:32
.= s3 to_power (1 / m) by A1 ;
hence ex r1, r2, r3 being Real st
( r1 = Integral M,((abs f) to_power m) & r2 = Integral M,((abs g) to_power m) & r3 = Integral M,((abs (f + g)) to_power m) & r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) ) by A99, A101, A92, XREAL_1:66; :: thesis: verum

end;

end;