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
( f (#) g in L1_Functions M & f (#) g is_integrable_on 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,n holds
( f (#) g in L1_Functions M & f (#) g is_integrable_on 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,n holds
( f (#) g in L1_Functions M & f (#) g is_integrable_on 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,n holds
( f (#) g in L1_Functions M & f (#) g is_integrable_on M )
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 ( f (#) g in L1_Functions M & f (#) g is_integrable_on M ) )
assume that
AS1: (1 / m) + (1 / n) = 1 and
AS2: ( f in Lp_Functions M,m & g in Lp_Functions M,n ) ; :: thesis: ( f (#) g in L1_Functions M & f (#) g is_integrable_on M )
A2: ( m > 1 & n > 1 ) by AS1, Lm300;
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_measurable_on NDf & (abs f1) to_power m is_integrable_on M ) ) by AS2;
consider EDf being Element of S such that
A4: ( M . (EDf ` ) = 0 & dom f1 = EDf & f1 is_measurable_on EDf ) 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_measurable_on NDg & (abs g1) to_power n is_integrable_on M ) ) by AS2;
consider EDg being Element of S such that
A6: ( M . (EDg ` ) = 0 & dom g1 = EDg & g1 is_measurable_on EDg ) by A5;
set u = (abs f1) to_power m;
set v = (abs g1) to_power n;
set w = f1 (#) g1;
set z = ((1 / m) (#) ((abs f1) to_power m)) + ((1 / n) (#) ((abs g1) to_power n));
A7: ( dom f1 = dom (abs f1) & dom g1 = dom (abs g1) ) by VALUED_1:def 11;
then A8: ( dom ((abs f1) to_power m) = dom f1 & dom ((abs g1) to_power n) = dom g1 ) by MESFUN6C:def 6;
then A9: dom (f1 (#) g1) = (dom ((abs f1) to_power m)) /\ (dom ((abs g1) to_power n)) by VALUED_1:def 4;
set Nf = EDf ` ;
set Ng = EDg ` ;
set E = EDf /\ EDg;
reconsider Nf = EDf ` , Ng = EDg ` as Element of S by MEASURE1:66;
( dom ((abs f1) to_power m) = Nf ` & dom ((abs g1) to_power n) = Ng ` ) by A4, A6, A7, MESFUN6C:def 6;
then ( (abs f1) to_power m in L1_Functions M & (abs g1) to_power n in L1_Functions M ) by A3, A4, A5, A6;
then ( (1 / m) (#) ((abs f1) to_power m) in L1_Functions M & (1 / n) (#) ((abs g1) to_power n) in L1_Functions M ) by LPSPACE1:24;
then ((1 / m) (#) ((abs f1) to_power m)) + ((1 / n) (#) ((abs g1) to_power n)) in L1_Functions M by LPSPACE1:23;
then A10: ex h being PartFunc of X,REAL st
( ((1 / m) (#) ((abs f1) to_power m)) + ((1 / n) (#) ((abs g1) to_power n)) = h & ex ND being Element of S st
( M . ND = 0 & dom h = ND ` & h is_integrable_on M ) ) ;
( dom ((1 / m) (#) ((abs f1) to_power m)) = dom ((abs f1) to_power m) & dom ((1 / n) (#) ((abs g1) to_power n)) = dom ((abs g1) to_power n) ) by VALUED_1:def 5;
then A11: dom (((1 / m) (#) ((abs f1) to_power m)) + ((1 / n) (#) ((abs g1) to_power n))) = (dom ((abs f1) to_power m)) /\ (dom ((abs g1) to_power n)) by VALUED_1:def 1;
A12: (EDf /\ EDg) ` = (EDf ` ) \/ (EDg ` ) by XBOOLE_1:54;
( Nf is measure_zero of M & Ng is measure_zero of M ) by A4, A6, MEASURE1:def 13;
then Nf \/ Ng is measure_zero of M by MEASURE1:70;
then A13: M . ((EDf /\ EDg) ` ) = 0 by A12, MEASURE1:def 13;
( f1 is_measurable_on EDf /\ EDg & g1 is_measurable_on EDf /\ EDg ) by A4, A6, MESFUNC6:16, XBOOLE_1:17;
then A14: f1 (#) g1 is_measurable_on EDf /\ EDg by A4, A6, MESFUN7C:31;
for x being Element of X st x in dom (f1 (#) g1) holds
abs ((f1 (#) g1) . x) <= (((1 / m) (#) ((abs f1) to_power m)) + ((1 / n) (#) ((abs g1) to_power n))) . x

proof

let x be Element of X; :: thesis: ( x in dom (f1 (#) g1) implies abs ((f1 (#) g1) . x) <= (((1 / m) (#) ((abs f1) to_power m)) + ((1 / n) (#) ((abs g1) to_power n))) . x )
assume A15: x in dom (f1 (#) g1) ; :: thesis: abs ((f1 (#) g1) . x) <= (((1 / m) (#) ((abs f1) to_power m)) + ((1 / n) (#) ((abs g1) to_power n))) . x
abs (f1 (#) g1) = (abs f1) (#) (abs g1) by RFUNCT_1:36;
then (abs (f1 (#) g1)) . x = ((abs f1) . x) * ((abs g1) . x) by VALUED_1:5;
then A16: abs ((f1 (#) g1) . x) = ((abs f1) . x) * ((abs g1) . x) by VALUED_1:18;
A17: ( (abs f1) . x >= 0 & (abs g1) . x >= 0 ) by MESFUNC6:51;
( x in dom ((abs f1) to_power m) & x in dom ((abs g1) to_power n) ) by A15, A9, XBOOLE_0:def 4;
then ( (((abs f1) . x) to_power m) / m = (1 / m) * (((abs f1) to_power m) . x) & (((abs g1) . x) to_power n) / n = (1 / n) * (((abs g1) to_power n) . x) ) by MESFUN6C:def 6;
then ( (((abs f1) . x) to_power m) / m = ((1 / m) (#) ((abs f1) to_power m)) . x & (((abs g1) . x) to_power n) / n = ((1 / n) (#) ((abs g1) to_power n)) . x ) by VALUED_1:6;
then abs ((f1 (#) g1) . x) <= (((1 / m) (#) ((abs f1) to_power m)) . x) + (((1 / n) (#) ((abs g1) to_power n)) . x) by AS1, A2, A16, A17, HOLDER_1:5;
hence abs ((f1 (#) g1) . x) <= (((1 / m) (#) ((abs f1) to_power m)) + ((1 / n) (#) ((abs g1) to_power n))) . x by A15, A9, A11, VALUED_1:def 1; :: thesis: verum

end;

then A19: f1 (#) g1 is_integrable_on M by A4, A6, A8, A9, A10, A14, A11, MESFUNC6:96;
set ND = (EDf /\ EDg) ` ;
reconsider ND = (EDf /\ EDg) ` as Element of S by MEASURE1:66;
dom (f1 (#) g1) = ND ` by A4, A6, VALUED_1:def 4;
hence ( f (#) g in L1_Functions M & f (#) g is_integrable_on M ) by A3, A5, A13, A19; :: thesis: verum