let p be Real; :: thesis: ( 1 < p implies for a, b, ap, bp, ab being Real_Sequence st ( for n being Element of NAT holds
( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((a . n) + (b . n))) to_power p ) ) holds
for n being Element of NAT holds ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) )
assume A1: 1 < p ; :: thesis: for a, b, ap, bp, ab being Real_Sequence st ( for n being Element of NAT holds
( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((a . n) + (b . n))) to_power p ) ) holds
for n being Element of NAT holds ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))
A2: 1 / p > 0 by A1, XREAL_1:141;
let a, b, ap, bp, ab be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds
( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((a . n) + (b . n))) to_power p ) ) implies for n being Element of NAT holds ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) )
assume A3: for n being Element of NAT holds
( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((a . n) + (b . n))) to_power p ) ; :: thesis: for n being Element of NAT holds ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))
A4: for n being Element of NAT holds 0 <= ap . n
proof
let n be Element of NAT ; :: thesis: 0 <= ap . n
A5: ap . n = (abs (a . n)) to_power p by A3;
now
per cases ( abs (a . n) = 0 or abs (a . n) > 0 ) by COMPLEX1:132;
case abs (a . n) = 0 ; :: thesis: 0 <= ap . n
hence 0 <= ap . n by A1, A5, POWER:def 2; :: thesis: verum
end;
case abs (a . n) > 0 ; :: thesis: 0 <= ap . n
hence 0 <= ap . n by A5, POWER:39; :: thesis: verum
end;
end;
end;
hence 0 <= ap . n ; :: thesis: verum
end;
A6: for n being Element of NAT holds 0 <= bp . n
proof
let n be Element of NAT ; :: thesis: 0 <= bp . n
A7: bp . n = (abs (b . n)) to_power p by A3;
now
per cases ( abs (b . n) = 0 or abs (b . n) > 0 ) by COMPLEX1:132;
case abs (b . n) = 0 ; :: thesis: 0 <= bp . n
hence 0 <= bp . n by A1, A7, POWER:def 2; :: thesis: verum
end;
case abs (b . n) > 0 ; :: thesis: 0 <= bp . n
hence 0 <= bp . n by A7, POWER:39; :: thesis: verum
end;
end;
end;
hence 0 <= bp . n ; :: thesis: verum
end;
deffunc H1( Element of NAT ) -> Element of REAL = (abs ((a . $1) + (b . $1))) to_power (p - 1);
consider x being Real_Sequence such that
A8: for n being Element of NAT holds x . n = H1(n) from SEQ_1:sch 1();
 A9: 1 - 1 < p - 1 by A1, XREAL_1:16;
