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,n) holds
ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )

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,n) holds
ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )

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,n) holds
ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )

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,n) holds
ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )

let m, n be positive Real; :: thesis: ( (1 / m) + (1 / n) = 1 & f in Lp_Functions (M,m) & g in Lp_Functions (M,n) implies ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) ) )

assume A1: ( (1 / m) + (1 / n) = 1 & f in Lp_Functions (M,m) & g in Lp_Functions (M,n) ) ; :: thesis: ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )

then A2: ( m > 1 & n > 1 ) by Th1;
consider f1 being PartFunc of X,REAL such that
A3: ( 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;
consider EDf being Element of S such that
A4: ( M . (EDf `) = 0 & dom f1 = EDf & f1 is EDf -measurable ) by A3;
consider g1 being PartFunc of X,REAL such that
A5: ( g = g1 & ex NDg being Element of S st
( M . (NDg `) = 0 & dom g1 = NDg & g1 is NDg -measurable & (abs g1) to_power n is_integrable_on M ) ) by A1;
consider EDg being Element of S such that
A6: ( M . (EDg `) = 0 & dom g1 = EDg & g1 is EDg -measurable ) by A5;
set u = (abs f1) to_power m;
set v = (abs g1) to_power n;
A7: ( 0 <= Integral (M,((abs f1) to_power m)) & 0 <= Integral (M,((abs g1) to_power n)) ) by A3, A5, A1, Th49;
reconsider s1 = Integral (M,((abs f1) to_power m)), s2 = Integral (M,((abs g1) to_power n)) as Element of REAL by A3, A5, A1, Th49;
A8: ( dom f1 = dom (abs f1) & dom g1 = dom (abs g1) ) by VALUED_1:def 11;
reconsider Nf = EDf ` , Ng = EDg ` as Element of S by MEASURE1:34;
set t1 = s1 to_power (1 / m);
set t2 = s2 to_power (1 / n);
set E = EDf /\ EDg;
A9: (EDf /\ EDg) ` = (EDf `) \/ (EDg `) by XBOOLE_1:54;
( Nf is measure_zero of M & Ng is measure_zero of M ) by ;
then A10: (EDf /\ EDg) ` is measure_zero of M by ;
A11: dom (f1 (#) g1) = EDf /\ EDg by ;
( f1 is EDf /\ EDg -measurable & g1 is EDf /\ EDg -measurable ) by ;
then A12: f1 (#) g1 is EDf /\ EDg -measurable by ;
A13: f1 (#) g1 in L1_Functions M by A1, A3, A5, Th59;
then A14: ex fg1 being PartFunc of X,REAL st
( fg1 = f1 (#) g1 & ex ND being Element of S st
( M . ND = 0 & dom fg1 = ND ` & fg1 is_integrable_on M ) ) ;
then A15: ( Integral (M,(abs (f1 (#) g1))) in REAL & abs (f1 (#) g1) is_integrable_on M ) by LPSPACE1:44;
per cases ( ( s1 = 0 & s2 >= 0 ) or ( s1 > 0 & s2 = 0 ) or ( s1 <> 0 & s2 <> 0 ) ) by A3, A5, A1, Th49;
suppose A16: ( s1 = 0 & s2 >= 0 ) ; :: thesis: ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )

f1 in Lp_Functions (M,m) by A3;
then f1 a.e.= X --> 0,M by ;
then consider Nf1 being Element of S such that
A17: ( M . Nf1 = 0 & f1 | (Nf1 `) = (X --> 0) | (Nf1 `) ) ;
reconsider Z = ((EDf /\ EDg) \ Nf1) ` as Element of S by MEASURE1:34;
A18: ((EDf /\ EDg) \ Nf1) ` = ((EDf /\ EDg) `) \/ Nf1 by SUBSET_1:14;
Nf1 is measure_zero of M by ;
then Z is measure_zero of M by ;
then A19: M . Z = 0 by MEASURE1:def 7;
dom (X --> 0) = X by FUNCOP_1:13;
then A20: dom ((X --> 0) | (Z `)) = Z ` by RELAT_1:62;
A21: dom ((f1 (#) g1) | (Z `)) = Z ` by ;
for x being object st x in dom ((f1 (#) g1) | (Z `)) holds
((f1 (#) g1) | (Z `)) . x = ((X --> 0) | (Z `)) . x
proof
let x be object ; :: thesis: ( x in dom ((f1 (#) g1) | (Z `)) implies ((f1 (#) g1) | (Z `)) . x = ((X --> 0) | (Z `)) . x )
assume A22: x in dom ((f1 (#) g1) | (Z `)) ; :: thesis: ((f1 (#) g1) | (Z `)) . x = ((X --> 0) | (Z `)) . x
then ( x in X & not x in Nf1 ) by ;
then x in Nf1 ` by XBOOLE_0:def 5;
then ( f1 . x = (f1 | (Nf1 `)) . x & (X --> 0) . x = ((X --> 0) | (Nf1 `)) . x ) by FUNCT_1:49;
then A23: f1 . x = 0 by ;
A24: dom ((f1 (#) g1) | (Z `)) c= dom (f1 (#) g1) by RELAT_1:60;
((f1 (#) g1) | (Z `)) . x = (f1 (#) g1) . x by
.= (f1 . x) * (g1 . x) by
.= ((Z `) --> 0) . x by
.= ((X /\ (Z `)) --> 0) . x by XBOOLE_1:28 ;
hence ((f1 (#) g1) | (Z `)) . x = ((X --> 0) | (Z `)) . x by FUNCOP_1:12; :: thesis: verum
end;
then (f1 (#) g1) | (Z `) = (X --> 0) | (Z `) by ;
then A25: f1 (#) g1 a.e.= X --> 0,M by A19;
X --> 0 in L1_Functions M by Th56;
then Integral (M,(abs (f1 (#) g1))) = Integral (M,(abs (X --> 0))) by ;
then A26: Integral (M,(abs (f1 (#) g1))) = 0 by LPSPACE1:54;
(s1 to_power (1 / m)) * (s2 to_power (1 / n)) = 0 * (s2 to_power (1 / n)) by ;
hence ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) ) by A3, A5, A26; :: thesis: verum
end;
suppose A27: ( s1 > 0 & s2 = 0 ) ; :: thesis: ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )

g1 in Lp_Functions (M,n) by A5;
then g1 a.e.= X --> 0,M by ;
then consider Ng1 being Element of S such that
A28: ( M . Ng1 = 0 & g1 | (Ng1 `) = (X --> 0) | (Ng1 `) ) ;
reconsider Z = ((EDf /\ EDg) \ Ng1) ` as Element of S by MEASURE1:34;
A29: ((EDf /\ EDg) \ Ng1) ` = ((EDf /\ EDg) `) \/ Ng1 by SUBSET_1:14;
Ng1 is measure_zero of M by ;
then Z is measure_zero of M by ;
then A30: M . Z = 0 by MEASURE1:def 7;
dom (X --> 0) = X by FUNCOP_1:13;
then A31: dom ((X --> 0) | (Z `)) = Z ` by RELAT_1:62;
A32: dom ((f1 (#) g1) | (Z `)) = Z ` by ;
for x being object st x in dom ((f1 (#) g1) | (Z `)) holds
((f1 (#) g1) | (Z `)) . x = ((X --> 0) | (Z `)) . x
proof
let x be object ; :: thesis: ( x in dom ((f1 (#) g1) | (Z `)) implies ((f1 (#) g1) | (Z `)) . x = ((X --> 0) | (Z `)) . x )
assume A33: x in dom ((f1 (#) g1) | (Z `)) ; :: thesis: ((f1 (#) g1) | (Z `)) . x = ((X --> 0) | (Z `)) . x
then ( x in X & not x in Ng1 ) by ;
then x in Ng1 ` by XBOOLE_0:def 5;
then ( g1 . x = (g1 | (Ng1 `)) . x & (X --> 0) . x = ((X --> 0) | (Ng1 `)) . x ) by FUNCT_1:49;
then A34: g1 . x = 0 by ;
A35: dom ((f1 (#) g1) | (Z `)) c= dom (f1 (#) g1) by RELAT_1:60;
((f1 (#) g1) | (Z `)) . x = (f1 (#) g1) . x by
.= (f1 . x) * (g1 . x) by
.= ((Z `) --> 0) . x by
.= ((X /\ (Z `)) --> 0) . x by XBOOLE_1:28 ;
hence ((f1 (#) g1) | (Z `)) . x = ((X --> 0) | (Z `)) . x by FUNCOP_1:12; :: thesis: verum
end;
then (f1 (#) g1) | (Z `) = (X --> 0) | (Z `) by ;
then A36: f1 (#) g1 a.e.= X --> 0,M by A30;
X --> 0 in L1_Functions M by Th56;
then Integral (M,(abs (f1 (#) g1))) = Integral (M,(abs (X --> 0))) by ;
then A37: Integral (M,(abs (f1 (#) g1))) = 0 by LPSPACE1:54;
(s1 to_power (1 / m)) * (s2 to_power (1 / n)) = (s1 to_power (1 / m)) * 0 by ;
hence ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) ) by A3, A5, A37; :: thesis: verum
end;
suppose A38: ( s1 <> 0 & s2 <> 0 ) ; :: thesis: ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )

then A39: ( s1 to_power (1 / m) > 0 & s2 to_power (1 / n) > 0 ) by ;
then A40: |.(1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))).| = 1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n))) by ABSVALUE:def 1;
set w = (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1);
set F = (1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m);
set G = (1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n);
set z = ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n));
A41: ( dom ((1 / (s1 to_power (1 / m))) (#) (abs f1)) = dom (abs f1) & dom ((1 / (s2 to_power (1 / n))) (#) (abs g1)) = dom (abs g1) ) by VALUED_1:def 5;
( dom ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) = dom (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) & dom ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) = dom (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) ) by VALUED_1:def 5;
then A42: ( dom ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) = dom (abs f1) & dom ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) = dom (abs g1) ) by ;
then A43: dom (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) = (dom (abs f1)) /\ (dom (abs g1)) by VALUED_1:def 1;
( ((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m = ((1 / (s1 to_power (1 / m))) to_power m) (#) ((abs f1) to_power m) & ((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n = ((1 / (s2 to_power (1 / n))) to_power n) (#) ((abs g1) to_power n) ) by ;
then A44: ( ((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m is_integrable_on M & ((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n is_integrable_on M ) by ;
then A45: ( (1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) is_integrable_on M & (1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) is_integrable_on M ) by MESFUNC6:102;
then A46: ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) is_integrable_on M by MESFUNC6:100;
A47: dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) = dom (f1 (#) g1) by VALUED_1:def 5;
then A48: dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) = (dom f1) /\ (dom g1) by VALUED_1:def 4;
dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (abs (f1 (#) g1))) = dom (abs (f1 (#) g1)) by VALUED_1:def 5;
then A49: dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (abs (f1 (#) g1))) = dom (f1 (#) g1) by VALUED_1:def 11;
A50: (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1) is EDf /\ EDg -measurable by ;
for x being Element of X st x in dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) holds
|.(((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) . x).| <= (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) . x
proof
let x be Element of X; :: thesis: ( x in dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) implies |.(((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) . x).| <= (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) . x )
assume A51: x in dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) ; :: thesis: |.(((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) . x).| <= (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) . x
( (abs f1) . x >= 0 & (abs g1) . x >= 0 ) by MESFUNC6:51;
then A52: ((1 / (s1 to_power (1 / m))) * ((abs f1) . x)) * ((1 / (s2 to_power (1 / n))) * ((abs g1) . x)) <= ((((1 / (s1 to_power (1 / m))) * ((abs f1) . x)) to_power m) / m) + ((((1 / (s2 to_power (1 / n))) * ((abs g1) . x)) to_power n) / n) by ;
dom ((abs f1) (#) (abs g1)) = (dom (abs f1)) /\ (dom (abs g1)) by VALUED_1:def 4;
then A53: ((abs f1) (#) (abs g1)) . x = ((abs f1) . x) * ((abs g1) . x) by ;
A54: ((1 / (s1 to_power (1 / m))) * ((abs f1) . x)) * ((1 / (s2 to_power (1 / n))) * ((abs g1) . x)) = (((1 / (s1 to_power (1 / m))) * (1 / (s2 to_power (1 / n)))) * ((abs f1) . x)) * ((abs g1) . x)
.= ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * ((abs f1) . x)) * ((abs g1) . x) by XCMPLX_1:102
.= (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * (((abs f1) (#) (abs g1)) . x) by A53
.= (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * ((abs (f1 (#) g1)) . x) by RFUNCT_1:24
.= ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (abs (f1 (#) g1))) . x by
.= (abs ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1))) . x by ;
A55: ( (1 / (s1 to_power (1 / m))) * ((abs f1) . x) = ((1 / (s1 to_power (1 / m))) (#) (abs f1)) . x & (1 / (s2 to_power (1 / n))) * ((abs g1) . x) = ((1 / (s2 to_power (1 / n))) (#) (abs g1)) . x ) by VALUED_1:6;
( dom (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) = dom f1 & dom (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) = dom g1 ) by ;
then ( x in dom (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) & x in dom (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) ) by ;
then ( (((1 / (s1 to_power (1 / m))) (#) (abs f1)) . x) to_power m = (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) . x & (((1 / (s2 to_power (1 / n))) (#) (abs g1)) . x) to_power n = (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) . x ) by MESFUN6C:def 4;
then ( ((((1 / (s1 to_power (1 / m))) (#) (abs f1)) . x) to_power m) / m = ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) . x & ((((1 / (s2 to_power (1 / n))) (#) (abs g1)) . x) to_power n) / n = ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) . x ) by VALUED_1:6;
then ((((1 / (s1 to_power (1 / m))) * ((abs f1) . x)) to_power m) / m) + ((((1 / (s2 to_power (1 / n))) * ((abs g1) . x)) to_power n) / n) = (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) . x by ;
hence |.(((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) . x).| <= (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) . x by ; :: thesis: verum
end;
then A56: Integral (M,(abs ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)))) <= Integral (M,(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)))) by ;
consider E1 being Element of S such that
A57: ( E1 = (dom ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m))) /\ (dom ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) & Integral (M,(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)))) = (Integral (M,(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) | E1))) + (Integral (M,(((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) | E1))) ) by ;
( EDf = X /\ EDf & EDg = X /\ EDg ) by XBOOLE_1:28;
then A58: ( EDf = X \ Nf & EDg = X \ Ng ) by XBOOLE_1:48;
A59: EDf \ (EDf /\ EDg) = EDf \ EDg by XBOOLE_1:47
.= ((X \ Nf) \ X) \/ ((X \ Nf) /\ Ng) by
.= (X \ (Nf \/ X)) \/ ((X \ Nf) /\ Ng) by XBOOLE_1:41
.= (X \ X) \/ ((X \ Nf) /\ Ng) by XBOOLE_1:12
.= {} \/ ((X \ Nf) /\ Ng) by XBOOLE_1:37 ;
A60: EDg \ (EDf /\ EDg) = EDg \ EDf by XBOOLE_1:47
.= ((X \ Ng) \ X) \/ ((X \ Ng) /\ Nf) by
.= (X \ (Ng \/ X)) \/ ((X \ Ng) /\ Nf) by XBOOLE_1:41
.= (X \ X) \/ ((X \ Ng) /\ Nf) by XBOOLE_1:12
.= {} \/ ((X \ Ng) /\ Nf) by XBOOLE_1:37 ;
set NF = EDf /\ Ng;
set NG = EDg /\ Nf;
( Nf is measure_zero of M & Ng is measure_zero of M ) by ;
then ( EDf /\ Ng is measure_zero of M & EDg /\ Nf is measure_zero of M ) by ;
then A61: ( M . (EDf /\ Ng) = 0 & M . (EDg /\ Nf) = 0 ) by MEASURE1:def 7;
( EDf /\ EDg = EDf /\ (EDf /\ EDg) & EDf /\ EDg = EDg /\ (EDf /\ EDg) ) by ;
then A62: ( EDf /\ EDg = EDf \ (EDf /\ Ng) & EDf /\ EDg = EDg \ (EDg /\ Nf) ) by ;
R_EAL ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) is_integrable_on M by A45;
then ex E being Element of S st
( E = dom (R_EAL ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m))) & R_EAL ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) is E -measurable ) ;
then A63: (1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) is EDf -measurable by A42, A8, A4;
R_EAL ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) is_integrable_on M by A45;
then ex E being Element of S st
( E = dom (R_EAL ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) & R_EAL ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) is E -measurable ) ;
then A64: (1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) is EDg -measurable by A42, A8, A6;
(1 / (s1 to_power (1 / m))) to_power m = (s1 to_power (1 / m)) to_power (- m) by ;
then (1 / (s1 to_power (1 / m))) to_power m = s1 to_power ((1 / m) * (- m)) by ;
then (1 / (s1 to_power (1 / m))) to_power m = s1 to_power (- ((1 * (1 / m)) * m)) ;
then (1 / (s1 to_power (1 / m))) to_power m = s1 to_power (- 1) by XCMPLX_1:106;
then (1 / (s1 to_power (1 / m))) to_power m = (1 / s1) to_power 1 by ;
then A65: (1 / (s1 to_power (1 / m))) to_power m = 1 / s1 by POWER:25;
A66: ( (1 / s1) * s1 = 1 & (1 / s2) * s2 = 1 ) by ;
A67: (1 / (s2 to_power (1 / n))) to_power n = (s2 to_power (1 / n)) to_power (- n) by
.= s2 to_power ((1 / n) * (- n)) by
.= s2 to_power (- ((1 * (1 / n)) * n))
.= s2 to_power (- 1) by XCMPLX_1:106
.= (1 / s2) to_power 1 by
.= 1 / s2 by POWER:25 ;
A68: Integral (M,(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) | (EDf /\ EDg))) = Integral (M,((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m))) by
.= (1 / m) * (Integral (M,(((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m))) by
.= (1 / m) * (Integral (M,(((1 / (s1 to_power (1 / m))) to_power m) (#) ((abs f1) to_power m)))) by
.= (1 / m) * (((1 / (s1 to_power (1 / m))) to_power m) * (Integral (M,((abs f1) to_power m)))) by
.= 1 / m by ;
A69: Integral (M,(((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) | (EDf /\ EDg))) = Integral (M,((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) by
.= (1 / n) * (Integral (M,(((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) by
.= (1 / n) * (Integral (M,(((1 / (s2 to_power (1 / n))) to_power n) (#) ((abs g1) to_power n)))) by
.= (1 / n) * (((1 / (s2 to_power (1 / n))) to_power n) * (Integral (M,((abs g1) to_power n)))) by
.= 1 / n by ;
reconsider n1 = 1 / n, m1 = 1 / m as Real ;
A70: Integral (M,(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)))) = (Integral (M,(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) | (EDf /\ EDg)))) + (Integral (M,(((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) | (EDf /\ EDg)))) by A42, A4, A6, A8, A57
.= m1 + n1 by
.= jj by A1 ;
abs ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) = |.(1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))).| (#) (abs (f1 (#) g1)) by RFUNCT_1:25;
then abs ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) = (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (abs (f1 (#) g1)) by ;
then A71: Integral (M,(abs ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)))) = (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * (Integral (M,(abs (f1 (#) g1)))) by ;
reconsider c1 = Integral (M,(abs (f1 (#) g1))) as Element of REAL by ;
(1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * (Integral (M,(abs (f1 (#) g1)))) = (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * c1 ;
then (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * (Integral (M,(abs (f1 (#) g1)))) = (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * c1 ;
then ((s1 to_power (1 / m)) * (s2 to_power (1 / n))) * ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * c1) <= ((s1 to_power (1 / m)) * (s2 to_power (1 / n))) * 1 by ;
then A72: (((s1 to_power (1 / m)) * (s2 to_power (1 / n))) * (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n))))) * c1 <= (s1 to_power (1 / m)) * (s2 to_power (1 / n)) ;
((s1 to_power (1 / m)) * (s2 to_power (1 / n))) * (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) = 1 by ;
hence ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) ) by A3, A5, A72; :: thesis: verum
end;
end;