let n be Nat; for x being Element of REAL n
for xMAX being Real st xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) holds
( Sum (abs x) <= n * xMAX & xMAX <= |.x.| & |.x.| <= Sum (abs x) )
let x be Element of REAL n; for xMAX being Real st xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) holds
( Sum (abs x) <= n * xMAX & xMAX <= |.x.| & |.x.| <= Sum (abs x) )
let xMAX be Real; ( xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) implies ( Sum (abs x) <= n * xMAX & xMAX <= |.x.| & |.x.| <= Sum (abs x) ) )
assume A1:
( xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) )
; ( Sum (abs x) <= n * xMAX & xMAX <= |.x.| & |.x.| <= Sum (abs x) )
len x = n
by CARD_1:def 7;
then A2:
dom x = Seg n
by FINSEQ_1:def 3;
A3:
dom (abs x) = dom x
by VALUED_1:def 11;
set F = n |-> xMAX;
for j being Nat st j in Seg n holds
(abs x) . j <= (n |-> xMAX) . j
then A5:
Sum (abs x) <= Sum (n |-> xMAX)
by RVSUM_1:82;
consider i being object such that
A6:
( i in dom (abs x) & xMAX = (abs x) . i )
by A1, FUNCT_1:def 3;
reconsider i = i as Element of NAT by A6;
A7: (abs x) . i =
absreal . (x . i)
by A3, A6, FUNCT_1:13
.=
|.(x . i).|
by EUCLID:def 2
;
reconsider y = x as Point of (TOP-REAL n) by EUCLID:22;
reconsider y = y as FinSequence of REAL ;
defpred S1[ Nat] means for x being Element of REAL $1 holds |.x.| ^2 <= (Sum (abs x)) ^2 ;
A8:
S1[ 0 ]
by SQUARE_1:def 2, RVSUM_1:72;
A9:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A10:
S1[
n]
;
S1[n + 1]
let x be
Element of
REAL (n + 1);
|.x.| ^2 <= (Sum (abs x)) ^2
set y =
x | n;
A11:
len x = n + 1
by CARD_1:def 7;
A12:
x | n is
Element of
(len (x | n)) -tuples_on REAL
by FINSEQ_2:92;
reconsider y =
x | n as
Element of
REAL n by A11, A12, NAT_1:11, FINSEQ_1:59;
n + 1
in Seg (n + 1)
by FINSEQ_1:4;
then
n + 1
in dom x
by A11, FINSEQ_1:def 3;
then
x . (n + 1) in rng x
by FUNCT_1:3;
then reconsider w =
x . (n + 1) as
Element of
REAL ;
A13:
x = y ^ <*w*>
by A11, FINSEQ_3:55;
A14:
0 <= Sum (sqr y)
by RVSUM_1:86;
A15:
0 <= Sum (sqr x)
by RVSUM_1:86;
sqr x = (sqr y) ^ <*(sqrreal . w)*>
by A13, FINSEQOP:8;
then A16:
Sum (sqr x) =
(Sum (sqr y)) + (sqrreal . w)
by RVSUM_1:74
.=
(Sum (sqr y)) + (w ^2)
by RVSUM_1:def 2
.=
(|.y.| ^2) + (w ^2)
by A14, SQUARE_1:def 2
;
A17:
|.x.| ^2 = Sum (sqr x)
by A15, SQUARE_1:def 2;
abs x =
(abs y) ^ (abs <*w*>)
by A13, FINSEQOP:9
.=
(abs y) ^ <*|.w.|*>
by JORDAN2B:19
;
then (Sum (abs x)) ^2 =
((Sum (abs y)) + |.w.|) ^2
by RVSUM_1:74
.=
(((Sum (abs y)) ^2) + ((2 * (Sum (abs y))) * |.w.|)) + (|.w.| ^2)
.=
(((Sum (abs y)) ^2) + ((2 * (Sum (abs y))) * |.w.|)) + (w ^2)
by COMPLEX1:75
;
then A18:
((Sum (abs x)) ^2) - (|.x.| ^2) = (((Sum (abs y)) ^2) - (|.y.| ^2)) + ((2 * (Sum (abs y))) * |.w.|)
by A16, A17;
A19:
0 <= ((Sum (abs y)) ^2) - (|.y.| ^2)
by A10, XREAL_1:48;
(
0 <= |.w.| &
0 <= Sum (abs y) )
by Th9;
hence
|.x.| ^2 <= (Sum (abs x)) ^2
by A18, A19, XREAL_1:49;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A8, A9);
then A20:
|.x.| ^2 <= (Sum (abs x)) ^2
;
n is Element of NAT
by ORDINAL1:def 12;
then
|.(y /. i).| <= |.x.|
by A2, A3, A6, PDIFF_8:1;
hence
( Sum (abs x) <= n * xMAX & xMAX <= |.x.| & |.x.| <= Sum (abs x) )
by A3, A5, A6, A7, A20, Th9, PARTFUN1:def 6, RVSUM_1:80, SQUARE_1:16; verum