:: Laplace Expansion
:: by Karol P\c{a}k and Andrzej Trybulec
::
:: Received August 13, 2007
:: Copyright (c) 2007-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, SUBSET_1, NAT_1, XBOOLE_0, MATRIX11, FINSEQ_1, ARYTM_3,
VECTSP_1, MATRIX_1, RELAT_1, FINSEQ_3, ARYTM_1, TREES_1, CARD_1,
XXREAL_0, FUNCT_1, INCSP_1, TARSKI, ALGSTR_0, ZFMISC_1, STRUCT_0,
REALSET1, SETWOP_2, FUNCT_2, FINSUB_1, GROUP_1, SETWISEO, INT_1,
FINSET_1, ABIAN, FINSEQ_2, BINOP_1, QC_LANG1, AFINSQ_1, ABSVALUE,
MATRIX_3, SUPINF_2, CARD_3, FINSOP_1, RVSUM_1, FVSUM_1, MESFUNC1,
MATRIX_6, LAPLACE, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, FINSET_1, RELAT_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2,
FINSEQ_1, BINOP_1, STRUCT_0, ALGSTR_0, GROUP_1, VECTSP_1, SETWISEO,
SETWOP_2, FINSEQ_2, MATRIX_0, FINSUB_1, MATRIX_1, NAT_1, FVSUM_1,
FINSOP_1, MATRIX_3, CARD_1, FINSEQ_7, NEWTON, MATRIX_7, FINSEQ_3,
MATRIX11, MATRIX_6, NAT_D;
constructors SETWISEO, FINSOP_1, SETWOP_2, ALGSTR_1, FVSUM_1, BINOP_1,
FINSEQ_4, FINSEQ_7, WELLORD2, NEWTON, MATRIX_6, MATRIX_7, MATRIX11,
NAT_D, BINOP_2, RELSET_1, XXREAL_0, NAT_1, VECTSP_2;
registrations FUNCT_1, FINSUB_1, FINSET_1, STRUCT_0, FVSUM_1, MATRIX_1,
VECTSP_1, FUNCT_2, PARTFUN1, XBOOLE_0, ORDINAL1, XXREAL_0, NAT_1, INT_1,
RELAT_1, CARD_1, MATRIX11, XCMPLX_0, RELSET_1, FINSEQ_2, FINSEQ_1,
MATRIX_0, MATRIX_6, VECTSP_2;
requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
begin :: Preliminaries
reserve x,y for object,
N for Element of NAT,
c,i,j,k,m,n for Nat,
D for non empty set,
s for Element of 2Set Seg (n+2),
p for Element of Permutations(n) ,
p1, q1 for Element of Permutations(n+1),
p2 for Element of Permutations(n +2),
K for Field,
a for Element of K,
f for FinSequence of K,
A for (Matrix of K),
AD for Matrix of n,m,D,
pD for FinSequence of D,
M for Matrix of n,K;
theorem :: LAPLACE:1
for f be FinSequence, i be Nat st i in dom f holds len Del(f,i) = len f -' 1;
theorem :: LAPLACE:2
for i,j,n being Nat, M being Matrix of n,K st i in dom M holds
len Deleting(M,i,j) = n-'1;
theorem :: LAPLACE:3
j in Seg width A implies width DelCol(A,j) = width A-'1;
theorem :: LAPLACE:4
for i be Nat st len A > 1 holds width A = width DelLine(A,i);
theorem :: LAPLACE:5
for i being Nat st j in Seg width M holds width Deleting(M,i,j) = n-' 1;
definition
let G be non empty multMagma;
let B be Function of [:the carrier of G,NAT:], the carrier of G;
let g be Element of G, i be Nat;
redefine func B.(g,i) -> Element of G;
end;
theorem :: LAPLACE:6
card Permutations n = n!;
theorem :: LAPLACE:7
for i,j st i in Seg (n+1) & j in Seg (n+1) holds card {p1: p1.i = j} = n!;
theorem :: LAPLACE:8
for K be Fanoian Field for p2 for X,Y be Element of Fin 2Set Seg
(n+2) st Y={s:s in X & Part_sgn(p2,K).s = -1_K} holds (the multF of K) $$ (X,
Part_sgn(p2,K)) = power(K).(-1_K,card Y);
theorem :: LAPLACE:9
for K be Fanoian Field for p2,i,j st i in Seg (n+2) & p2.i=j ex X
be Element of Fin 2Set Seg (n+2) st
X = {{N,i} where N is Nat : {N,i} in 2Set Seg (n+2)} & (
the multF of K) $$ (X,Part_sgn(p2,K)) = power(K).(-1_K,i+j);
theorem :: LAPLACE:10
for i,j st i in Seg (n+1) & n >= 2 ex Proj be Function of 2Set
Seg n, 2Set Seg(n+1)
st rng Proj = 2Set Seg(n+1)\{{N,i} where N is Nat:{N,i} in 2Set Seg(n+1)}
& Proj is one-to-one & for k,m st k= i & k < i implies Proj.{k,m} = {k,m+1} )
& (m >= i & k >= i implies Proj.{k,m} = {k+1,m+1});
theorem :: LAPLACE:11
n < 2 implies for p be Element of Permutations n holds p is even & p=idseq n;
theorem :: LAPLACE:12
for X,Y,D be non empty set for f be Function of X,Fin Y, g be
Function of Fin Y,D, F be BinOp of D st (for A,B be Element of Fin Y st A
misses B holds F.(g.A,g.B) = g.(A \/ B)) & F is commutative associative & F is
having_a_unity & g.{} = the_unity_wrt F for I be Element of Fin X st for x,y st
x in I & y in I & f.x meets f.y holds x = y holds F $$ (I,g*f) = F $$ (f.:I,g)
& F $$ (f.:I,g) = g.union (f.:I) & union (f.:I) is Element of Fin Y;
begin :: Auxiliary notions
definition
let i,j,n be Nat;
let K;
let M be Matrix of n,K;
assume that
i in Seg n and
j in Seg n;
func Delete(M,i,j) -> Matrix of n-'1,K equals
:: LAPLACE:def 1
Deleting(M,i,j);
end;
theorem :: LAPLACE:13
for i,j st i in Seg n & j in Seg n for k,m st k in Seg (n-'1) &
m in Seg (n-'1) holds (k < i & m < j implies Delete(M,i,j)*(k,m) = M*(k,m) )& (
k < i & m >= j implies Delete(M,i,j)*(k,m) = M*(k,m+1) )& (k >= i & m < j
implies Delete(M,i,j)*(k,m) = M*(k+1,m) )& (k >= i & m >= j implies Delete(M,i,
j)*(k,m) = M*(k+1,m+1));
theorem :: LAPLACE:14
for i,j st i in Seg n & j in Seg n holds Delete(M,i,j)@ = Delete (M@,j,i);
theorem :: LAPLACE:15
for f be FinSequence of K, i,j st i in Seg n & j in Seg n holds
Delete(M,i,j) = Delete(RLine(M,i,f),i,j);
definition
let c, n, m, D;
let M be Matrix of n,m,D;
let pD be FinSequence of D;
func ReplaceCol(M,c,pD) -> Matrix of n,m,D means
:: LAPLACE:def 2
len it = len M &
width it = width M & for i,j st [i,j] in Indices M holds (j <> c implies it*(i,
j) = M*(i,j)) & (j = c implies it*(i,c) = pD.i) if len pD = len M otherwise it
= M;
end;
notation
let c, n, m, D;
let M be Matrix of n,m,D;
let pD be FinSequence of D;
synonym RCol(M,c,pD) for ReplaceCol(M,c,pD);
end;
theorem :: LAPLACE:16
for i st i in Seg width AD holds (i = c & len pD = len AD implies Col(
RCol(AD,c,pD),i) = pD) & (i <> c implies Col(RCol(AD,c,pD),i) = Col(AD,i));
theorem :: LAPLACE:17
not c in Seg width AD implies RCol(AD,c,pD) = AD;
theorem :: LAPLACE:18
RCol(AD,c,Col(AD,c)) = AD;
theorem :: LAPLACE:19
for A be Matrix of n,m,D, A9 be Matrix of m,n,D st A9 = A@ & (m=
0 implies n=0) holds ReplaceCol(A,c,pD) = ReplaceLine(A9,c,pD)@;
begin :: Permutations
definition
let i,n;
let perm be Element of Permutations(n+1);
assume
i in Seg (n+1);
func Rem(perm,i) -> Element of Permutations n means
:: LAPLACE:def 3
for k st k in Seg
n holds (k*= perm.
i implies it.k = perm.k-1) )& (k>=i implies (perm.(k+1) < perm.i implies it.k =
perm.(k+1) )& (perm.(k+1) >= perm.i implies it.k = perm.(k+1)-1));
end;
theorem :: LAPLACE:20
for i,j st i in Seg (n+1) & j in Seg(n+1) for P be set st P = { p1: p1
.i = j} ex Proj be Function of P,Permutations n st Proj is bijective & for
q1 st q1.i = j holds Proj.q1 = Rem(q1,i);
theorem :: LAPLACE:21
for i,j st i in Seg (n+1) & p1.i = j holds -(a,p1) = power(K).(-
1_K,i+j) * -(a,Rem(p1,i));
theorem :: LAPLACE:22
for i,j st i in Seg (n+1) & p1.i = j for M be Matrix of n+1,K
for DM be Matrix of n,K st DM = Delete(M,i,j) holds (Path_product M).p1 = power
(K).(-1_K,i+j)*(M*(i,j))*(Path_product(DM)).Rem(p1,i);
begin :: Minors & cofactors
definition
let i,j,n be Nat;
let K;
let M be Matrix of n,K;
func Minor(M,i,j) -> Element of K equals
:: LAPLACE:def 4
Det Delete(M,i,j);
end;
definition
let i,j,n be Nat;
let K;
let M be Matrix of n,K;
func Cofactor(M,i,j) -> Element of K equals
:: LAPLACE:def 5
power(K).(-1_K,i+j)*Minor(M,i,j);
end;
theorem :: LAPLACE:23
for i,j st i in Seg n & j in Seg n for P be Element of Fin
Permutations n st P = {p:p.i = j} for M be Matrix of n,K holds (the addF of K)
$$ (P,Path_product(M)) = M*(i,j)*Cofactor(M,i,j);
theorem :: LAPLACE:24
for i,j st i in Seg n & j in Seg n holds Minor(M,i,j) = Minor(M@ ,j,i);
definition
let n,K;
let M be Matrix of n,K;
func Matrix_of_Cofactor(M) -> Matrix of n,K means
:: LAPLACE:def 6
for i,j being Nat st [i,j] in Indices it holds it*(i,j) = Cofactor(M,i,j);
end;
begin :: Laplace expansion
definition
let n,i,K;
let M be Matrix of n,K;
::$N Laplace expansion
func LaplaceExpL(M,i) -> FinSequence of K means
:: LAPLACE:def 7
len it = n & for j st j in dom it holds it.j = M*(i,j)*Cofactor(M,i,j);
end;
definition
let n;
let j be Nat,K;
let M be Matrix of n,K;
func LaplaceExpC(M,j) -> FinSequence of K means
:: LAPLACE:def 8
len it = n & for i st i in dom it holds it.i = M*(i,j)*Cofactor(M,i,j);
end;
theorem :: LAPLACE:25
for i be Nat, M be Matrix of n,K st i in Seg n holds Det M = Sum
LaplaceExpL(M,i);
theorem :: LAPLACE:26
for i st i in Seg n holds LaplaceExpC(M,i) = LaplaceExpL(M@,i);
theorem :: LAPLACE:27
for j be Nat, M be Matrix of n,K st j in Seg n holds Det M = Sum
LaplaceExpC(M,j);
theorem :: LAPLACE:28
for p,i st len f=n & i in Seg n holds mlt(Line(
Matrix_of_Cofactor M,i),f) = LaplaceExpL(RLine(M,i,f),i);
theorem :: LAPLACE:29
i in Seg n implies Line(M,j) "*" Col((Matrix_of_Cofactor M)@,i)
= Det RLine(M,i,Line(M,j));
theorem :: LAPLACE:30
Det M <> 0.K implies M * ((Det M)" * (Matrix_of_Cofactor M)@) = 1.(K,n);
theorem :: LAPLACE:31
for f,i st len f=n & i in Seg n holds mlt(Col(Matrix_of_Cofactor
M,i),f) = LaplaceExpL(RLine(M@,i,f),i);
theorem :: LAPLACE:32
i in Seg n & j in Seg n implies Line((Matrix_of_Cofactor M)@,i)
"*" Col(M,j) = Det RLine(M@,i,Line(M@,j));
theorem :: LAPLACE:33
Det M <> 0.K implies ((Det M)" * (Matrix_of_Cofactor M)@) * M = 1.(K,n);
theorem :: LAPLACE:34
M is invertible iff Det M <> 0.K;
theorem :: LAPLACE:35
Det M <> 0.K implies M~ = (Det M)" * (Matrix_of_Cofactor M)@;
theorem :: LAPLACE:36
for M be Matrix of n,K st M is invertible for i,j st [i,j] in Indices
(M~) holds M~*(i,j) = (Det M)" * power(K).(-1_K,i+j) * Minor(M,j,i);
theorem :: LAPLACE:37
for A be Matrix of n,K st Det A <> 0.K for x,b be Matrix of K st
len x = n & A * x = b holds x = A~ * b & for i,j st [i,j] in Indices x holds x*
(i,j) = (Det A)" * Det ReplaceCol(A,i,Col(b,j));
theorem :: LAPLACE:38
for A be Matrix of n,K st Det A <> 0.K for x,b be Matrix of K st
width x = n & x * A = b holds x = b * A~ & for i,j st [i,j] in Indices x holds
x*(i,j) = (Det A)" * Det ReplaceLine(A,j,Line(b,i));
begin :: Product by a vector
definition
let D be non empty set;
let f be FinSequence of D;
redefine func <*f*> -> Matrix of 1,len f,D;
end;
definition
let K;
let M be Matrix of K;
let f be FinSequence of K;
func M * f -> Matrix of K equals
:: LAPLACE:def 9
M * (<*f*>@);
func f * M -> Matrix of K equals
:: LAPLACE:def 10
<*f*> * M;
end;
theorem :: LAPLACE:39
for A be Matrix of n,K st Det A <> 0.K for x,b be FinSequence of K st
len x = n & A * x = <*b*>@ holds <*x*>@ = A~ * b & for i st i in Seg n holds x.
i = (Det A)" * Det ReplaceCol(A,i,b);
::$N Cramer's Rule
theorem :: LAPLACE:40
for A be Matrix of n,K st Det A <> 0.K for x,b be FinSequence of K st
len x = n & x * A = <*b*> holds <*x*> = b * A~ & for i st i in Seg n holds x.i
= (Det A)" * Det ReplaceLine(A,i,b);
*