|
ellipsoid: theory
begin
importing matrix_operator, matrices
M,N,Q:var Matrix
n:var posnat
i,j:var posnat
ellipsoid: LEMMA
forall (n:posnat, Q, M: SquareMat(n), x, y, b, c: Vector[n]):
bijective?(n)(T(n,n)(Q)) AND bijective?(n)(T(n,n)(M))
AND (x-c)*(inv(n)(Q)*(x-c))<=1
AND y=M*x + b
IMPLIES
(y-b-M*c)*(inv(n)(M*(Q*transpose(M)))*(y-b-M*c))<=1
%thm1:LEMMA same_dim?(M,N) and i<M`rows and j<M`cols
% IMPLIES
% (M+N)`matrix(i,j)=(N+M)`matrix(i,j)
%thm2 :LEMMA %same_dim?(M,I(n))and i<M`rows and j<n implies
% (M*I(n))`matrix(i,j)=M`matrix(i,j)
%thm3: LEMMA same_dim?(M,I(n))implies inv(n)(M)*M=I(n)
%thm4:LEMMA square?(M) AND squareMat?(n)(M) AND bijective?(n)(T(n, n)(M))
% implies
% (inv(n)(M)*M)`matrix(i,j)=1
end ellipsoid
¤ Dauer der Verarbeitung: 0.14 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.
|
