let p be Real; :: thesis: ( 1 <= p implies for a, b being Real_Sequence
for n being Nat holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) )
assume A1: 1 <= p ; :: thesis: for a, b being Real_Sequence
for n being Nat holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
reconsider p = p as Real ;
let a, b be Real_Sequence; :: thesis: for n being Nat holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
set ap = a rto_power p;
set bp = b rto_power p;
set ab = (a + b) rto_power p;
let n be Nat; :: thesis: ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
now :: thesis: ( ( p > 1 & ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) ) or ( p = 1 & ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) ) )
per cases ( p > 1 or p = 1 ) by A1, XXREAL_0:1;
case A2: p > 1 ; :: thesis: ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
now :: thesis: for n being Nat holds
( (a rto_power p) . n = |.(a . n).| to_power p & (b rto_power p) . n = |.(b . n).| to_power p & ((a + b) rto_power p) . n = |.((a . n) + (b . n)).| to_power p )
let n be Nat; :: thesis: ( (a rto_power p) . n = |.(a . n).| to_power p & (b rto_power p) . n = |.(b . n).| to_power p & ((a + b) rto_power p) . n = |.((a . n) + (b . n)).| to_power p )
thus (a rto_power p) . n = |.(a . n).| to_power p by Def1; :: thesis: ( (b rto_power p) . n = |.(b . n).| to_power p & ((a + b) rto_power p) . n = |.((a . n) + (b . n)).| to_power p )
thus (b rto_power p) . n = |.(b . n).| to_power p by Def1; :: thesis: ((a + b) rto_power p) . n = |.((a . n) + (b . n)).| to_power p
((a + b) rto_power p) . n = |.((a + b) . n).| to_power p by Def1
.= |.((a . n) + (b . n)).| to_power p by SEQ_1:7 ;
hence ((a + b) rto_power p) . n = |.((a . n) + (b . n)).| to_power p ; :: thesis: verum
end;
hence ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) by A2, HOLDER_1:7; :: thesis: verum
end;
case p = 1 ; :: thesis: ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
hence ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) by Lm3; :: thesis: verum
end;
end;
end;
hence ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p)) ; :: thesis: verum