Quelle sigma_vector.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 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

quality82%

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