let rf be real-valued FinSequence; ( rf is nonnegative-yielding implies sqrt (Sum rf) <= Sum (sqrt rf) )
defpred S1[ Nat] means for f being real-valued FinSequence st len f = $1 & f is nonnegative-yielding holds
( sqrt (Sum f) <= Sum (sqrt f) & 0 <= Sum f );
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
set n1 =
n + 1;
let f be
real-valued FinSequence;
( len f = n + 1 & f is nonnegative-yielding implies ( sqrt (Sum f) <= Sum (sqrt f) & 0 <= Sum f ) )
assume that A3:
len f = n + 1
and A4:
f is
nonnegative-yielding
;
( sqrt (Sum f) <= Sum (sqrt f) & 0 <= Sum f )
rng f c= REAL
;
then reconsider F =
f as
FinSequence of
REAL by FINSEQ_1:def 4;
reconsider fn =
F | n as
FinSequence of
REAL ;
A5:
F = fn ^ <*(F . (n + 1))*>
by A3, FINSEQ_3:55;
then sqrt F =
(sqrt fn) ^ (sqrt <*(F . (n + 1))*>)
by Th2
.=
(sqrt fn) ^ <*(sqrt (F . (n + 1)))*>
by Th3
;
then A6:
Sum (sqrt F) = (Sum (sqrt fn)) + (sqrt (F . (n + 1)))
by RVSUM_1:74;
A7:
len fn = n
by A3, FINSEQ_3:53;
then
sqrt (Sum fn) <= Sum (sqrt fn)
by A2, A4;
then A8:
(sqrt (Sum fn)) + (sqrt (f . (n + 1))) <= Sum (sqrt F)
by A6, XREAL_1:6;
A9:
Sum f = (Sum fn) + (f . (n + 1))
by A5, RVSUM_1:74;
n + 1
>= 1
by NAT_1:11;
then
n + 1
in dom f
by A3, FINSEQ_3:25;
then
f . (n + 1) in rng f
by FUNCT_1:def 3;
then A10:
f . (n + 1) >= 0
by A4;
A11:
Sum fn >= 0
by A2, A4, A7;
then
sqrt (Sum f) <= (sqrt (Sum fn)) + (sqrt (f . (n + 1)))
by A9, A10, SQUARE_1:59;
hence
(
sqrt (Sum f) <= Sum (sqrt f) &
0 <= Sum f )
by A9, A11, A10, A8, XXREAL_0:2;
verum
end;
A12:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A12, A1);
then
S1[ len rf]
;
hence
( rf is nonnegative-yielding implies sqrt (Sum rf) <= Sum (sqrt rf) )
; verum