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

for n being Nat holds 0 <= ab . n

deffunc H_{1}( 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_{1}(n)
from SEQ_1:sch 1();

for n being Nat holds 0 <= ap . n

deffunc H_{2}( 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_{2}(n)
from SEQ_1:sch 1();

A16: for n being Nat holds (Partial_Sums ab) . n <= (x (#) y) . n

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

( 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

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

A9: bq . n = |.(b . n).| to_power q by A3;

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

end;A9: bq . n = |.(b . n).| to_power q by A3;

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

for n being Nat holds 0 <= ab . n

proof

then A11:
Partial_Sums ab is V48()
by SERIES_1:16;
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;ab . n = |.((a . n) * (b . n)).| by A3;

hence 0 <= ab . n by COMPLEX1:46; :: thesis: verum

deffunc H

consider y being Real_Sequence such that

A12: for n being Nat holds y . n = H

for n being Nat holds 0 <= ap . n

proof

then A14:
for n being Nat holds 0 <= (Partial_Sums ap) . n
by Lm2;
let n be Nat; :: thesis: 0 <= ap . n

A13: ap . n = |.(a . n).| to_power p by A3;

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

end;A13: ap . n = |.(a . n).| to_power p by A3;

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

deffunc H

consider x being Real_Sequence such that

A15: for n being Nat holds x . n = H

A16: for n being Nat holds (Partial_Sums ab) . n <= (x (#) y) . n

proof

A18:
1 / p > 0
by A1, XREAL_1:139;
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;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

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