|
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
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
