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 ;
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 ;
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 ;
then A10: abs (f + g) is EDf /\ EDg -measurable by ;
reconsider s1 = Integral (M,((abs f) to_power m)) as Element of REAL by ;
reconsider s2 = Integral (M,((abs g) to_power m)) as Element of REAL by ;
reconsider s3 = Integral (M,((abs (f + g)) to_power m)) as Element of REAL by ;
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 ;
then A13: (abs (f + g)) to_power (m - 1) is EDf /\ EDg -measurable by ;
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 ;
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 ;
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 ;
( 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 ;
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 ;
( ((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 ;
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 ;
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 ;
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 ;
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 ;
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 ;
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 ;
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 ;
( (((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 ;
(((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 ; :: 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 ;
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 ;
( 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 ;
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 ;
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 ;
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 ;
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 ;
per cases ( s3 = 0 or s3 > 0 ) by ;
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 ;
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 ;
(1 / (s3 to_power (1 / n))) * s3 = (s3 to_power (- (1 / n))) * s3 by
.= (s3 to_power (- (1 / n))) * (s3 to_power 1) by POWER:25
.= s3 to_power ((- (1 / n)) + 1) by
.= 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 ; :: thesis: verum
end;
end;