|
linear_dependence % [ parameters ]
: THEORY
BEGIN
IMPORTING matrices, matrix_props
A,M,N: VAR PosFullMatrix
m,i: VAR nat
p: VAR posnat
v: VAR Vector
f,g: VAR [nat->real]
zerow(p): PosFullMatrix = (: zero(p) :)
zecolumn(p): PosFullMatrix = transpose(zerow(p))
zerow_dim: LEMMA rows(zerow(p)) = 1 AND columns(zerow(p)) = p
zecolumn_dim: LEMMA rows(zecolumn(p)) = p AND columns(zecolumn(p))=1
row2mat(A, (j:below(rows(A)))): PosFullMatrix = (:row(A)(j):)
row2mat_dim: LEMMA FORALL (j:below(rows(A))): rows(row2mat(A,j)) = 1 AND columns(row2mat(A,j)) = columns(A)
sum_rows(A,f,(j:below(rows(A))), M): RECURSIVE PosFullMatrix =
IF j=0 THEN M+f(j)*row2mat(A,j)
ELSE sum_rows(A,f,j-1, M+f(j)*row2mat(A,j))
ENDIF
MEASURE j
sum_rows(A,f): PosFullMatrix = sum_rows(A,f, rows(A)-1, zerow(columns(A)))
sum_rows_eq: LEMMA FORALL (j:below(rows(A))):
(FORALL (k:subrange(0,j)): f(k) = g(k)) IMPLIES
sum_rows(A,f,j,M) = sum_rows(A,g,j,M)
sum_rows_add_start: LEMMA FORALL (j:below(rows(A))):
sum_rows(A, f, j, M+N) = sum_rows(A, f, j, M) + N
subtract_same_scal: LEMMA FORALL (j:below(rows(A))): (f(j) * row2mat(A, j) - f(j) * row2mat(A, j)) = 0 * row2mat(A, j)
sum_lem_prep: LEMMA FORALL(j:below(rows(A)), k:below(j+1)):
sum_rows(A,f WITH [k:=0], j, M) = sum_rows(A, f, j, M) - f(k)*row2mat(A,k)
sum_lem: LEMMA FORALL(j:below(rows(A))): sum_rows(A,f WITH [j:=0]) = sum_rows(A,f) -f(j)*row2mat(A,j)
row_dependent(A,(j:below(rows(A))),f): bool =
(sum_rows(A,f) = zerow(columns(A)))
row_dependence_lem: LEMMA FORALL (j:below(rows(A)), (f|f(j)=-1)):
row_dependent(A,j,f) IMPLIES
%FORALL ((M|rows(M) = columns(A) AND columns(M) =1)):
row2mat(A,j)*M = sum_rows(A, f WITH [j:=0])*M
row_dep(A, (j:below(rows(A))), f): bool = ((f(j)=-1 AND row_dependent(A,j,f)) OR (f = LAMBDA(i:nat): 0))
row_dep_fun(A, (j:below(rows(A))), (f: {g:[nat->real]| row_dep(A,j,g)})): [nat->real] =
f WITH [j:= f(j)+1]
END linear_dependence
¤ Dauer der Verarbeitung: 0.15 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.
|
