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)).| ) ) holds
for n being Nat holds (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) 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)).| ) ) holds
for n being Nat holds (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))
reconsider pp = 1 / p as Real ;
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)).| ) ) implies for n being Nat holds (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) )
assume 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)).| ) ; :: thesis: for n being Nat holds (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))
let n be Nat; :: thesis: (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))
set B = (Partial_Sums bq) . n;
1 / p < 1 by A1, XREAL_1:189;
then A4: 1 - 1 < 1 - pp by XREAL_1:15;
then A5: 0 < q by A2;
A6: for n being Nat holds 0 <= bq . n
proof
let n be Nat; :: thesis: 0 <= bq . n
A7: 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 A5, A7, POWER:def 2; :: thesis: verum
end;
case |.(b . n).| > 0 ; :: thesis: 0 <= bq . n
hence 0 <= bq . n by A7, POWER:34; :: thesis: verum
end;
end;
end;
hence 0 <= bq . n ; :: thesis: verum
end;
then A8: 0 <= (Partial_Sums bq) . n by Lm2;
set A = (Partial_Sums ap) . n;
A9: for n being Nat holds 0 <= ap . n
proof
let n be Nat; :: thesis: 0 <= ap . n
A10: 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, A10, POWER:def 2; :: thesis: verum
end;
case |.(a . n).| > 0 ; :: thesis: 0 <= ap . n
hence 0 <= ap . n by A10, POWER:34; :: thesis: verum
end;
end;
end;
hence 0 <= ap . n ; :: thesis: verum
end;
then A11: 0 <= (Partial_Sums ap) . n by Lm2;
set Bq = ((Partial_Sums bq) . n) to_power (1 / q);
set Ap = ((Partial_Sums ap) . n) to_power (1 / p);
A12: 1 / p > 0 by A1, XREAL_1:139;
now :: thesis: ( ( ((Partial_Sums ap) . n) * ((Partial_Sums bq) . n) = 0 & (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) ) or ( ((Partial_Sums ap) . n) * ((Partial_Sums bq) . n) <> 0 & (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) ) )
per cases ( ((Partial_Sums ap) . n) * ((Partial_Sums bq) . n) = 0 or ((Partial_Sums ap) . n) * ((Partial_Sums bq) . n) <> 0 ) ;
case A13: ((Partial_Sums ap) . n) * ((Partial_Sums bq) . n) = 0 ; :: thesis: (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))
A14: 0 <= ((Partial_Sums ap) . n) to_power (1 / p)
proof
now :: thesis: ( ( 0 < (Partial_Sums ap) . n & 0 <= ((Partial_Sums ap) . n) to_power (1 / p) ) or ( 0 = (Partial_Sums ap) . n & 0 <= ((Partial_Sums ap) . n) to_power (1 / p) ) )
per cases ( 0 < (Partial_Sums ap) . n or 0 = (Partial_Sums ap) . n ) by A9, Lm2;
case 0 < (Partial_Sums ap) . n ; :: thesis: 0 <= ((Partial_Sums ap) . n) to_power (1 / p)
hence 0 <= ((Partial_Sums ap) . n) to_power (1 / p) by POWER:34; :: thesis: verum
end;
case 0 = (Partial_Sums ap) . n ; :: thesis: 0 <= ((Partial_Sums ap) . n) to_power (1 / p)
hence 0 <= ((Partial_Sums ap) . n) to_power (1 / p) by A12, POWER:def 2; :: thesis: verum
end;
end;
end;
hence 0 <= ((Partial_Sums ap) . n) to_power (1 / p) ; :: thesis: verum
end;
0 <= ((Partial_Sums bq) . n) to_power (1 / q)
proof
now :: thesis: ( ( 0 < (Partial_Sums bq) . n & 0 <= ((Partial_Sums bq) . n) to_power (1 / q) ) or ( 0 = (Partial_Sums bq) . n & 0 <= ((Partial_Sums bq) . n) to_power (1 / q) ) )
per cases ( 0 < (Partial_Sums bq) . n or 0 = (Partial_Sums bq) . n ) by A6, Lm2;
case 0 < (Partial_Sums bq) . n ; :: thesis: 0 <= ((Partial_Sums bq) . n) to_power (1 / q)
hence 0 <= ((Partial_Sums bq) . n) to_power (1 / q) by POWER:34; :: thesis: verum
end;
case 0 = (Partial_Sums bq) . n ; :: thesis: 0 <= ((Partial_Sums bq) . n) to_power (1 / q)
hence 0 <= ((Partial_Sums bq) . n) to_power (1 / q) by A2, A4, POWER:def 2; :: thesis: verum
end;
end;
end;
hence 0 <= ((Partial_Sums bq) . n) to_power (1 / q) ; :: thesis: verum
end;
then A15: 0 <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) by A14;
now :: thesis: ( ( (Partial_Sums ap) . n = 0 & (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) ) or ( (Partial_Sums bq) . n = 0 & (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) ) )
per cases ( (Partial_Sums ap) . n = 0 or (Partial_Sums bq) . n = 0 ) by A13, XCMPLX_1:6;
case A16: (Partial_Sums ap) . n = 0 ; :: thesis: (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))
A17: for k being Nat st k <= n holds
a . k = 0
proof
let k be Nat; :: thesis: ( k <= n implies a . k = 0 )
assume k <= n ; :: thesis: a . k = 0
then ap . k = 0 by A9, A16, Lm3;
then A18: |.(a . k).| to_power p = 0 by A3;
|.(a . k).| = 0
proof
assume |.(a . k).| <> 0 ; :: thesis: contradiction
then |.(a . k).| > 0 by COMPLEX1:46;
hence contradiction by A18, POWER:34; :: thesis: verum
end;
hence a . k = 0 by ABSVALUE:2; :: thesis: verum
end;
for k being Nat st k <= n holds
ab . k = 0
proof
let k be Nat; :: thesis: ( k <= n implies ab . k = 0 )
assume A19: k <= n ; :: thesis: ab . k = 0
thus ab . k = |.((a . k) * (b . k)).| by A3
.= |.(0 * (b . k)).| by A17, A19
.= 0 by ABSVALUE:2 ; :: thesis: verum
end;
hence (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) by A15, Lm4; :: thesis: verum
end;
case A20: (Partial_Sums bq) . n = 0 ; :: thesis: (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))
A21: for k being Nat st k <= n holds
b . k = 0
proof
let k be Nat; :: thesis: ( k <= n implies b . k = 0 )
assume k <= n ; :: thesis: b . k = 0
then bq . k = 0 by A6, A20, Lm3;
then A22: |.(b . k).| to_power q = 0 by A3;
|.(b . k).| = 0
proof
assume |.(b . k).| <> 0 ; :: thesis: contradiction
then |.(b . k).| > 0 by COMPLEX1:46;
hence contradiction by A22, POWER:34; :: thesis: verum
end;
hence b . k = 0 by ABSVALUE:2; :: thesis: verum
end;
for k being Nat st k <= n holds
ab . k = 0
proof
let k be Nat; :: thesis: ( k <= n implies ab . k = 0 )
assume A23: k <= n ; :: thesis: ab . k = 0
thus ab . k = |.((a . k) * (b . k)).| by A3
.= |.((a . k) * 0).| by A21, A23
.= 0 by ABSVALUE:2 ; :: thesis: verum
end;
hence (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) by A15, Lm4; :: thesis: verum
end;
end;
end;
hence (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) ; :: thesis: verum
end;
case A24: ((Partial_Sums ap) . n) * ((Partial_Sums bq) . n) <> 0 ; :: thesis: (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))
deffunc H1( Nat) -> set = |.(b . $1).| / (((Partial_Sums bq) . n) to_power (1 / q));
consider y being Real_Sequence such that
A25: for n being Nat holds y . n = H1(n) from SEQ_1:sch 1();
A26: (Partial_Sums bq) . n <> 0 by A24;
then A27: ((Partial_Sums bq) . n) to_power (1 / q) > 0 by A8, POWER:34;
A28: for n being Nat holds 0 <= y . n
proof
let n be Nat; :: thesis: 0 <= y . n
0 <= |.(b . n).| by COMPLEX1:46;
then 0 <= |.(b . n).| / (((Partial_Sums bq) . n) to_power (1 / q)) by A27;
hence 0 <= y . n by A25; :: thesis: verum
end;
deffunc H2( Nat) -> set = |.(a . $1).| / (((Partial_Sums ap) . n) to_power (1 / p));
consider x being Real_Sequence such that
A29: for n being Nat holds x . n = H2(n) from SEQ_1:sch 1();
A30: for n being Nat holds ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab) . n = (x . n) * (y . n)
proof
let n be Nat; :: thesis: ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab) . n = (x . n) * (y . n)
( x . n = |.(a . n).| / (((Partial_Sums ap) . n) to_power (1 / p)) & y . n = |.(b . n).| / (((Partial_Sums bq) . n) to_power (1 / q)) ) by A29, A25;
hence (x . n) * (y . n) = (|.(a . n).| * |.(b . n).|) / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))) by XCMPLX_1:76
.= |.((a . n) * (b . n)).| / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))) by COMPLEX1:65
.= (ab . n) / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))) by A3
.= (1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) * (ab . n) by XCMPLX_1:99
.= ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab) . n by SEQ_1:9 ;
:: thesis: verum
end;
A31: (Partial_Sums ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab)) . n = ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) (Partial_Sums ab)) . n by SERIES_1:9
.= (1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) * ((Partial_Sums ab) . n) by SEQ_1:9 ;
A32: (Partial_Sums ap) . n <> 0 by A24;
then A33: ((Partial_Sums ap) . n) to_power (1 / p) > 0 by A11, POWER:34;
then A34: (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) > 0 by A27, XREAL_1:129;
A35: for n being Nat holds (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n = (((x . n) to_power p) / p) + (((y . n) to_power q) / q)
proof
let n be Nat; :: thesis: (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n = (((x . n) to_power p) / p) + (((y . n) to_power q) / q)
A36: (|.(a . n).| / (((Partial_Sums ap) . n) to_power (1 / p))) to_power p = (|.(a . n).| to_power p) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p)
proof
now :: thesis: ( ( |.(a . n).| = 0 & (|.(a . n).| / (((Partial_Sums ap) . n) to_power (1 / p))) to_power p = (|.(a . n).| to_power p) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p) ) or ( |.(a . n).| <> 0 & (|.(a . n).| / (((Partial_Sums ap) . n) to_power (1 / p))) to_power p = (|.(a . n).| to_power p) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p) ) )
per cases ( |.(a . n).| = 0 or |.(a . n).| <> 0 ) ;
case A37: |.(a . n).| = 0 ; :: thesis: (|.(a . n).| / (((Partial_Sums ap) . n) to_power (1 / p))) to_power p = (|.(a . n).| to_power p) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p)
hence (|.(a . n).| / (((Partial_Sums ap) . n) to_power (1 / p))) to_power p = 0 / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p) by A1, POWER:def 2
.= (|.(a . n).| to_power p) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p) by A1, A37, POWER:def 2 ;
:: thesis: verum
end;
case |.(a . n).| <> 0 ; :: thesis: (|.(a . n).| / (((Partial_Sums ap) . n) to_power (1 / p))) to_power p = (|.(a . n).| to_power p) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p)
then |.(a . n).| > 0 by COMPLEX1:46;
hence (|.(a . n).| / (((Partial_Sums ap) . n) to_power (1 / p))) to_power p = (|.(a . n).| to_power p) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p) by A33, POWER:31; :: thesis: verum
end;
end;
end;
hence (|.(a . n).| / (((Partial_Sums ap) . n) to_power (1 / p))) to_power p = (|.(a . n).| to_power p) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p) ; :: thesis: verum
end;
A38: (|.(b . n).| / (((Partial_Sums bq) . n) to_power (1 / q))) to_power q = (|.(b . n).| to_power q) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q)
proof
now :: thesis: ( ( |.(b . n).| = 0 & (|.(b . n).| / (((Partial_Sums bq) . n) to_power (1 / q))) to_power q = (|.(b . n).| to_power q) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q) ) or ( |.(b . n).| <> 0 & (|.(b . n).| / (((Partial_Sums bq) . n) to_power (1 / q))) to_power q = (|.(b . n).| to_power q) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q) ) )
per cases ( |.(b . n).| = 0 or |.(b . n).| <> 0 ) ;
case A39: |.(b . n).| = 0 ; :: thesis: (|.(b . n).| / (((Partial_Sums bq) . n) to_power (1 / q))) to_power q = (|.(b . n).| to_power q) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q)
hence (|.(b . n).| / (((Partial_Sums bq) . n) to_power (1 / q))) to_power q = 0 / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q) by A5, POWER:def 2
.= (|.(b . n).| to_power q) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q) by A5, A39, POWER:def 2 ;
:: thesis: verum
end;
case |.(b . n).| <> 0 ; :: thesis: (|.(b . n).| / (((Partial_Sums bq) . n) to_power (1 / q))) to_power q = (|.(b . n).| to_power q) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q)
then |.(b . n).| > 0 by COMPLEX1:46;
hence (|.(b . n).| / (((Partial_Sums bq) . n) to_power (1 / q))) to_power q = (|.(b . n).| to_power q) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q) by A27, POWER:31; :: thesis: verum
end;
end;
end;
hence (|.(b . n).| / (((Partial_Sums bq) . n) to_power (1 / q))) to_power q = (|.(b . n).| to_power q) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q) ; :: thesis: verum
end;
y . n = |.(b . n).| / (((Partial_Sums bq) . n) to_power (1 / q)) by A25;
then A40: ((y . n) to_power q) / q = ((bq . n) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q)) / q by A3, A38
.= ((bq . n) / (((Partial_Sums bq) . n) to_power ((1 / q) * q))) / q by A8, A26, POWER:33
.= ((bq . n) / (((Partial_Sums bq) . n) to_power 1)) / q by A5, XCMPLX_1:87
.= ((bq . n) / ((Partial_Sums bq) . n)) / q by POWER:25
.= (1 / q) * ((bq . n) / ((Partial_Sums bq) . n)) by XCMPLX_1:99
.= (1 / q) * ((1 / ((Partial_Sums bq) . n)) * (bq . n)) by XCMPLX_1:99
.= (1 / q) * (((1 / ((Partial_Sums bq) . n)) (#) bq) . n) by SEQ_1:9
.= ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq)) . n by SEQ_1:9 ;
x . n = |.(a . n).| / (((Partial_Sums ap) . n) to_power (1 / p)) by A29;
then ((x . n) to_power p) / p = ((ap . n) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p)) / p by A3, A36
.= ((ap . n) / (((Partial_Sums ap) . n) to_power ((1 / p) * p))) / p by A11, A32, POWER:33
.= ((ap . n) / (((Partial_Sums ap) . n) to_power 1)) / p by A1, XCMPLX_1:87
.= ((ap . n) / ((Partial_Sums ap) . n)) / p by POWER:25
.= (1 / p) * ((ap . n) / ((Partial_Sums ap) . n)) by XCMPLX_1:99
.= (1 / p) * ((1 / ((Partial_Sums ap) . n)) * (ap . n)) by XCMPLX_1:99
.= (1 / p) * (((1 / ((Partial_Sums ap) . n)) (#) ap) . n) by SEQ_1:9
.= ((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) . n by SEQ_1:9 ;
hence (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) by A40, SEQ_1:7; :: thesis: verum
end;
A41: for n being Nat holds 0 <= x . n
proof
let n be Nat; :: thesis: 0 <= x . n
0 <= |.(a . n).| by COMPLEX1:46;
then 0 <= |.(a . n).| / (((Partial_Sums ap) . n) to_power (1 / p)) by A33;
hence 0 <= x . n by A29; :: thesis: verum
end;
A42: for n being Nat holds
( (x . n) * (y . n) <= (((x . n) to_power p) / p) + (((y . n) to_power q) / q) & ( (x . n) * (y . n) = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) implies (x . n) to_power p = (y . n) to_power q ) & ( (x . n) to_power p = (y . n) to_power q implies (x . n) * (y . n) = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) ) )
proof
let n be Nat; :: thesis: ( (x . n) * (y . n) <= (((x . n) to_power p) / p) + (((y . n) to_power q) / q) & ( (x . n) * (y . n) = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) implies (x . n) to_power p = (y . n) to_power q ) & ( (x . n) to_power p = (y . n) to_power q implies (x . n) * (y . n) = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) ) )
( 0 <= x . n & 0 <= y . n ) by A41, A28;
hence ( (x . n) * (y . n) <= (((x . n) to_power p) / p) + (((y . n) to_power q) / q) & ( (x . n) * (y . n) = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) implies (x . n) to_power p = (y . n) to_power q ) & ( (x . n) to_power p = (y . n) to_power q implies (x . n) * (y . n) = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) ) ) by A1, A2, Th5; :: thesis: verum
end;
for n being Nat holds ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab) . n <= (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n
proof
let n be Nat; :: thesis: ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab) . n <= (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n
( (x . n) * (y . n) <= (((x . n) to_power p) / p) + (((y . n) to_power q) / q) & (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) ) by A42, A35;
hence ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab) . n <= (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n by A30; :: thesis: verum
end;
then A43: (Partial_Sums ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab)) . n <= (Partial_Sums (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq)))) . n by SERIES_1:14;
(Partial_Sums (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq)))) . n = ((Partial_Sums ((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap))) + (Partial_Sums ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq)))) . n by SERIES_1:5
.= ((Partial_Sums ((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap))) . n) + ((Partial_Sums ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n) by SEQ_1:7
.= (((1 / p) (#) (Partial_Sums ((1 / ((Partial_Sums ap) . n)) (#) ap))) . n) + ((Partial_Sums ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n) by SERIES_1:9
.= ((1 / p) * ((Partial_Sums ((1 / ((Partial_Sums ap) . n)) (#) ap)) . n)) + ((Partial_Sums ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n) by SEQ_1:9
.= ((1 / p) * (((1 / ((Partial_Sums ap) . n)) (#) (Partial_Sums ap)) . n)) + ((Partial_Sums ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n) by SERIES_1:9
.= ((1 / p) * ((1 / ((Partial_Sums ap) . n)) * ((Partial_Sums ap) . n))) + ((Partial_Sums ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n) by SEQ_1:9
.= ((1 / p) * ((1 / ((Partial_Sums ap) . n)) * ((Partial_Sums ap) . n))) + (((1 / q) (#) (Partial_Sums ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n) by SERIES_1:9
.= ((1 / p) * ((1 / ((Partial_Sums ap) . n)) * ((Partial_Sums ap) . n))) + ((1 / q) * ((Partial_Sums ((1 / ((Partial_Sums bq) . n)) (#) bq)) . n)) by SEQ_1:9
.= ((1 / p) * ((1 / ((Partial_Sums ap) . n)) * ((Partial_Sums ap) . n))) + ((1 / q) * (((1 / ((Partial_Sums bq) . n)) (#) (Partial_Sums bq)) . n)) by SERIES_1:9
.= ((1 / p) * ((1 / ((Partial_Sums ap) . n)) * ((Partial_Sums ap) . n))) + ((1 / q) * ((1 / ((Partial_Sums bq) . n)) * ((Partial_Sums bq) . n))) by SEQ_1:9
.= ((1 / p) * 1) + ((1 / q) * ((1 / ((Partial_Sums bq) . n)) * ((Partial_Sums bq) . n))) by A32, XCMPLX_1:87
.= ((1 / p) * 1) + ((1 / q) * 1) by A26, XCMPLX_1:87
.= 1 by A2 ;
then ((Partial_Sums ab) . n) / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))) <= 1 by A43, A31, XCMPLX_1:99;
hence (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) by A34, XREAL_1:187; :: thesis: verum
end;
end;
end;
hence (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) ; :: thesis: verum