Quelle linear_map_def.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
% ---------------------------------------------------------------
% 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

quality96%

¤ Dauer der Verarbeitung: 0.17 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.