Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/linear_algebra/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 11 kB

Quelle matrix_operator.pvs Sprache: PVS

% --------------------------------------------------------------
% 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

quality85%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.