|
% --------------------------------------------------------------
% Linear Algebra library
% Heber Herencia-Zapana NIA
% Gilberto Pérez University of Coruña Spain
% Pablo Ascariz University of Coruña Spain
% Felicidad Aguado University of Coruña Spain
% Date: December, 2013
% ---------------------------------------------------------------
%
% File Contents
%-----------------------------------------------------------------------------
% This theory gives a one to one relation between maps and matrices
% The inverse of a matrix is defined using the inverse of the associated map
% This theory gives basic properties of the inverse of a matrix
%
% ----------------------------------------------------------------------------
% This file is a single component of a library of linear
% algebra theories.
% ---------------------------------------------------------------------------
% For the most part, we follow the treatmet in the following texts
%
% [FIS] Linear Algebra, S. Friedburg, A. Insel, and L. Spense, 3rd edition, Prentice-Hall.
%
% [SA] Linear Algebra Done Right, S. Axler. 2nd Edition. Springer-Verlag.
%
% [D] Topology, J. Dungundji, Allen and Bacon Co.
%
% [K] Introductory Functional Analysis, Kreysizg, Wiley.
%
% [R] Convex Analysis, R. Rockafellar, Princeton University Press.
%
% [J] A Lecture or the S-Procedure, U. Jonsson.
%
% --------------------------------------------------------------
matrix_operator: theory
BEGIN
IMPORTING matrices,linear_map_def
A,B: VAR Matrix
M:VAR Square
n,m,l,p: VAR posnat
% ------------------------------------------------------------------------------------------
% Preliminary lemmas
% ------------------------------------------------------------------------------------------
% Given a linear bijective map, its inverse is also linear
linear_inverse_map_n: LEMMA FORALL (f: Map_linear(n,n)): bijective?(n)(f) IMPLIES linear_map_e?(n,n)(inverse(n)(f))
% The composition of linear maps is also linear
linear_comp: LEMMA FORALL (n,m,l: posnat,g: Map_linear(n,m),f: Map_linear(m,l)):
linear_map_e?(n,l)(f o g)
linear_matrix: LEMMA FORALL (A: Mat(n,m),F: [below[l] -> [Vector[m]]]): A*SigmaV(0,l-1,F) = SigmaV(0,l-1,lambda(i: below[l]):A*F(i))
% The inverse of a map is unique
equa_inv:LEMMA FORALL(f,g,h: Map(n,n)):(f o g)`mp = id(n)`mp and (h o f)`mp = id(n)`mp
IMPLIES
bijective?(n)(f)
inv_uni:LEMMA FORALL(f,g,h: Map(n,n)): (f o g)`mp = id(n)`mp and (h o f)`mp = id(n)`mp
IMPLIES
inverse(n)(f) = g and inverse(n)(f) = h
% ------------------------------------------------------------------------------------------
% Defines an operator L which associates a Matrix to a linear map f,
% See pg 74[FIS].
% ------------------------------------------------------------------------------------------
L(n,m): [Map_linear(n,m) -> Mat(m,n)] = (lambda(f: Map_linear(n,m)):
(#rows:= m,cols:= n,matrix:= lambda(j: below[m],i: below[n]): f`mp(e(n)(i))(j)#))
% -------------------------------------------------------------------------------------------
% Defines a operator T that given an n x n square matrix A produces a linear map on the n
% dimensional vector space.
% -------------------------------------------------------------------------------------------
T(n,m): [Mat(m,n) -> Map_linear(n,m)]=(lambda(A: Mat(m,n)): (#dom:= n,codom:= m,mp:= lambda(x: Vector[n]): lambda(j: below[m]):
sigma(0,A`cols-1,lambda(i: below[A`cols]): A`matrix(j,i)*x(i))#))
% -------------------------------------------------------------------------------------------
% The operator T is just multiplying by the matrix
% -------------------------------------------------------------------------------------------
T_matr: LEMMA FORALL (A: Mat(m,n),x: Vector[n]): (T(n,m)(A))`mp(x) = A*x;
% -------------------------------------------------------------------------------------------
% The map produced by T is a linear map.
% -------------------------------------------------------------------------------------------
linear_map_T: LEMMA FORALL (A: Mat(m,n)): linear_map_e?(n,m)(T(n,m)(A));
% -------------------------------------------------------------------------------------------
% There is bijection between L and T.
% -------------------------------------------------------------------------------------------
map_matrix_bij: LEMMA FORALL (A: Mat(m,n)): L(n,m)(T(n,m)(A)) = A
% -------------------------------------------------------------------------------------------
% If f and g are equal, then the matrices produced by applying L to them are also
% equal.
% -------------------------------------------------------------------------------------------
operator: LEMMA FORALL (f,g: Map_linear(n,m)): f = g
IMPLIES
L(f`dom,f`codom)(f) = L(g`dom,g`codom)(g)
% -------------------------------------------------------------------------------------------
% The operator L is bijective
% -------------------------------------------------------------------------------------------
Iso: LEMMA bijective?(L(n,m))
% -------------------------------------------------------------------------------------------
% Given a linear map f, applying L and then T yields f
% -------------------------------------------------------------------------------------------
iso_map: LEMMA FORALL (f: Map_linear(n,m)):
T(n,m)(L(n,m)(f)) = f
% -------------------------------------------------------------------------------------------
% The inverse of L is T
% -------------------------------------------------------------------------------------------
L_inverse: LEMMA inverse(L(n,m)) = T(n,m)
% -------------------------------------------------------------------------------------------
% The operator T is bijective
% -------------------------------------------------------------------------------------------
Iso_T : LEMMA bijective?(T(n,m))
% -------------------------------------------------------------------------------------------
% T takes products of matrices to compositions of maps.
% L takes compositions of maps to products of matrices
% -------------------------------------------------------------------------------------------
mult_comp: LEMMA FORALL (A: Mat(p,m),B: Mat(m,n)): T(n,p)(A*B) = T(m,p)(A) o T(n,m)(B)
comp_mult: LEMMA FORALL (g: Map_linear(n,m),f: Map_linear(m,p)):
L(n,p)(f o g) = L(m,p)(f)*L(n,m)(g)
% -------------------------------------------------------------------------------------------
% Applying L to the indetiy map yields the identiy matrix.
% Applying T to the idenity matrix yields the identity map
% -------------------------------------------------------------------------------------------
iso_ide_L: LEMMA L(n,n)(id(n)) = I(n)
iso_ide_T: LEMMA T(n,n)(I(n)) = id(n)
% -------------------------------------------------------------------------------------------
% Defines the set of all square matrices where the T operator applied to them is bijective.
% These will be the set of invertible matrices
% -------------------------------------------------------------------------------------------
Matrix_inv(n):type= {A: Square | squareMat?(n)(A) and bijective?(n)(T(n,n)(A))}
% -------------------------------------------------------------------------------------------
% Defines the inverse of an invertable matrix A by applying L to the inverse of the
% map produced by T(A). See page 94 of [FIS]
% -------------------------------------------------------------------------------------------
inverse_invertible: LEMMA
square?(A) AND
squareMat?(n)(A) AND
bijective?(n)(T(n,n)(A))
IMPLIES
squareMat?(n)(L(n, n)(inverse(n)(T(n, n)(A)))) AND
bijective?(n)(T(n, n)(L(n, n)(inverse(n)(T(n, n)(A)))))
% Definition of the inverse matrix
inv(n): [Matrix_inv(n) -> Matrix_inv(n)] = (lambda (A: Matrix_inv(n)): L(n,n)(inverse(n)(T(n,n)(A))))
% -------------------------------------------------------------------------------------------
% The product of the inverse of a matrix A and A is the identity matrix.
% See Page 94 of [FIS]
% -------------------------------------------------------------------------------------------
iso_inv: LEMMA squareMat?(n)(M) AND bijective?(n)(T(n,n)(M))
IMPLIES
inv(n)(M)*M = I(n) AND M*inv(n)(M) = I(n)
% -------------------------------------------------------------------------------------------
% The matrix given by "inv" is in fact the inverse
% -------------------------------------------------------------------------------------------
inv: LEMMA squareMat?(n)(M) AND
bijective?(n)(T(n,n)(M))
IMPLIES
inverse?(M)(inv(n)(M))
% Technical lemma
bijec_prod: LEMMA square?(A) AND squareMat?(n)(A) AND bijective?(n)(T(n,n)(A)) AND
square?(M) AND squareMat?(n)(M) AND bijective?(n)(T(n,n)(M))
IMPLIES
bijective?(n)(T(n,n)(A*M))
%--------------------------------------------------------------------------------------------
% The operator T commutes with the inverse
%--------------------------------------------------------------------------------------------
map_matrix_bij_inv: LEMMA FORALL (A: Matrix_inv(n)): inverse(n)(T(n,n)(A)) = T(n,n)(inv(n)(A))
% Technical lemma
tran_inv: LEMMA square?(A) and squareMat?(n)(A) and bijective?(n)(T(n,n)(A))
IMPLIES
inverse?(transpose(A))(transpose(inv(n)(A)))
%----------------------------------------------------------------------------------------------
% The inverse of a transpose matrix is the transpose of the inverse matrix
%----------------------------------------------------------------------------------------------
bijec_transpose: LEMMA square?(A) AND squareMat?(n)(A) AND
bijective?(n)(T(n,n)(A))
IMPLIES
bijective?(n)(T(n,n)(transpose(A)))
tran_inv_oper: LEMMA square?(A) and squareMat?(n)(A) and bijective?(n)(T(n,n)(A))
IMPLIES
inv(n)(transpose(A))=transpose(inv(n)(A))
%----------------------------------------------------------------------------------------------
% The inverse of a product of matrices, is the product of the inverses (in the opposite order)
%----------------------------------------------------------------------------------------------
prod_inv:LEMMA square?(A) and squareMat?(n)(A) and bijective?(n)(T(n,n)(A)) AND
square?(B) and squareMat?(n)(B) and bijective?(n)(T(n,n)(B))
IMPLIES
inverse?(A*B)(inv(n)(B)*inv(n)(A))
prod_inv_oper:LEMMA square?(A) and squareMat?(n)(A) and bijective?(n)(T(n,n)(A)) AND
square?(B) and squareMat?(n)(B) and bijective?(n)(T(n,n)(B))
IMPLIES
inv(n)(A*B)=inv(n)(B)*inv(n)(A)
% Technical lemma, to prove the ellipsoid theorem
equa_sol: LEMMA FORALL(x,y,b:Vector[n]): square?(M) AND
squareMat?(n)(M) and
y=M*x+b and
bijective?(n)(T(n,n)(M))
IMPLIES
x=inv(n)(M)*(y-b)
end matrix_operator
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
