|
% --------------------------------------------------------------
% 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
% ---------------------------------------------------------------
% This PVS theory defines a linear map on vector spaces. See [SA] Chapter 3 and
% Chapter 2 of [FIS] for an a detailed account of the concepts.
%
% --------------------------------------------------------------
% 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
%
%-------------------------------------------------------------
linear_map_def: theory
BEGIN
IMPORTING sigma_vector,sigma_lemmas
f,g,h,k: VAR Maping
n,m,l,p: VAR posnat
% -------------------------------------------------------------------------------
% We define a base of an n-dimensionan vector space as a set of n vector which
% are unitary, orthogonal and which generate the whole vector space
% -------------------------------------------------------------------------------
unit?(n)(e: [below[n] -> Vector[n]]): bool = FORALL (i: below[n]): e(i)*e(i)=1
ortho?(n)(e: [below[n] -> Vector[n]]): bool = FORALL (i,j: below[n]): (i /= j IMPLIES e(i)*e(j)=0)
vec_expan?(n)(e: [below[n] -> Vector[n]]): bool = FORALL (x: Vector[n]): x = SigmaV(0,n-1,x*e)
base?(n)(e: [below[n] -> Vector[n]]): bool = unit?(n)(e) and ortho?(n)(e) and vec_expan?(n)(e)
% -------------------------------------------------------------------------------
% We now define the base of an n-dimensional vector space as the "standard
% base", that is, each ith element of the base is a row of 0s with the exception
% that the ith entry is 1.
% So base e(i)(i) = 1 and e(i)(j) =0 if i /= j.
%
% We also prove that this is indeed a base, according to the previous definition.
% In order to do this we use the lemma which states that a vector can be
% represented as a combination of itself and the "standar base"
% -------------------------------------------------------------------------------
e(n): [below[n]->Vector[n]] = LAMBDA(j: below[n]): LAMBDA(i: below[n]): IF (i=j) THEN 1 ELSE 0 ENDIF
vec_repre_bases: LEMMA FORALL (x: Vector[n]): x = SigmaV(0,n-1,x*e(n))
cano_base:LEMMA base?(n)(e(n))
%---------------------------------------------------------------------------
% Definition of linear maps, which is given with two different notations
%---------------------------------------------------------------------------
linear_map_e?(h,l,n,m): bool = h`dom = n and h`codom = m and FORALL (x: Vector[l],F: [below[l]->Vector[n]]):
h`mp(SigmaV[below[l],n](0,l-1,x*F)) = SigmaV[below[l],m](0,l - 1,x*(h`mp o F));
linear_map_e?(n,m)(h): bool = FORALL (l): linear_map_e?(h,l,n,m)
Map_linear(n,m): TYPE = {h: Map(n,m) | linear_map_e?(n,m)(h)}
% -------------------------------------------------------------------------------------------
% If f and g are linear maps, then their compositon is a linear map.
% -------------------------------------------------------------------------------------------
linear_map_e_comp: LEMMA FORALL (f: Map(m,p),g: Map(n,m)): linear_map_e?(m,p)(f) AND linear_map_e?(n,m)(g)
IMPLIES linear_map_e?(n,p)(f o g)
% --------------------------------------------------------------------------
% If functions k and j are equal and h is bijective, then k is bijective.
% --------------------------------------------------------------------------
bijecti_fun_equa: LEMMA FORALL (k,h:Map(n,n)):k=h AND bijective?(n)(h)
IMPLIES
bijective?(n)(k)
% --------------------------------------------------------------------------
% If two linear maps, h and k, coincide when applying them to the standard
% base, the maps are equal
% --------------------------------------------------------------------------
equa_basis_n: LEMMA FORALL (h,k: Map_linear(n,m)): h`mp o e(n) = k`mp o e(n)
IMPLIES h = k
%------------------------------------------------------------
% Classic linear map definition
%------------------------------------------------------------
additive?(f): bool = FORALL (x,y: Vector[f`dom]): f`mp(x + y) = f`mp(x) + f`mp(y)
homogeneous?(f): bool = FORALL (a: real, x: Vector[f`dom]): f`mp(a*x) = a*f`mp(x)
linear_map?(f): bool = additive?(f) AND homogeneous?(f);
%------------------------------------------------------------
% Equivalence between the two linear map definitions
%------------------------------------------------------------
linear_map_characterization: LEMMA FORALL (f: Map(n,n)): linear_map?(f) IFF linear_map_e?(n,n)(f);
end linear_map_def
¤ Dauer der Verarbeitung: 0.19 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.
|
