let n, m be Nat; for M being Matrix of n,m,F_Real
for f being n -element real-valued FinSequence ex L being m -element FinSequence of REAL st
( |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| & ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) )
let M be Matrix of n,m,F_Real; for f being n -element real-valued FinSequence ex L being m -element FinSequence of REAL st
( |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| & ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) )
let f be n -element real-valued FinSequence; ex L being m -element FinSequence of REAL st
( |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| & ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) )
set Lf = LineVec2Mx (@ f);
set LfM = (LineVec2Mx (@ f)) * M;
set LM = Line (((LineVec2Mx (@ f)) * M),1);
deffunc H1( Nat) -> object = |.(@ (Col (M,$1))).|;
consider L being FinSequence such that
A1:
( len L = m & ( for k being Nat st k in dom L holds
L . k = H1(k) ) )
from FINSEQ_1:sch 2();
rng L c= REAL
then
L is FinSequence of REAL
by FINSEQ_1:def 4;
then reconsider L1 = L as Element of m -tuples_on REAL by A1, FINSEQ_2:92;
take
L1
; ( |.((Mx2Tran M) . f).| <= (Sum L1) * |.f.| & ( for i being Nat st i in dom L1 holds
L1 . i = |.(@ (Col (M,i))).| ) )
per cases
( n <> 0 or n = 0 )
;
suppose A4:
n <> 0
;
( |.((Mx2Tran M) . f).| <= (Sum L1) * |.f.| & ( for i being Nat st i in dom L1 holds
L1 . i = |.(@ (Col (M,i))).| ) )then A5:
len M = n
by MATRIX13:1;
(Mx2Tran M) . f = Line (
((LineVec2Mx (@ f)) * M),1)
by A4, Def3;
then A6:
len (Line (((LineVec2Mx (@ f)) * M),1)) = m
by CARD_1:def 7;
A7:
|.((Mx2Tran M) . f).| = sqrt (Sum (sqr (@ (Line (((LineVec2Mx (@ f)) * M),1)))))
by A4, Def3;
reconsider LM =
Line (
((LineVec2Mx (@ f)) * M),1) as
Element of
m -tuples_on REAL by A6, FINSEQ_2:92;
len (abs LM) = m
by CARD_1:def 7;
then reconsider aLM =
abs LM as
Element of
m -tuples_on REAL by FINSEQ_2:92;
A8:
len f = n
by CARD_1:def 7;
then A9:
width (LineVec2Mx (@ f)) = n
by MATRIX13:1;
width M = m
by A4, MATRIX13:1;
then A10:
width ((LineVec2Mx (@ f)) * M) = m
by A5, A9, MATRIX_3:def 4;
len (LineVec2Mx (@ f)) = 1
by MATRIX13:1;
then A11:
len ((LineVec2Mx (@ f)) * M) = 1
by A5, A9, MATRIX_3:def 4;
now for i being Nat st i in Seg m holds
aLM . i <= (|.f.| * L1) . ilet i be
Nat;
( i in Seg m implies aLM . i <= (|.f.| * L1) . i )A12:
len (Col (M,i)) = n
by A5, MATRIX_0:def 8;
then A13:
|.|(f,(@ (Col (M,i))))|.| <= |.f.| * H1(
i)
by A8, EUCLID_2:15;
assume A14:
i in Seg m
;
aLM . i <= (|.f.| * L1) . ithen A15:
( 1
<= i &
i <= m )
by FINSEQ_1:1;
then A16:
[1,i] in Indices ((LineVec2Mx (@ f)) * M)
by A11, A10, MATRIX_0:30;
i in dom L
by A1, A15, FINSEQ_3:25;
then A17:
L . i = H1(
i)
by A1;
LM . i =
((LineVec2Mx (@ f)) * M) * (1,
i)
by A10, A14, MATRIX_0:def 7
.=
(Line ((LineVec2Mx (@ f)),1)) "*" (Col (M,i))
by A5, A9, A16, MATRIX_3:def 4
.=
Sum (mlt ((@ f),(Col (M,i))))
by MATRIX15:25
.=
Sum (mlt (f,(@ (Col (M,i)))))
by A8, A12, MATRPROB:35, MATRPROB:36
.=
|(f,(@ (Col (M,i))))|
by RVSUM_1:def 16
;
then
aLM . i <= |.f.| * H1(
i)
by A13, VALUED_1:18;
hence
aLM . i <= (|.f.| * L1) . i
by A17, RVSUM_1:44;
verum end; then A18:
Sum aLM <= Sum (|.f.| * L1)
by RVSUM_1:82;
sqr LM = LM (#) LM
by VALUED_1:def 8;
then
sqrt (Sum (sqr LM)) <= Sum (sqrt (sqr LM))
by Th5;
then
(
Sum (|.f.| * L1) = |.f.| * (Sum L1) &
sqrt (Sum (sqr LM)) <= Sum aLM )
by Th4, RVSUM_1:87;
hence
(
|.((Mx2Tran M) . f).| <= (Sum L1) * |.f.| & ( for
i being
Nat st
i in dom L1 holds
L1 . i = |.(@ (Col (M,i))).| ) )
by A7, A1, A18, XXREAL_0:2;
verum end; end;