:: Block Diagonal Matrices :: by Karol P\c{a}k :: :: Received May 13, 2008 :: Copyright (c) 2008-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, NAT_1, VECTSP_1, SUBSET_1, XBOOLE_0, MATRIX_1, FINSEQ_1, ALGSTR_0, RELAT_1, ARYTM_3, TARSKI, STRUCT_0, ZFMISC_1, ORDINAL4, XXREAL_0, FUNCT_1, PARTFUN1, FINSEQ_3, CARD_1, ARYTM_1, FINSEQ_2, CARD_3, GROUP_1, RFINSEQ, TREES_1, INCSP_1, MATRIX_3, SUPINF_2, LAPLACE, MATRIX11, MESFUNC1, RVSUM_1, MATHMORP, VALUED_1, FVSUM_1, MATRIXJ1, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, CARD_1, XCMPLX_0, ALGSTR_0, XXREAL_0, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, STRUCT_0, RLVECT_1, GROUP_1, VECTSP_1, FINSEQ_2, MATRIX_0, MATRIX_1, FVSUM_1, NAT_D, GROUP_4, MATRIX_3, MATRIX11, FINSEQOP, MATRIX13, LAPLACE, RFINSEQ, WSIERP_1; constructors GROUP_4, MATRIX11, MATRIX13, LAPLACE, RFINSEQ, WSIERP_1, REAL_1, BINARITH, RELSET_1, FVSUM_1, MATRIX_1, NUMBERS, RECDEF_1; registrations XBOOLE_0, FINSET_1, STRUCT_0, VECTSP_1, ORDINAL1, XXREAL_0, NAT_1, FINSEQ_1, RELAT_1, FINSEQ_2, MATRIX13, XREAL_0, VALUED_0, CARD_1; requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET; begin :: Preliminaries reserve i,j,m,n,k for Nat, x,y for set, K for Field, a,a1,a2 for Element of K, D for non empty set, d,d1,d2 for Element of D, M,M1,M2 for (Matrix of D), A,A1,A2,B1,B2 for (Matrix of K), f,g for FinSequence of NAT; theorem :: MATRIXJ1:1 for K be non empty addLoopStr for f1,f2,g1,g2 be FinSequence of K st len f1 = len f2 holds (f1+f2)^(g1+g2)=(f1^g1)+(f2^g2); theorem :: MATRIXJ1:2 for f,g be FinSequence of D st i in dom f holds Del(f^g,i) = Del( f,i)^g; theorem :: MATRIXJ1:3 for f,g be FinSequence of D st i in dom g holds Del(f^g,i+len f)= f^Del(g,i); theorem :: MATRIXJ1:4 i in Seg (n+1) implies Del((n+1) |->d,i)=n |-> d; theorem :: MATRIXJ1:5 Product (n|->a) = (power K).(a,n); definition let f; let i be Nat such that i in Seg (Sum f); func min(f,i) -> Element of NAT means :: MATRIXJ1:def 1 i <= Sum(f|it) & it in dom f & for j st i<=Sum (f|j) holds it <= j; end; theorem :: MATRIXJ1:6 i in dom f & f.i <> 0 implies min(f,Sum(f|i)) = i; theorem :: MATRIXJ1:7 i in Seg (Sum f) implies min(f,i)-'1 = min(f,i) - 1 & Sum(f| (min( f,i)-'1)) 0) & ( j in dom f implies f.j <> 0) holds i = j; begin :: Finite Sequences of Matrices definition let D; let F be FinSequence of (D**); attr F is Matrix-yielding means :: MATRIXJ1:def 2 for i st i in dom F holds F.i is Matrix of D; end; registration let D; cluster Matrix-yielding for FinSequence of D**; end; definition let D; mode FinSequence_of_Matrix of D is Matrix-yielding FinSequence of D**; end; definition let K; mode FinSequence_of_Matrix of K is Matrix-yielding FinSequence of (the carrier of K)**; end; theorem :: MATRIXJ1:12 {} is FinSequence_of_Matrix of D; reserve F,F1,F2 for FinSequence_of_Matrix of D, G,G9,G1,G2 for FinSequence_of_Matrix of K; definition let D,F,x; redefine func F.x -> Matrix of D; end; definition let D,F1,F2; redefine func F1^F2 -> FinSequence_of_Matrix of D; end; definition let D,M1; redefine func <* M1 *> -> FinSequence_of_Matrix of D; let M2; redefine func <* M1,M2 *> -> FinSequence_of_Matrix of D; end; definition let D,n,F; redefine func F|n -> FinSequence_of_Matrix of D; redefine func F/^n -> FinSequence_of_Matrix of D; end; begin :: Sequences of Sizes of Matrices in a Finite Sequence definition let D,F; func Len F -> FinSequence of NAT means :: MATRIXJ1:def 3 dom it = dom F & for i st i in dom it holds it.i=len (F.i); func Width F -> FinSequence of NAT means :: MATRIXJ1:def 4 dom it = dom F & for i st i in dom it holds it.i=width (F.i); end; definition let D,F; redefine func Len F -> Element of (len F)-tuples_on NAT; redefine func Width F -> Element of (len F)-tuples_on NAT; end; theorem :: MATRIXJ1:13 Sum Len F = 0 implies Sum Width F = 0; theorem :: MATRIXJ1:14 Len (F1 ^ F2) = Len F1 ^ Len F2; theorem :: MATRIXJ1:15 Len <*M*> = <*len M*>; theorem :: MATRIXJ1:16 Sum Len <*M1,M2*> = len M1 + len M2; theorem :: MATRIXJ1:17 Len (F1|n) = (Len F1) |n; theorem :: MATRIXJ1:18 Width (F1 ^ F2)= Width F1 ^ Width F2; theorem :: MATRIXJ1:19 Width <*M*> = <*width M*>; theorem :: MATRIXJ1:20 Sum Width <*M1,M2*>=width M1+width M2; theorem :: MATRIXJ1:21 Width (F1|n) =(Width F1) |n; begin :: Block Diagonal Matrices definition let D; let d be Element of D; let F be FinSequence_of_Matrix of D; func block_diagonal(F,d) -> Matrix of D means :: MATRIXJ1:def 5 len it = Sum Len F & width it = Sum Width F & for i,j st [i,j] in Indices it holds (j<=Sum((Width F) | (min(Len F,i)-'1)) or j>Sum ((Width F) |min(Len F,i)) implies it*(i,j) = d) & ( Sum((Width F) | (min(Len F,i)-'1)) < j & j <= Sum((Width F) |min(Len F,i)) implies it*(i,j) = F.min(Len F,i)*(i-'Sum((Len F) | (min(Len F,i)-'1)), j-'Sum ((Width F) | (min(Len F,i)-'1)))); end; definition let D; let d be Element of D; let F be FinSequence_of_Matrix of D; redefine func block_diagonal(F,d) -> Matrix of Sum Len F,Sum Width F,D; end; theorem :: MATRIXJ1:22 for F be FinSequence_of_Matrix of D st F={} holds block_diagonal(F,d)= {}; theorem :: MATRIXJ1:23 for M be Matrix of Sum Len (<*M1,M2*>),Sum Width (<*M1,M2*>),D holds M = block_diagonal(<*M1,M2*>,d) iff for i holds (i in dom M1 implies Line (M,i)=Line(M1,i)^(width M2 |-> d)) & (i in dom M2 implies Line(M,i+len M1)=( width M1|->d)^Line(M2,i)); theorem :: MATRIXJ1:24 for M be Matrix of Sum Len (<*M1,M2*>),Sum Width (<*M1,M2*>),D holds M = block_diagonal(<*M1,M2*>,d) iff for i holds (i in Seg width M1 implies Col(M,i) = Col(M1,i)^(len M2 |-> d)) & (i in Seg width M2 implies Col(M ,i+width M1)=(len M1|->d)^Col(M2,i)); theorem :: MATRIXJ1:25 Indices block_diagonal(F1,d1) is Subset of Indices block_diagonal(F1^F2,d2); theorem :: MATRIXJ1:26 [i,j] in Indices block_diagonal(F1,d) implies block_diagonal(F1, d)*(i,j) = block_diagonal(F1^F2,d)*(i,j); theorem :: MATRIXJ1:27 [i,j] in Indices block_diagonal(F2,d1) iff i>0 & j>0 & [i+Sum Len F1,j+Sum Width F1] in Indices block_diagonal(F1^F2,d2); theorem :: MATRIXJ1:28 [i,j] in Indices block_diagonal(F2,d) implies block_diagonal(F2, d)*(i,j) = block_diagonal(F1^F2,d)*(i+Sum Len F1,j+Sum Width F1); theorem :: MATRIXJ1:29 [i,j] in Indices block_diagonal(F1^F2,d) & (i <= Sum Len F1 & j > Sum Width F1 or i > Sum Len F1 & j <= Sum Width F1) implies block_diagonal(F1 ^F2,d)*(i,j) = d; theorem :: MATRIXJ1:30 for i,j,k st i in dom F & [j,k] in Indices F.i holds [j+Sum (( Len F) | (i-'1)), k+Sum((Width F) | (i-'1))] in Indices block_diagonal(F,d) & (F.i)*(j,k) = block_diagonal(F,d)*(j+Sum ((Len F) | (i-'1)), k+Sum((Width F) | (i-'1))); theorem :: MATRIXJ1:31 i in dom F implies F.i = Segm(block_diagonal(F,d),(Seg Sum((Len F) |i))\Seg Sum((Len F) | (i-'1)), (Seg Sum((Width F) |i))\Seg Sum((Width F) | (i-'1) )); theorem :: MATRIXJ1:32 M = Segm(block_diagonal(<*M*>^F,d),Seg len M,Seg width M); theorem :: MATRIXJ1:33 M = Segm(block_diagonal(F^<*M*>,d),Seg (len M+Sum Len F)\Seg Sum Len F, Seg (width M+Sum Width F)\Seg Sum Width F); theorem :: MATRIXJ1:34 block_diagonal(<*M*>,d) = M; theorem :: MATRIXJ1:35 block_diagonal(F1^F2,d) = block_diagonal(<*block_diagonal(F1,d) *>^F2,d); theorem :: MATRIXJ1:36 block_diagonal(F1^F2,d) = block_diagonal(F1^<*block_diagonal(F2, d)*>,d); theorem :: MATRIXJ1:37 i in Seg Sum Len F & m = min(Len F,i) implies Line(block_diagonal(F,d) ,i) = (Sum (Width F| (m-'1)) |->d)^ Line(F.m,i-'Sum (Len F| (m-'1)))^ ((Sum Width F-'Sum (Width F|m)) |->d); theorem :: MATRIXJ1:38 i in Seg Sum Width F & m = min(Width F,i) implies Col(block_diagonal(F ,d),i) = (Sum (Len F| (m-'1)) |->d)^ Col(F.m,i-'Sum (Width F| (m-'1)))^ ((Sum Len F-'Sum (Len F|m)) |->d); theorem :: MATRIXJ1:39 for M1,M2,N1,N2 be Matrix of D st len M1=len N1 & width M1=width N1 & len M2=len N2 & width M2=width N2 & block_diagonal(<*M1,M2*>,d1) = block_diagonal(<*N1,N2*>,d2) holds M1 = N1 & M2= N2; theorem :: MATRIXJ1:40 M={} implies block_diagonal(F^<*M*>,d) = block_diagonal(F,d) & block_diagonal(<*M*>^F,d) = block_diagonal(F,d); theorem :: MATRIXJ1:41 i in dom A & width A = width DelLine(A,i) implies DelLine( block_diagonal(<*A*>^G,a),i) = block_diagonal(<*DelLine(A,i)*>^G,a); theorem :: MATRIXJ1:42 i in dom A & width A = width DelLine(A,i) implies DelLine( block_diagonal(G^<*A*>,a),Sum Len G+i) = block_diagonal(G^<*DelLine(A,i)*>,a) ; theorem :: MATRIXJ1:43 i in Seg width A implies DelCol(block_diagonal(<*A*>^G,a),i) = block_diagonal(<*DelCol(A,i)*>^G,a); theorem :: MATRIXJ1:44 i in Seg width A implies DelCol(block_diagonal(G^<*A*>,a),i+Sum Width G) = block_diagonal(G^<*DelCol(A,i)*>,a); definition let D; let F be FinSequence of (D**); attr F is Square-Matrix-yielding means :: MATRIXJ1:def 6 for i st i in dom F ex n st F. i is Matrix of n,D; end; registration let D; cluster Square-Matrix-yielding for FinSequence of D**; end; registration let D; cluster Square-Matrix-yielding -> Matrix-yielding for FinSequence of D**; end; definition let D; mode FinSequence_of_Square-Matrix of D is Square-Matrix-yielding FinSequence of D**; end; definition let K; mode FinSequence_of_Square-Matrix of K is Square-Matrix-yielding FinSequence of (the carrier of K)**; end; reserve S,S1,S2 for FinSequence_of_Square-Matrix of D, R,R1,R2 for FinSequence_of_Square-Matrix of K; theorem :: MATRIXJ1:45 {} is FinSequence_of_Square-Matrix of D; definition let D,S,x; redefine func S.x -> Matrix of len (S.x),D; end; definition let D,S1,S2; redefine func S1^S2 -> FinSequence_of_Square-Matrix of D; end; definition let D,n; let M1 be Matrix of n,D; redefine func <* M1 *> -> FinSequence_of_Square-Matrix of D; end; definition let D,n,m; let M1 be Matrix of n,D; let M2 be Matrix of m,D; redefine func <* M1,M2 *> -> FinSequence_of_Square-Matrix of D; end; definition let D,n,S; redefine func S|n -> FinSequence_of_Square-Matrix of D; redefine func S/^n -> FinSequence_of_Square-Matrix of D; end; theorem :: MATRIXJ1:46 Len S = Width S; definition let D; let d be Element of D; let S be FinSequence_of_Square-Matrix of D; redefine func block_diagonal(S,d) -> Matrix of Sum Len S,D; end; theorem :: MATRIXJ1:47 for A be (Matrix of n,K) st i in dom A & j in Seg n holds Deleting(block_diagonal(<*A*>^R,a),i,j)= block_diagonal(<*Deleting(A,i,j)*>^R,a ); theorem :: MATRIXJ1:48 for A be Matrix of n,K st i in dom A & j in Seg n holds Deleting( block_diagonal(R^<*A*>,a),i+Sum Len R,j+Sum Len R)= block_diagonal(R^<*Deleting (A,i,j)*>,a); definition let K,R; func Det R -> FinSequence of K means :: MATRIXJ1:def 7 dom it = dom R & for i st i in dom it holds it.i = Det R.i; end; definition let K,R; redefine func Det R-> Element of (len R)-tuples_on the carrier of K; end; reserve N for (Matrix of n,K), N1 for (Matrix of m,K); theorem :: MATRIXJ1:49 Det <*N*> = <*Det N*>; theorem :: MATRIXJ1:50 Det (R1^R2) = Det R1^Det R2; theorem :: MATRIXJ1:51 Det (R|n) = (Det R) |n; theorem :: MATRIXJ1:52 Det block_diagonal(<*N,N1*>,0.K) = Det N * Det N1; theorem :: MATRIXJ1:53 Det block_diagonal(R,0.K) = Product (Det R); theorem :: MATRIXJ1:54 len A1 <> width A1 & N = block_diagonal(<*A1,A2*>,0.K) implies Det N = 0.K; theorem :: MATRIXJ1:55 Len G <> Width G implies for M be Matrix of n,K st M = block_diagonal( G,0.K) holds Det M = 0.K; begin :: An Example of a Finite Sequence of Matrices definition let K; let f be FinSequence of NAT; func 1.(K,f) -> FinSequence_of_Square-Matrix of K means :: MATRIXJ1:def 8 dom it = dom f & for i st i in dom it holds it.i = 1.(K,f.i); end; theorem :: MATRIXJ1:56 Len 1.(K,f) = f & Width 1.(K,f) = f; theorem :: MATRIXJ1:57 for i be Element of NAT holds 1.(K,<*i*>) = <*1.(K,i)*>; theorem :: MATRIXJ1:58 1.(K,f^g) = 1.(K,f)^1.(K,g); theorem :: MATRIXJ1:59 1.(K,f|n) = 1.(K,f) |n; theorem :: MATRIXJ1:60 block_diagonal(<*1.(K,i),1.(K,j)*>,0.K)=1.(K,i+j); theorem :: MATRIXJ1:61 block_diagonal(1.(K,f),0.K) = 1.(K,Sum f); reserve p,p1 for FinSequence of K; begin :: Operations On a Finite Sequence of Matrices definition let K,G,p; func mlt(p,G) -> FinSequence_of_Matrix of K means :: MATRIXJ1:def 9 dom it = dom G & for i st i in dom it holds it.i = p/.i * G.i; end; registration let K; let R,p; cluster mlt(p,R) -> Square-Matrix-yielding; end; theorem :: MATRIXJ1:62 Len mlt(p,G) = Len G & Width mlt(p,G) = Width G; theorem :: MATRIXJ1:63 mlt(p,<*A*>)=<*p/.1*A*>; theorem :: MATRIXJ1:64 len G = len p & len G1 <=len p1 implies mlt(p^p1,G^G1) = mlt(p,G )^mlt(p1,G1) ; theorem :: MATRIXJ1:65 a*block_diagonal(G,a1) = block_diagonal(mlt(len G|->a,G),a*a1); definition let K; let G1,G2 be FinSequence_of_Matrix of K; func G1(+)G2 -> FinSequence_of_Matrix of K means :: MATRIXJ1:def 10 dom it = dom G1 & for i st i in dom it holds it.i= G1.i + G2.i; end; registration let K; let R,G; cluster R(+)G -> Square-Matrix-yielding; end; theorem :: MATRIXJ1:66 Len (G1(+)G2) = Len G1 & Width (G1(+)G2) = Width G1; theorem :: MATRIXJ1:67 len G = len G9 implies (G^G1)(+)(G9^G2) = (G(+)G9)^(G1(+)G2); theorem :: MATRIXJ1:68 <*A*>(+)G = <*A + G.1*>; theorem :: MATRIXJ1:69 <*A1*>(+)<*A2*> = <* A1+A2 *>; theorem :: MATRIXJ1:70 <*A1,B1*>(+)<*A2,B2*> = <*A1+A2,B1+B2*>; theorem :: MATRIXJ1:71 len A1 = len B1 & len A2 = len B2 & width A1 = width B1 & width A2 = width B2 implies block_diagonal(<*A1,A2*>,a1) + block_diagonal(<*B1,B2*>, a2) = block_diagonal(<*A1,A2*>(+)<*B1,B2*>,a1+a2); theorem :: MATRIXJ1:72 Len R1 = Len R2 & Width R1 = Width R2 implies block_diagonal(R1,a1) + block_diagonal(R2,a2) = block_diagonal(R1(+)R2,a1+a2); definition let K; let G1,G2 be FinSequence_of_Matrix of K; func G1(#)G2 -> FinSequence_of_Matrix of K means :: MATRIXJ1:def 11 dom it = dom G1 & for i st i in dom it holds it.i= G1.i * G2.i; end; theorem :: MATRIXJ1:73 Width G1 = Len G2 implies Len (G1(#)G2) = Len G1 & Width (G1(#) G2) = Width G2; theorem :: MATRIXJ1:74 len G = len G9 implies (G^G1)(#)(G9^G2) = (G(#)G9)^(G1(#)G2); theorem :: MATRIXJ1:75 <*A*>(#)G = <*A * G.1*>; theorem :: MATRIXJ1:76 <*A1*>(#)<*A2*> = <* A1*A2 *>; theorem :: MATRIXJ1:77 <*A1,B1*>(#)<*A2,B2*> = <*A1*A2,B1*B2*>; theorem :: MATRIXJ1:78 width A1 = len B1 & width A2 = len B2 implies block_diagonal(<* A1,A2*>,0.K)*block_diagonal(<*B1,B2*>,0.K) = block_diagonal(<*A1,A2*>(#)(<*B1, B2*>),0.K); theorem :: MATRIXJ1:79 Width R1 = Len R2 implies block_diagonal(R1,0.K)*block_diagonal(R2,0.K )= block_diagonal(R1(#)R2,0.K);