:: Jordan Matrix Decomposition
:: by Karol P\c{a}k
::
:: Received July 11, 2008
:: Copyright (c) 2008 Association of Mizar Users
Lm1:
for x, y being set
for f being Function st f is one-to-one & x in dom f holds
rng (f +* x,y) = ((rng f) \ {(f . x)}) \/ {y}
definition
let K be
Field;
let L be
Element of
K;
let n be
Nat;
func Jordan_block L,
n -> Matrix of
K means :
Def1:
:: MATRIXJ2:def 1
(
len it = n &
width it = n & ( for
i,
j being
Nat st
[i,j] in Indices it holds
( (
i = j implies
it * i,
j = L ) & (
i + 1
= j implies
it * i,
j = 1_ K ) & (
i <> j &
i + 1
<> j implies
it * i,
j = 0. K ) ) ) );
existence
ex b1 being Matrix of K st
( len b1 = n & width b1 = n & ( for i, j being Nat st [i,j] in Indices b1 holds
( ( i = j implies b1 * i,j = L ) & ( i + 1 = j implies b1 * i,j = 1_ K ) & ( i <> j & i + 1 <> j implies b1 * i,j = 0. K ) ) ) )
uniqueness
for b1, b2 being Matrix of K st len b1 = n & width b1 = n & ( for i, j being Nat st [i,j] in Indices b1 holds
( ( i = j implies b1 * i,j = L ) & ( i + 1 = j implies b1 * i,j = 1_ K ) & ( i <> j & i + 1 <> j implies b1 * i,j = 0. K ) ) ) & len b2 = n & width b2 = n & ( for i, j being Nat st [i,j] in Indices b2 holds
( ( i = j implies b2 * i,j = L ) & ( i + 1 = j implies b2 * i,j = 1_ K ) & ( i <> j & i + 1 <> j implies b2 * i,j = 0. K ) ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines Jordan_block MATRIXJ2:def 1 :
theorem Th1: :: MATRIXJ2:1
theorem Th2: :: MATRIXJ2:2
theorem Th3: :: MATRIXJ2:3
theorem Th4: :: MATRIXJ2:4
theorem Th5: :: MATRIXJ2:5
theorem Th6: :: MATRIXJ2:6
theorem Th7: :: MATRIXJ2:7
theorem :: MATRIXJ2:8
theorem Th9: :: MATRIXJ2:9
:: deftheorem Def2 defines Jordan-block-yielding MATRIXJ2:def 2 :
Lm2:
for K being Field holds {} is FinSequence_of_Jordan_block of K
:: deftheorem Def3 defines FinSequence_of_Jordan_block MATRIXJ2:def 3 :
theorem Th10: :: MATRIXJ2:10
theorem Th11: :: MATRIXJ2:11
theorem Th12: :: MATRIXJ2:12
:: deftheorem Def4 defines nilpotent MATRIXJ2:def 4 :
theorem Th13: :: MATRIXJ2:13
theorem Th14: :: MATRIXJ2:14
definition
let K be
doubleLoopStr ;
let V be non
empty VectSpStr of
K;
let f be
nilpotent Function of
V,
V;
func degree_of_nilpotent f -> Nat means :
Def5:
:: MATRIXJ2:def 5
(
f |^ it = ZeroMap V,
V & ( for
k being
Nat st
f |^ k = ZeroMap V,
V holds
it <= k ) );
existence
ex b1 being Nat st
( f |^ b1 = ZeroMap V,V & ( for k being Nat st f |^ k = ZeroMap V,V holds
b1 <= k ) )
uniqueness
for b1, b2 being Nat st f |^ b1 = ZeroMap V,V & ( for k being Nat st f |^ k = ZeroMap V,V holds
b1 <= k ) & f |^ b2 = ZeroMap V,V & ( for k being Nat st f |^ k = ZeroMap V,V holds
b2 <= k ) holds
b1 = b2
end;
:: deftheorem Def5 defines degree_of_nilpotent MATRIXJ2:def 5 :
theorem Th15: :: MATRIXJ2:15
theorem Th16: :: MATRIXJ2:16
theorem Th17: :: MATRIXJ2:17
theorem Th18: :: MATRIXJ2:18
theorem Th19: :: MATRIXJ2:19
for
i being
Nat for
K being
Field for
V1,
V2 being
finite-dimensional VectSp of
K for
W1,
W2 being
Subspace of
V1 for
U1,
U2 being
Subspace of
V2 for
b1 being
OrdBasis of
V1 for
B2 being
FinSequence of
V2 for
bw1 being
OrdBasis of
W1 for
bw2 being
OrdBasis of
W2 for
Bu1 being
FinSequence of
U1 for
Bu2 being
FinSequence of
U2 for
M being
Matrix of
len b1,
len B2,
K for
M1 being
Matrix of
len bw1,
len Bu1,
K for
M2 being
Matrix of
len bw2,
len Bu2,
K st
b1 = bw1 ^ bw2 &
B2 = Bu1 ^ Bu2 &
M = block_diagonal <*M1,M2*>,
(0. K) &
width M1 = len Bu1 &
width M2 = len Bu2 holds
( (
i in dom bw1 implies
(Mx2Tran M,b1,B2) . (b1 /. i) = (Mx2Tran M1,bw1,Bu1) . (bw1 /. i) ) & (
i in dom bw2 implies
(Mx2Tran M,b1,B2) . (b1 /. (i + (len bw1))) = (Mx2Tran M2,bw2,Bu2) . (bw2 /. i) ) )
theorem Th20: :: MATRIXJ2:20
for
K being
Field for
V1,
V2 being
finite-dimensional VectSp of
K for
b1 being
OrdBasis of
V1 for
B2 being
FinSequence of
V2 for
M being
Matrix of
len b1,
len B2,
K for
F being
FinSequence_of_Matrix of
K st
M = block_diagonal F,
(0. K) holds
for
i,
m being
Nat st
i in dom b1 &
m = min (Len F),
i holds
(
(Mx2Tran M,b1,B2) . (b1 /. i) = Sum (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1)))))) &
len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
theorem Th21: :: MATRIXJ2:21
theorem Th22: :: MATRIXJ2:22
theorem Th23: :: MATRIXJ2:23
theorem Th24: :: MATRIXJ2:24
for
K being
Field for
L being
Element of
K for
V1,
V2 being
finite-dimensional VectSp of
K for
b1 being
OrdBasis of
V1 for
B2 being
FinSequence of
V2 for
J being
FinSequence_of_Jordan_block of
L,
K for
M being
Matrix of
len b1,
len B2,
K st
M = block_diagonal J,
(0. K) holds
for
i,
m being
Nat st
i in dom b1 &
m = min (Len J),
i holds
( (
i = Sum (Len (J | m)) implies
(Mx2Tran M,b1,B2) . (b1 /. i) = L * (B2 /. i) ) & (
i <> Sum (Len (J | m)) implies
(Mx2Tran M,b1,B2) . (b1 /. i) = (L * (B2 /. i)) + (B2 /. (i + 1)) ) )
theorem Th25: :: MATRIXJ2:25
Lm3:
for n being Nat
for K being Field
for L being Element of K
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of L,K
for M being Matrix of len b1, len b1,K st M = block_diagonal J,(0. K) & len b1 <> 0 holds
( ((Mx2Tran M,b1,b1) |^ n) . (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) = ((power K) . L,n) * (b1 /. (Sum (Len (J | (min (Len J),(len b1)))))) & Sum (Len (J | (min (Len J),(len b1)))) in dom b1 )
theorem :: MATRIXJ2:26
theorem :: MATRIXJ2:27
Lm4:
for K being Field
for V1, V2 being VectSp of K
for f being linear-transformation of V1,V2
for W1 being Subspace of V1
for W2 being Subspace of V2
for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
theorem Th28: :: MATRIXJ2:28
theorem Th29: :: MATRIXJ2:29
theorem Th30: :: MATRIXJ2:30
theorem Th31: :: MATRIXJ2:31
theorem :: MATRIXJ2:32