|
% --------------------------------------------------------------
% 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 is the top level file of a linear algebra library for PVS.
%
%
% --------------------------------------------------------------
% This file is a single component of a library of linear
% algebra theories. The NASA vector libraries are used.
%
% ---------------------------------------------------------------
% --------------------------------------------------------------
% 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
%
%-------------------------------------------------------------------
%-------------------------------------------------------------------
% This theory introduces and defines properties of the summation of
% vector valued functions, F: T -> Rn
%
% high
% ----
% (SigmaV(low, high, F))(i) = \ (F(j))(i)
% /
% ----
% j = low
%
%------------------------------------------------------------------
sigma_vector[T: type from int,n: posnat]: THEORY
BEGIN
ASSUMING
connected_domain: ASSUMPTION (FORALL (x, y: T), (z: integer):
x <= z AND z <= y IMPLIES T_pred(z))
ENDASSUMING
IMPORTING linear_map
F: VAR FUNCTION [T -> Vector[n]]
d: VAR FUNCTION [T -> real]
low: VAR T_low[T]
high: VAR T_high[T]
a: VAR real
%--------------------------------------------------------------------------------------------
% Defines the vector given by the summation of a vector valued function over a given range
% -------------------------------------------------------------------------------------------
SigmaV(low,high,F): Vector[n] = (lambda(i: below[n]): sigma(low,high,lambda(j: T): F(j)(i)));
%---------------------------------------------------------------------------
% Defines multiplication of a scalar real by a vector valued function
% --------------------------------------------------------------------------
*: [real,function[T -> Vector[n]] -> function[T -> Vector[n]]] = LAMBDA(a,F): LAMBDA(i: T): a*F(i);
% --------------------------------------------------------------------------
% Defines the multiplication of a vector by a vector valued function
% --------------------------------------------------------------------------
*: [function[T -> real],function[T -> Vector[n]] -> function[T -> Vector[n]]] = LAMBDA(d,F): LAMBDA(i: T): d(i)*F(i);
% --------------------------------------------------------------------------
% Defines the compositon of a map and a vector valued function.
% --------------------------------------------------------------------------
o: [Map(n,n),function[T -> Vector[n]] -> function[T -> Vector[n]]] = LAMBDA(h: Map(n,n),F): LAMBDA(i: T): h`mp(F(i));
%---------------------------------------------------------------------------
% This lemma allow us to isolate the last term of the sum
%---------------------------------------------------------------------------
SigmaV_last: THEOREM high >= low IMPLIES SigmaV(low, high, F) = SigmaV(low, high-1, F) + F(high);
%---------------------------------------------------------------------------
% This lemma allow us to extract an scalar from the sum
%---------------------------------------------------------------------------
SigmaV_scal: LEMMA FORALL (a: real, m,p: T,F: [T -> Vector[n]]): SigmaV(p,m,a*F) = a*SigmaV(p,m,F)
END sigma_vector
¤ Dauer der Verarbeitung: 0.1 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.
|
