Quelle matrix_lemmas.pvs Sprache: PVS

matrix_lemmas: THEORY

% 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

BEGIN

IMPORTING matrix_operator

%--------------------------------------------------------------------------------------
%--------------------------------------------------------------------------------------
% Matrix Lemmas
%--------------------------------------------------------------------------------------
%--------------------------------------------------------------------------------------

%--------------------------------------------------------------------------------------
% Multiplying a matrix and the zero vector yields the zero vector
%--------------------------------------------------------------------------------------

matrix_prod_zero: LEMMA FORALL (A:Matrix): A * zero[A`cols] = zero[A`rows]

%--------------------------------------------------------------------------------------
% Rows and cols of a subtraction of matrices
%--------------------------------------------------------------------------------------

minus_rows: LEMMA FORALL (A:Matrix,B: (same_dim?(A))): (A - B)`rows = A`rows

minus_cols: LEMMA FORALL (A:Matrix,B: (same_dim?(A))): (A - B)`cols = A`cols

%--------------------------------------------------------------------------------------
% Rows and cols of the transpose matrix
%--------------------------------------------------------------------------------------

transpose_rows: LEMMA FORALL (A: Matrix): transpose(A)`rows = A`cols

transpose_cols: LEMMA FORALL (A: Matrix): transpose(A)`cols = A`rows

%--------------------------------------------------------------------------------------
% Rows and cols of a product of matrices
%--------------------------------------------------------------------------------------

product_rows: LEMMA FORALL (A: Matrix,(B: Matrix | B`rows = A`cols)): (A * B)`rows = A`rows

product_cols: LEMMA FORALL (A: Matrix,(B: Matrix | B`rows = A`cols)): (A * B)`cols = B`cols

product_rows2: LEMMA FORALL (A: Matrix,(B: Matrix | B`rows = A`cols),(C: Matrix | C`rows = B`cols)): (A * B * C)`rows = A`rows

product_cols2: LEMMA FORALL (A: Matrix,(B: Matrix | B`rows = A`cols),(C: Matrix | C`rows = B`cols)): (A * B * C)`cols = C`cols

product_rows3: LEMMA FORALL (A: Matrix,(B: Matrix | B`rows = A`cols),(C: Matrix | C`rows = B`cols),(D: Matrix | D`rows = C`cols)): (A * B * C * D)`rows = A`rows

product_cols3: LEMMA FORALL (A: Matrix,(B: Matrix | B`rows = A`cols),(C: Matrix | C`rows = B`cols),(D: Matrix | D`rows = C`cols)): (A * B * C * D)`cols = D`cols

product_rows4: LEMMA FORALL (A: Matrix,(B: Matrix | B`rows = A`cols),(C: Matrix | C`rows = B`cols),(D: Matrix | D`rows = C`cols),(E: Matrix | E`rows = D`cols)): (A * B * C * D * E)`rows = A`rows

product_cols4: LEMMA FORALL (A: Matrix,(B: Matrix | B`rows = A`cols),(C: Matrix | C`rows = B`cols),(D: Matrix | D`rows = C`cols),(E: Matrix | E`rows = D`cols)): (A * B * C * D * E)`cols = E`cols

%--------------------------------------------------------------------------------------
% Multiplying a matrix by its inverse yields the identity matrix
%--------------------------------------------------------------------------------------

inverse_ident: LEMMA FORALL (N: (invertible?)): inverse(N) * N = I(N`rows)

ident_inverse: LEMMA FORALL (N: (invertible?)): N * (inverse(N)) = I(N`rows)

%--------------------------------------------------------------------------------------
% Multiplying the identity matrix by a vector yields the vector
%--------------------------------------------------------------------------------------

ident_mat_prod: LEMMA FORALL (n: posnat, x: Vector[n]): matrices.I(n) * x = x

%--------------------------------------------------------------------------------------
% Rows and cols of the inverse matrix
%--------------------------------------------------------------------------------------

