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:211;
then (m + n) * (((m * n) ") * (m * n)) = m * n ;
then (m + n) * 1 = m * n by XCMPLX_0:def 7;
then A2: m = n * (m - 1) ;
A3: 1 - 1 < m - 1 by A1, Th1, XREAL_1:14;
then A4: 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 NDf -measurable & (abs f1) to_power m is_integrable_on M ) ) by A1;
then consider EDf being Element of S such that
A5: ( M . (EDf `) = 0 & dom f = EDf & f is EDf -measurable ) ;
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 NDg -measurable & (abs g1) to_power m is_integrable_on M ) ) by A1;
then consider EDg being Element of S such that
A6: ( M . (EDg `) = 0 & dom g = EDg & g is EDg -measurable ) ;
set E = EDf /\ EDg;
A7: f + g in Lp_Functions (M,m) by A1, Th25;
then A8: 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 NDfg -measurable & (abs h1) to_power m is_integrable_on M ) ) ;
A9: dom (f + g) = EDf /\ EDg by A5, A6, VALUED_1:def 1;
then A10: abs (f + g) is EDf /\ EDg -measurable by A8, MESFUNC6:48;
reconsider s1 = Integral (M,((abs f) to_power m)) as Element of REAL by A1, Th49;
reconsider s2 = Integral (M,((abs g) to_power m)) as Element of REAL by A1, Th49;
reconsider s3 = Integral (M,((abs (f + g)) to_power m)) as Element of REAL by A7, Th49;
set t = (abs (f + g)) to_power (m - 1);
A11: dom ((abs (f + g)) to_power (m - 1)) = dom (abs (f + g)) by MESFUN6C:def 4;
then A12: dom ((abs (f + g)) to_power (m - 1)) = EDf /\ EDg by A9, VALUED_1:def 11;
then A13: (abs (f + g)) to_power (m - 1) is EDf /\ EDg -measurable by A3, A10, A11, MESFUN6C:29;
A14: ((abs (f + g)) to_power (m - 1)) to_power n = (abs (f + g)) to_power m by A2, A3, Th6;
A15: abs ((abs (f + g)) to_power (m - 1)) = (abs (f + g)) to_power (m - 1) by Th14, A4;
then A16: (abs (f + g)) to_power (m - 1) in Lp_Functions (M,n) by A9, A12, A14, A8, A13;
then reconsider s4 = Integral (M,((abs ((abs (f + g)) to_power (m - 1))) to_power n)) as Element of REAL by Th49;
( ((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, A16, Th59;
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 Element of REAL by LPSPACE1:44;
A17: ( dom (abs f) = EDf & dom (abs g) = EDg ) by A5, A6, 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 A18: ( 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 A12, A17, XBOOLE_1:17, XBOOLE_1:28;
A19: ( 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 A15, RFUNCT_1:24;
( ((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, A16, A7, Th59;
then A20: ( ((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 A19, 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));
A21: dom (((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))) = (EDf /\ EDg) /\ (EDf /\ EDg) by A11, A12, VALUED_1:def 4;
A22: dom ((((abs (f + g)) to_power (m - 1)) (#) (abs f)) + (((abs (f + g)) to_power (m - 1)) (#) (abs g))) = (EDf /\ EDg) /\ (EDf /\ EDg) by A18, VALUED_1:def 1;
R_EAL (((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))) is_integrable_on M by A20;
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 E1 -measurable ) ;
then A23: ((abs (f + g)) to_power (m - 1)) (#) (abs (f + g)) is EDf /\ EDg -measurable by A21;
A24: (((abs (f + g)) to_power (m - 1)) (#) (abs f)) + (((abs (f + g)) to_power (m - 1)) (#) (abs g)) is_integrable_on M by A20, MESFUNC6:100;
for x being Element of X st x in dom (((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))) holds
|.((((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 (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 A25: x in dom (((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))) ; :: thesis: |.((((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 |.((f . x) + (g . x)).| = |.((f + g) . x).| by A9, A21, VALUED_1:def 1;
then A26: ( |.((f . x) + (g . x)).| = (abs (f + g)) . x & |.(f . x).| = (abs f) . x & |.(g . x).| = (abs g) . x ) by VALUED_1:18;
A27: ( |.(f . x).| = |.(f . x).| & |.(g . x).| = |.(g . x).| & |.((f . x) + (g . x)).| = |.((f . x) + (g . x)).| ) ;
A28: ( ((abs (f + g)) to_power (m - 1)) . x >= 0 & (abs (f + g)) . x >= 0 ) by A3, MESFUNC6:51;
reconsider fx = f . x, gx = g . x as R_eal by XXREAL_0:def 1;
A29: fx + gx = (f . x) + (g . x) by SUPINF_2:1;
|.(fx + gx).| <= |.fx.| + |.gx.| by EXTREAL1:24;
then |.((f . x) + (g . x)).| <= |.fx.| + |.gx.| by A29;
then |.((f . x) + (g . x)).| <= |.(f . x).| + |.(g . x).| by A27, SUPINF_2:1;
then A30: (((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 A26, A28, XREAL_1:64;
( (((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 A31: (((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 A21, A22, A25, 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 (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 A31, A30, A28, ABSVALUE:def 1; :: thesis: verum

end;

then A32: 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 A21, A22, A23, A24, MESFUNC6:96;
A33: 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 A18, A20, 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 A18, RELAT_1:69;
then A34: Integral (M,((((abs (f + g)) to_power (m - 1)) (#) (abs f)) + (((abs (f + g)) to_power (m - 1)) (#) (abs g)))) = u1 + u2 by A19, A33, 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, A16, Th60;
then A35: 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:7;
((abs (f + g)) to_power (m - 1)) (#) (abs (f + g)) = ((abs (f + g)) to_power (m - 1)) (#) ((abs (f + g)) to_power 1) by Th8
.= (abs (f + g)) to_power ((m - 1) + 1) by Th7, A3 ;
then Integral (M,(abs (((abs (f + g)) to_power (m - 1)) (#) (abs (f + g))))) = s3 by Th14;
then A36: s3 <= ((s3 to_power (1 / n)) * (s1 to_power (1 / m))) + ((s3 to_power (1 / n)) * (s2 to_power (1 / m))) by A14, A15, A32, A34, A35, XXREAL_0:2;

per cases ( s3 = 0 or s3 > 0 ) by A7, Th49;

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 A37: s3 to_power (1 / m) = 0 by POWER:def 2;
( s1 to_power (1 / m) >= 0 & s2 to_power (1 / m) >= 0 ) by A1, Th49, Th4;
then s3 to_power (1 / m) <= (s1 to_power (1 / m)) + (s2 to_power (1 / m)) by A37;
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 A38: 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 A39: s3 to_power (1 / n) > 0 by POWER:34;
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 A40: (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 A39, XCMPLX_1:106;
(1 / (s3 to_power (1 / n))) * s3 = (s3 to_power (- (1 / n))) * s3 by A38, POWER:28
.= (s3 to_power (- (1 / n))) * (s3 to_power 1) by POWER:25
.= s3 to_power ((- (1 / n)) + 1) by A38, POWER:27
.= 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 A39, A40, A36, XREAL_1:64; :: thesis: verum

end;

end;