let p, q be Real; :: thesis: ( 1 < p & (1 / p) + (1 / q) = 1 implies for a, b, ap, bq, ab being Real_Sequence st ( for n being Nat holds
( ap . n = |.(a . n).| to_power p & bq . n = |.(b . n).| to_power q & ab . n = |.((a . n) * (b . n)).| ) ) & ap is summable & bq is summable holds
( ab is summable & Sum ab <= ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) ) )
assume that
A1: 1 < p and
A2: (1 / p) + (1 / q) = 1 ; :: thesis: for a, b, ap, bq, ab being Real_Sequence st ( for n being Nat holds
( ap . n = |.(a . n).| to_power p & bq . n = |.(b . n).| to_power q & ab . n = |.((a . n) * (b . n)).| ) ) & ap is summable & bq is summable holds
( ab is summable & Sum ab <= ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) )
let a, b, ap, bq, ab be Real_Sequence; :: thesis: ( ( for n being Nat holds
( ap . n = |.(a . n).| to_power p & bq . n = |.(b . n).| to_power q & ab . n = |.((a . n) * (b . n)).| ) ) & ap is summable & bq is summable implies ( ab is summable & Sum ab <= ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) ) )
assume that
A3: for n being Nat holds
( ap . n = |.(a . n).| to_power p & bq . n = |.(b . n).| to_power q & ab . n = |.((a . n) * (b . n)).| ) and
A4: ap is summable and
A5: bq is summable ; :: thesis: ( ab is summable & Sum ab <= ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) )
A6: Partial_Sums ap is convergent by A4, SERIES_1:def 2;
reconsider pp = 1 / p as Real ;
1 / p < 1 by A1, XREAL_1:189;
then A7: 1 - 1 < 1 - pp by XREAL_1:15;
then A8: 0 < q by A2;
for n being Nat holds 0 <= bq . n

proof

let n be Nat; :: thesis: 0 <= bq . n
A9: bq . n = |.(b . n).| to_power q by A3;

now :: thesis: ( ( |.(b . n).| = 0 & 0 <= bq . n ) or ( |.(b . n).| > 0 & 0 <= bq . n ) )

per cases ( |.(b . n).| = 0 or |.(b . n).| > 0 ) by COMPLEX1:46;

case |.(b . n).| = 0 ; :: thesis: 0 <= bq . n

hence 0 <= bq . n by A8, A9, POWER:def 2; :: thesis: verum

end;

case |.(b . n).| > 0 ; :: thesis: 0 <= bq . n

hence 0 <= bq . n by A9, POWER:34; :: thesis: verum

end;

end;

end;

hence 0 <= bq . n ; :: thesis: verum

end;

then A10: for n being Nat holds 0 <= (Partial_Sums bq) . n by Lm2;
for n being Nat holds 0 <= ab . n

proof

let n be Nat; :: thesis: 0 <= ab . n
ab . n = |.((a . n) * (b . n)).| by A3;
hence 0 <= ab . n by COMPLEX1:46; :: thesis: verum

end;

then A11: Partial_Sums ab is non-decreasing by SERIES_1:16;
deffunc H₁( Nat) -> object = ((Partial_Sums bq) . $1) to_power (1 / q);
consider y being Real_Sequence such that
A12: for n being Nat holds y . n = H₁(n) from SEQ_1:sch 1();
for n being Nat holds 0 <= ap . n

proof

let n be Nat; :: thesis: 0 <= ap . n
A13: ap . n = |.(a . n).| to_power p by A3;

now :: thesis: ( ( |.(a . n).| = 0 & 0 <= ap . n ) or ( |.(a . n).| > 0 & 0 <= ap . n ) )

per cases ( |.(a . n).| = 0 or |.(a . n).| > 0 ) by COMPLEX1:46;

case |.(a . n).| = 0 ; :: thesis: 0 <= ap . n

hence 0 <= ap . n by A1, A13, POWER:def 2; :: thesis: verum

end;

case |.(a . n).| > 0 ; :: thesis: 0 <= ap . n

hence 0 <= ap . n by A13, POWER:34; :: thesis: verum

end;

end;

end;

hence 0 <= ap . n ; :: thesis: verum

end;

then A14: for n being Nat holds 0 <= (Partial_Sums ap) . n by Lm2;
deffunc H₂( Nat) -> object = ((Partial_Sums ap) . $1) to_power (1 / p);
consider x being Real_Sequence such that
A15: for n being Nat holds x . n = H₂(n) from SEQ_1:sch 1();
A16: for n being Nat holds (Partial_Sums ab) . n <= (x (#) y) . n

proof

let n be Nat; :: thesis: (Partial_Sums ab) . n <= (x (#) y) . n
A17: y . n = ((Partial_Sums bq) . n) to_power (1 / q) by A12;
( (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) & x . n = ((Partial_Sums ap) . n) to_power (1 / p) ) by A1, A2, A3, A15, Th6;
hence (Partial_Sums ab) . n <= (x (#) y) . n by A17, SEQ_1:8; :: thesis: verum

end;

A18: 1 / p > 0 by A1, XREAL_1:139;
then A19: x is convergent by A15, A6, A14, Th10;
A20: Partial_Sums bq is convergent by A5, SERIES_1:def 2;
then A21: y is convergent by A2, A7, A12, A10, Th10;
then x (#) y is convergent by A19;
then A22: ( Partial_Sums ab is convergent & lim (Partial_Sums ab) <= lim (x (#) y) ) by A16, A11, Th8;
Sum ap = lim (Partial_Sums ap) by SERIES_1:def 3;
then A23: lim x = (Sum ap) to_power (1 / p) by A18, A15, A6, A14, Th10;
Sum bq = lim (Partial_Sums bq) by SERIES_1:def 3;
then lim y = (Sum bq) to_power (1 / q) by A2, A7, A12, A20, A10, Th10;
then lim (x (#) y) = ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) by A19, A23, A21, SEQ_2:15;
hence ( ab is summable & Sum ab <= ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) ) by A22, SERIES_1:def 2, SERIES_1:def 3; :: thesis: verum