inverse_rows: LEMMA FORALL (N: (invertible?)): (inverse(N))`rows = N`rows

inverse_cols: LEMMA FORALL (N: (invertible?)): (inverse(N))`cols = N`cols

%--------------------------------------------------------------------------------------
% The transpose of the identity matrix is the identity matrix
%--------------------------------------------------------------------------------------

transp_ident: LEMMA FORALL (n: posnat): transpose(I(n)) = I(n)

%--------------------------------------------------------------------------------------
% Transpose and inverse "commute"
%--------------------------------------------------------------------------------------

transp_inv: LEMMA FORALL (M: (invertible?)):
                transpose(inverse(M))=inverse((transpose(M)))

%--------------------------------------------------------------------------------------
% Auxiliary lemmas to make further calculations eaiser with no other interest
%--------------------------------------------------------------------------------------

invar_inverse: LEMMA FORALL (A: Matrix, (N: (invertible?) | A`cols = N`rows)):
     A * (inverse(N) * N) = A

invar_inverse_left: LEMMA FORALL (B: Matrix, (N: (invertible?) | B`rows = N`cols)):
     N * (inverse(N)) * B = B

simply1_mat_vect: LEMMA FORALL (A: Matrix, (N: (invertible?) | A`cols = N`rows), y: Vector[A`rows], x: Vector[A`cols]):
     y * ((A * (inverse(N) * N)) * x) = y * (A * x)

simply2_mat_vect: LEMMA FORALL (B: Matrix, (N: (invertible?) | B`rows = N`rows), y: Vector[B`rows], x: Vector[B`cols]):
     y * (N * (inverse(N)) * B * x) = y * (B * x)

%--------------------------------------------------------------------------------------
% Distributive rules for matrices and vectors
%--------------------------------------------------------------------------------------

distr_mat_vect: LEMMA FORALL (A: Matrix, (B: (same_dim?(A))), y: Vector[A`cols]):
    (A + B) * y = A * y + B * y

distr_vect_mat: LEMMA FORALL (A: Matrix, x, y: Vector[A`cols]):
    A * x + A * y = A * (x + y)

%--------------------------------------------------------------------------------------
% Technical lemmas about applying "minus" to matrices
%--------------------------------------------------------------------------------------

matrix_sum_minus: LEMMA FORALL (A: Matrix, (B: (same_dim?(A)))): A - B = A + (-B)

matrix_prod_minus: LEMMA FORALL (A: Matrix, x: Vector[A`cols]): -(A * x) = (-A) * x

%--------------------------------------------------------------------------------------
% Some more distributive rules for matrices and vectors
%--------------------------------------------------------------------------------------

distr_esc_add: LEMMA FORALL (A: Matrix, (B: (same_dim?(A))), x:Vector[A`rows], y:Vector[A`cols]):
    x * ((A + B) * y) = x * (A * y) + x * (B * y)

distr_esc_dif: LEMMA FORALL (A: Matrix, (B: (same_dim?(A))), x:Vector[A`rows], y:Vector[A`cols]):
    x * ((A - B) * y) = x * (A * y) - x * (B * y)

distr_add_esc: LEMMA FORALL (A: (square?), x:Vector[A`cols], y:Vector[A`cols]):
    (x + y) * (A  * (x + y)) = x * (A * x) + x * (A * y) + y * (A * x) + y * (A * y)

%--------------------------------------------------------------------------------------
% Auxiliary lemma to make further calculations easier (aimed at Schur formula)
%--------------------------------------------------------------------------------------

conv_prod_int:  LEMMA FORALL (B: Matrix, (A: Matrix | B`cols = A`rows), (C: Matrix | A`cols = C`rows),  x: Vector[B`rows], y: Vector[C`cols]):
    x*((B*(A*C))*y) = (transpose(B)*x)*(A*(C*y))

END matrix_lemmas

quality81%

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