A10: for n being Element of NAT holds 0 <= x . n
proof
let n be Element of NAT ; :: thesis: 0 <= x . n
A11: x . n = (abs ((a . n) + (b . n))) to_power (p - 1) by A8;
now
per cases ( abs ((a . n) + (b . n)) = 0 or abs ((a . n) + (b . n)) > 0 ) by COMPLEX1:132;
case abs ((a . n) + (b . n)) = 0 ; :: thesis: 0 <= x . n
hence 0 <= x . n by A9, A11, POWER:def 2; :: thesis: verum
end;
case abs ((a . n) + (b . n)) > 0 ; :: thesis: 0 <= x . n
hence 0 <= x . n by A11, POWER:39; :: thesis: verum
end;
end;
end;
hence 0 <= x . n ; :: thesis: verum
end;
A12: for n being Element of NAT holds (x (#) (abs b)) . n = abs ((b . n) * (x . n))
proof
let n be Element of NAT ; :: thesis: (x (#) (abs b)) . n = abs ((b . n) * (x . n))
0 <= x . n by A10;
then A13: abs (x . n) = x . n by ABSVALUE:def 1;
thus (x (#) (abs b)) . n = (x . n) * ((abs b) . n) by SEQ_1:12
.= (x . n) * (abs (b . n)) by SEQ_1:16
.= abs ((b . n) * (x . n)) by A13, COMPLEX1:151 ; :: thesis: verum
end;
reconsider pp = 1 / p as Real ;
reconsider qq = 1 - pp as Real ;
reconsider q = 1 / qq as Real ;
A14: qq = 1 / q by XCMPLX_1:56;
then A15: (1 / p) + (1 / q) = 1 ;
1 / p < 1 by A1, XREAL_1:191;
then A16: 1 - 1 < 1 - pp by XREAL_1:17;
then A17: q <> 0 by A14;
then (((1 * q) + (1 * p)) / (p * q)) * (p * q) = 1 * (p * q) by A1, A15, XCMPLX_1:117;
then A18: q + p = p * q by A1, A17, XCMPLX_1:6, XCMPLX_1:88;
A19: for n being Element of NAT holds ab . n = (x . n) * (abs ((a . n) + (b . n)))
proof
let n be Element of NAT ; :: thesis: ab . n = (x . n) * (abs ((a . n) + (b . n)))
now
per cases ( abs ((a . n) + (b . n)) = 0 or abs ((a . n) + (b . n)) <> 0 ) ;
case A20: abs ((a . n) + (b . n)) = 0 ; :: thesis: ab . n = (x . n) * (abs ((a . n) + (b . n)))
thus ab . n = (abs ((a . n) + (b . n))) to_power p by A3
.= (x . n) * (abs ((a . n) + (b . n))) by A1, A20, POWER:def 2 ; :: thesis: verum
end;
case A21: abs ((a . n) + (b . n)) <> 0 ; :: thesis: ab . n = (x . n) * (abs ((a . n) + (b . n)))
A22: 0 <= abs ((a . n) + (b . n)) by COMPLEX1:132;
thus ab . n = (abs ((a . n) + (b . n))) to_power ((p - 1) + 1) by A3
.= ((abs ((a . n) + (b . n))) to_power (p - 1)) * ((abs ((a . n) + (b . n))) to_power 1) by A21, A22, POWER:32
.= ((abs ((a . n) + (b . n))) to_power (p - 1)) * (abs ((a . n) + (b . n))) by POWER:30
.= (x . n) * (abs ((a . n) + (b . n))) by A8 ; :: thesis: verum
end;
end;
end;
hence ab . n = (x . n) * (abs ((a . n) + (b . n))) ; :: thesis: verum
end;
A23: for n being Element of NAT holds ab . n <= ((x (#) (abs a)) + (x (#) (abs b))) . n
proof
let n be Element of NAT ; :: thesis: ab . n <= ((x (#) (abs a)) + (x (#) (abs b))) . n
A24: (x . n) * ((abs (a . n)) + (abs (b . n))) = ((x . n) * (abs (a . n))) + ((x . n) * (abs (b . n)))
.= ((x . n) * ((abs a) . n)) + ((x . n) * (abs (b . n))) by SEQ_1:16
.= ((x . n) * ((abs a) . n)) + ((x . n) * ((abs b) . n)) by SEQ_1:16
.= ((x (#) (abs a)) . n) + ((x . n) * ((abs b) . n)) by SEQ_1:12
.= ((x (#) (abs a)) . n) + ((x (#) (abs b)) . n) by SEQ_1:12
.= ((x (#) (abs a)) + (x (#) (abs b))) . n by SEQ_1:11 ;
( 0 <= x . n & ab . n = (x . n) * (abs ((a . n) + (b . n))) ) by A10, A19;
hence ab . n <= ((x (#) (abs a)) + (x (#) (abs b))) . n by A24, COMPLEX1:142, XREAL_1:66; :: thesis: verum
end;
A25: 0 < q by A16, A14;
A26: for n being Element of NAT holds (abs (x . n)) to_power q = ab . n
proof
let n be Element of NAT ; :: thesis: (abs (x . n)) to_power q = ab . n
0 <= x . n by A10;
then abs (x . n) = x . n by ABSVALUE:def 1;
then A27: (abs (x . n)) to_power q = ((abs ((a . n) + (b . n))) to_power (p - 1)) to_power q by A8;
now
per cases ( abs ((a . n) + (b . n)) = 0 or abs ((a . n) + (b . n)) <> 0 ) ;
case A28: abs ((a . n) + (b . n)) = 0 ; :: thesis: (abs (x . n)) to_power q = ab . n
then A29: ab . n = 0 to_power p by A3
.= 0 by A1, POWER:def 2 ;
(abs (x . n)) to_power q = 0 to_power q by A9, A27, A28, POWER:def 2
.= 0 by A25, POWER:def 2 ;
hence (abs (x . n)) to_power q = ab . n by A29; :: thesis: verum
end;
case abs ((a . n) + (b . n)) <> 0 ; :: thesis: (abs (x . n)) to_power q = ab . n
then 0 < abs ((a . n) + (b . n)) by COMPLEX1:132;
hence (abs (x . n)) to_power q = (abs ((a . n) + (b . n))) to_power ((p - 1) * q) by A27, POWER:38
.= ab . n by A3, A18 ;
:: thesis: verum
end;
end;
end;
hence (abs (x . n)) to_power q = ab . n ; :: thesis: verum
end;
A30: for n being Element of NAT holds (x (#) (abs a)) . n = abs ((a . n) * (x . n))
proof
let n be Element of NAT ; :: thesis: (x (#) (abs a)) . n = abs ((a . n) * (x . n))
0 <= x . n by A10;
then A31: abs (x . n) = x . n by ABSVALUE:def 1;
thus (x (#) (abs a)) . n = (x . n) * ((abs a) . n) by SEQ_1:12
.= (x . n) * (abs (a . n)) by SEQ_1:16
.= abs ((a . n) * (x . n)) by A31, COMPLEX1:151 ; :: thesis: verum
end;
A32: for n being Element of NAT holds (Partial_Sums ab) . n <= ((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * (((Partial_Sums ab) . n) to_power (1 / q))
proof
let n be Element of NAT ; :: thesis: (Partial_Sums ab) . n <= ((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * (((Partial_Sums ab) . n) to_power (1 / q))
A33: (Partial_Sums ((x (#) (abs a)) + (x (#) (abs b)))) . n = ((Partial_Sums (x (#) (abs a))) + (Partial_Sums (x (#) (abs b)))) . n by SERIES_1:8
.= ((Partial_Sums (x (#) (abs a))) . n) + ((Partial_Sums (x (#) (abs b))) . n) by SEQ_1:11 ;
( (Partial_Sums (x (#) (abs a))) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums ab) . n) to_power (1 / q)) & (Partial_Sums (x (#) (abs b))) . n <= (((Partial_Sums bp) . n) to_power (1 / p)) * (((Partial_Sums ab) . n) to_power (1 / q)) ) by A1, A3, A15, A30, A12, A26, Th6;
then A34: ((Partial_Sums (x (#) (abs a))) . n) + ((Partial_Sums (x (#) (abs b))) . n) <= ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums ab) . n) to_power (1 / q))) + ((((Partial_Sums bp) . n) to_power (1 / p)) * (((Partial_Sums ab) . n) to_power (1 / q))) by XREAL_1:9;
(Partial_Sums ab) . n <= (Partial_Sums ((x (#) (abs a)) + (x (#) (abs b)))) . n by A23, SERIES_1:17;
hence (Partial_Sums ab) . n <= ((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * (((Partial_Sums ab) . n) to_power (1 / q)) by A33, A34, XXREAL_0:2; :: thesis: verum
end;
A35: for n being Element of NAT holds 0 <= ab . n
proof
let n be Element of NAT ; :: thesis: 0 <= ab . n
0 <= abs ((a . n) + (b . n)) by COMPLEX1:132;
then A36: 0 to_power p <= (abs ((a . n) + (b . n))) to_power p by A1, Th3;
ab . n = (abs ((a . n) + (b . n))) to_power p by A3;
hence 0 <= ab . n by A1, A36, POWER:def 2; :: thesis: verum
end;
now
let n be Element of NAT ; :: thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))
set A = (Partial_Sums ab) . n;
set C = (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p));
set D = ((Partial_Sums ab) . n) to_power (1 / q);
A37: 0 <= (Partial_Sums ab) . n by A35, Lm2;
0 <= (Partial_Sums bp) . n by A6, Lm2;
then 0 to_power (1 / p) <= ((Partial_Sums bp) . n) to_power (1 / p) by A2, Th3;
then A38: 0 <= ((Partial_Sums bp) . n) to_power (1 / p) by A2, POWER:def 2;
0 <= (Partial_Sums ap) . n by A4, Lm2;
then 0 to_power (1 / p) <= ((Partial_Sums ap) . n) to_power (1 / p) by A2, Th3;
then 0 <= ((Partial_Sums ap) . n) to_power (1 / p) by A2, POWER:def 2;
then A39: 0 + 0 <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) by A38;
now
per cases ( (Partial_Sums ab) . n = 0 or (Partial_Sums ab) . n <> 0 ) ;
case (Partial_Sums ab) . n = 0 ; :: thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))
hence ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) by A2, A39, POWER:def 2; :: thesis: verum
end;
case A40: (Partial_Sums ab) . n <> 0 ; :: thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))
set B = 1 / (((Partial_Sums ab) . n) to_power (1 / q));
A41: 0 < ((Partial_Sums ab) . n) to_power (1 / q) by A37, A40, POWER:39;
then A42: 0 < 1 / (((Partial_Sums ab) . n) to_power (1 / q)) by XREAL_1:141;
A43: (((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * (((Partial_Sums ab) . n) to_power (1 / q))) * (1 / (((Partial_Sums ab) . n) to_power (1 / q))) = ((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * ((((Partial_Sums ab) . n) to_power (1 / q)) * (1 / (((Partial_Sums ab) . n) to_power (1 / q))))
.= ((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * 1 by A41, XCMPLX_1:88
.= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) ;
((Partial_Sums ab) . n) * (1 / (((Partial_Sums ab) . n) to_power (1 / q))) = ((Partial_Sums ab) . n) / (((Partial_Sums ab) . n) to_power (1 / q)) by XCMPLX_1:100
.= (((Partial_Sums ab) . n) to_power 1) / (((Partial_Sums ab) . n) to_power (1 / q)) by POWER:30
.= ((Partial_Sums ab) . n) to_power (1 - (1 / q)) by A37, A40, POWER:34
.= ((Partial_Sums ab) . n) to_power (1 / p) by A14 ;
hence ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) by A32, A42, A43, XREAL_1:66; :: thesis: verum
end;
end;
end;
hence ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) ; :: thesis: verum
end;
hence for n being Element of NAT holds ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) ; :: thesis: verum