let a, b be Real_Sequence; for p being Real st 1 = p & a rto_power p is summable & b rto_power p is summable holds
( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )
let p be Real; ( 1 = p & a rto_power p is summable & b rto_power p is summable implies ( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) ) )
assume that
A1:
p = 1
and
A2:
a rto_power p is summable
and
A3:
b rto_power p is summable
; ( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )
then A5:
(a + b) rto_power p = abs (a + b)
by SEQ_1:12;
A6:
a = seq_id a
;
A7:
a rto_power p = |.a.|
by A4, SEQ_1:12;
then
a is absolutely_summable
by A2, SERIES_1:def 4;
then reconsider a1 = a as VECTOR of l1_Space by A6, RSSPACE3:6;
|.b.| is summable
by A3, A4, SEQ_1:12;
then A8:
|.a.| + |.b.| is summable
by A2, A7, SERIES_1:7;
A9:
b rto_power p = |.b.|
by A4, SEQ_1:12;
then A10:
(Sum (b rto_power p)) to_power (1 / p) = Sum |.b.|
by A1, POWER:25;
A11:
b = seq_id b
;
b is absolutely_summable
by A3, A9, SERIES_1:def 4;
then reconsider b1 = b as VECTOR of l1_Space by A11, RSSPACE3:6;
A12:
||.b1.|| = Sum (abs (seq_id b1))
by RSSPACE3:def 2, RSSPACE3:def 3;
deffunc H1( Nat) -> set = |.(a . $1).| + |.(b . $1).|;
consider c being Real_Sequence such that
A14:
for n being Nat holds c . n = H1(n)
from SEQ_1:sch 1();
then
c = |.a.| + |.b.|
by SEQ_1:7;
hence
(a + b) rto_power p is summable
by A5, A8, A15, SERIES_1:20; (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p))
A17:
||.a1.|| = Sum (abs (seq_id a1))
by RSSPACE3:def 2, RSSPACE3:def 3;
A19: ||.(a1 + b1).|| =
Sum (abs (seq_id (a1 + b1)))
by RSSPACE3:def 2, RSSPACE3:def 3
.=
Sum (abs (seq_id ((seq_id a1) + (seq_id b1))))
by RSSPACE3:6
.=
Sum (abs ((seq_id a1) + (seq_id b1)))
;
A20:
||.(a1 + b1).|| <= ||.a1.|| + ||.b1.||
by RSSPACE3:7;
(Sum (a rto_power p)) to_power (1 / p) = Sum |.a.|
by A1, A7, POWER:25;
hence
(Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p))
by A1, A5, A10, A20, A19, A17, A12, POWER:25; verum