|
% --------------------------------------------------------------
% 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 theory defines the map operator.
%
% --------------------------------------------------------------
% 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: theory
BEGIN
IMPORTING vectors@vectors
n,m :VAR posnat
%------------------------------------------------------------------------
% A map from an n dimensional vector space to an m dimensional vector
% space takes a n-dimensional vector to an m-dimensional vector.
% It is defined as a record given by: the dimension of the domain, the
% dimension of the codomain, and the function from the domain to the
% codomain
%------------------------------------------------------------------------
Maping: TYPE = [#dom: posnat,codom: posnat,mp: [Vector[dom]->Vector[codom]]#]
Map(n,m): TYPE = {f: Maping | f`dom = n and f`codom = m}
%-----------------------------------------------------------------------------
% Next we define operations with mappings.
% same_dim? and same? provide the restrictions relating to the domain and
% codomain which allow us to define the sum and the composition, respectively
%-----------------------------------------------------------------------------
same_dim?(f: Maping)(g: Maping):bool = f`dom = g`dom and f`codom = g`codom;
same?(f: Maping)(g: Maping): bool = f`dom = g`codom;
+(f: Maping,(g: (same_dim?(f)))): Maping = f WITH [`mp:= lambda(x: Vector[f`dom]): f`mp(x) + g`mp(x)];
*(a: real, f: Maping): Maping = f WITH [`mp:= lambda(x: Vector[f`dom]): a*f`mp(x)];
o(f: Maping,(g: (same?(f)))): Maping = (#dom:= g`dom,codom:= f`codom,mp:= f`mp o g`mp#)
%------------------------------------------------------------------------------------
% Finally we define the concepts of bijective map and inverse mapping, which are
% given through the same definitions relating to functions, and we also define
% the identity mapping
%------------------------------------------------------------------------------------
bijective?(n)(f: Map(n,n)): bool = bijective?[Vector[n],Vector[n]](f`mp);
inverse(n)(f: Map(n,n)): Maping = (#dom:= n,codom:= n,mp:= inverse[Vector[n],Vector[n]](f`mp)#)
id(n): Maping = (#dom:= n,codom:= n,mp:= lambda(x: Vector[n]): x#)
end linear_map
¤ Dauer der Verarbeitung: 0.16 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.
|
