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
A1: (1 / m) + (1 / n) = 1 and
A2: ( 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 )
A3: ( m > 1 & n > 1 ) by A1, Th1;
consider f1 being PartFunc of X,REAL such that
A4: ( 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 A2;
consider EDf being Element of S such that
A5: ( M . (EDf `) = 0 & dom f1 = EDf & f1 is EDf -measurable ) by A4;
consider g1 being PartFunc of X,REAL such that
A6: ( 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 A2;
consider EDg being Element of S such that
A7: ( M . (EDg `) = 0 & dom g1 = EDg & g1 is EDg -measurable ) by A6;
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));
A8: ( dom f1 = dom (abs f1) & dom g1 = dom (abs g1) ) by VALUED_1:def 11;
then A9: ( dom ((abs f1) to_power m) = dom f1 & dom ((abs g1) to_power n) = dom g1 ) by MESFUN6C:def 4;
then A10: 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:34;
( dom ((abs f1) to_power m) = Nf ` & dom ((abs g1) to_power n) = Ng ` ) by A5, A7, A8, MESFUN6C:def 4;
then ( (abs f1) to_power m in L1_Functions M & (abs g1) to_power n in L1_Functions M ) by A4, A5, A6, A7;
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 A11: 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 A12: 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;
A13: (EDf /\ EDg) ` = (EDf `) \/ (EDg `) by XBOOLE_1:54;
( Nf is measure_zero of M & Ng is measure_zero of M ) by A5, A7, MEASURE1:def 7;
then Nf \/ Ng is measure_zero of M by MEASURE1:37;
then A14: M . ((EDf /\ EDg) `) = 0 by A13, MEASURE1:def 7;
( f1 is EDf /\ EDg -measurable & g1 is EDf /\ EDg -measurable ) by A5, A7, MESFUNC6:16, XBOOLE_1:17;
then A15: f1 (#) g1 is EDf /\ EDg -measurable by A5, A7, MESFUN7C:31;
for x being Element of X st x in dom (f1 (#) g1) holds
|.((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 |.((f1 (#) g1) . x).| <= (((1 / m) (#) ((abs f1) to_power m)) + ((1 / n) (#) ((abs g1) to_power n))) . x )
assume A16: x in dom (f1 (#) g1) ; :: thesis: |.((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:24;
then (abs (f1 (#) g1)) . x = ((abs f1) . x) * ((abs g1) . x) by VALUED_1:5;
then A17: |.((f1 (#) g1) . x).| = ((abs f1) . x) * ((abs g1) . x) by VALUED_1:18;
A18: ( (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 A16, A10, 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 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 VALUED_1:6;
then |.((f1 (#) g1) . x).| <= (((1 / m) (#) ((abs f1) to_power m)) . x) + (((1 / n) (#) ((abs g1) to_power n)) . x) by A1, A3, A17, A18, HOLDER_1:5;
hence |.((f1 (#) g1) . x).| <= (((1 / m) (#) ((abs f1) to_power m)) + ((1 / n) (#) ((abs g1) to_power n))) . x by A16, A10, A12, VALUED_1:def 1; :: thesis: verum

end;

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