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))
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 A2: 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))
reconsider pp = 1 / p as Real ;
reconsider qq = 1 - pp as Real ;
reconsider q = 1 / qq as Real ;
1 / p < 1 by A1, XREAL_1:191;
then A3: 1 - 1 < 1 - pp by XREAL_1:17;
A4: qq = 1 / q by XCMPLX_1:56;
then A5: 0 < q by A3;
A6: q <> 0 by A3, A4;
A7: 1 / p > 0 by A1, XREAL_1:141;
A8: 1 - 1 < p - 1 by A1, XREAL_1:16;
A9: (1 / p) + (1 / q) = 1 by A4;
then (((1 * q) + (1 * p)) / (p * q)) * (p * q) = 1 * (p * q) by A1, A6, XCMPLX_1:117;
then A10: q + p = p * q by A1, A6, XCMPLX_1:6, XCMPLX_1:88;
deffunc H₁( Element of NAT ) -> Element of REAL = (abs ((a . $1) + (b . $1))) to_power (p - 1);
consider x being Real_Sequence such that
A11: for n being Element of NAT holds x . n = H₁(n) from SEQ_1:sch 1();
A12: for n being Element of NAT holds 0 <= x . n

proof

let n be Element of NAT ; :: thesis: 0 <= x . n
A13: x . n = (abs ((a . n) + (b . n))) to_power (p - 1) by A11;

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 A8, A13, POWER:def 2; :: thesis: verum

end;

case abs ((a . n) + (b . n)) > 0 ; :: thesis: 0 <= x . n

hence 0 <= x . n by A13, POWER:39; :: thesis: verum

end;

end;

end;

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

end;

A14: 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 A15: 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 A2
.= (x . n) * (abs ((a . n) + (b . n))) by A1, A15, POWER:def 2 ; :: thesis: verum

end;

case A16: abs ((a . n) + (b . n)) <> 0 ; :: thesis: ab . n = (x . n) * (abs ((a . n) + (b . n)))

A17: 0 <= abs ((a . n) + (b . n)) by COMPLEX1:132;
thus ab . n = (abs ((a . n) + (b . n))) to_power ((p - 1) + 1) by A2
.= ((abs ((a . n) + (b . n))) to_power (p - 1)) * ((abs ((a . n) + (b . n))) to_power 1) by A16, A17, 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 A11 ; :: thesis: verum

end;

end;

end;

hence ab . n = (x . n) * (abs ((a . n) + (b . n))) ; :: thesis: verum

end;

A18: 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
A19: 0 <= x . n by A12;
A20: ab . n = (x . n) * (abs ((a . n) + (b . n))) by A14;
(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 ;
hence ab . n <= ((x (#) (abs a)) + (x (#) (abs b))) . n by A19, A20, COMPLEX1:142, XREAL_1:66; :: thesis: verum

end;

A21: 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 A12;
then A22: 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 A22, COMPLEX1:151 ; :: thesis: verum

end;

A23: 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 A12;
then A24: 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 A24, COMPLEX1:151 ; :: thesis: verum

end;

A25: 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 A12;
then abs (x . n) = x . n by ABSVALUE:def 1;
then A26: (abs (x . n)) to_power q = ((abs ((a . n) + (b . n))) to_power (p - 1)) to_power q by A11;

now

per cases ( abs ((a . n) + (b . n)) = 0 or abs ((a . n) + (b . n)) <> 0 ) ;

case A27: abs ((a . n) + (b . n)) = 0 ; :: thesis: (abs (x . n)) to_power q = ab . n

then A28: ab . n = 0 to_power p by A2
.= 0 by A1, POWER:def 2 ;
(abs (x . n)) to_power q = 0 to_power q by A8, A26, A27, POWER:def 2
.= 0 by A5, POWER:def 2 ;
hence (abs (x . n)) to_power q = ab . n by A28; :: 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 A26, POWER:38
.= ab . n by A2, A10 ;
:: thesis: verum

end;

end;

end;

hence (abs (x . n)) to_power q = ab . n ; :: thesis: verum

end;

A29: 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))
A30: (Partial_Sums ab) . n <= (Partial_Sums ((x (#) (abs a)) + (x (#) (abs b)))) . n by A18, SERIES_1:17;
A31: (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 ;
A32: (Partial_Sums (x (#) (abs a))) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums ab) . n) to_power (1 / q)) by A1, A2, A9, A21, A25, Th6;
(Partial_Sums (x (#) (abs b))) . n <= (((Partial_Sums bp) . n) to_power (1 / p)) * (((Partial_Sums ab) . n) to_power (1 / q)) by A1, A2, A9, A23, A25, Th6;
then ((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 A32, XREAL_1:9;
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 A30, A31, XXREAL_0:2; :: thesis: verum

end;

A33: for n being Element of NAT holds 0 <= ap . n

proof

let n be Element of NAT ; :: thesis: 0 <= ap . n
A34: ap . n = (abs (a . n)) to_power p by A2;

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, A34, POWER:def 2; :: thesis: verum

end;

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

hence 0 <= ap . n by A34, POWER:39; :: thesis: verum

end;

end;

end;

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

end;

A35: for n being Element of NAT holds 0 <= bp . n

proof

let n be Element of NAT ; :: thesis: 0 <= bp . n
A36: bp . n = (abs (b . n)) to_power p by A2;

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, A36, POWER:def 2; :: thesis: verum

end;

case abs (b . n) > 0 ; :: thesis: 0 <= bp . n

hence 0 <= bp . n by A36, POWER:39; :: thesis: verum

end;

end;

end;

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

end;

A37: for n being Element of NAT holds 0 <= ab . n

proof

let n be Element of NAT ; :: thesis: 0 <= ab . n
A38: 0 <= abs ((a . n) + (b . n)) by COMPLEX1:132;
A39: ab . n = (abs ((a . n) + (b . n))) to_power p by A2;
0 to_power p <= (abs ((a . n) + (b . n))) to_power p by A1, A38, Th3;
hence 0 <= ab . n by A1, A39, 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);
A40: 0 <= (Partial_Sums ab) . n by A37, Lm2;
0 <= (Partial_Sums ap) . n by A33, Lm2;
then 0 to_power (1 / p) <= ((Partial_Sums ap) . n) to_power (1 / p) by A7, Th3;
then A41: 0 <= ((Partial_Sums ap) . n) to_power (1 / p) by A7, POWER:def 2;
0 <= (Partial_Sums bp) . n by A35, Lm2;
then 0 to_power (1 / p) <= ((Partial_Sums bp) . n) to_power (1 / p) by A7, Th3;
then 0 <= ((Partial_Sums bp) . n) to_power (1 / p) by A7, POWER:def 2;
then A42: 0 + 0 <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) by A41;

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 A7, A42, POWER:def 2; :: thesis: verum

end;

case A43: (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))

then A44: 0 < ((Partial_Sums ab) . n) to_power (1 / q) by A40, POWER:39;
set B = 1 / (((Partial_Sums ab) . n) to_power (1 / q));
A45: 0 < 1 / (((Partial_Sums ab) . n) to_power (1 / q)) by A44, XREAL_1:141;
A46: (((((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 A44, 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 A40, A43, POWER:34
.= ((Partial_Sums ab) . n) to_power (1 / p) by A4 ;
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 A29, A45, A46, 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