| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/linear_algebra/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 877 B |
|
Quelle ellipsoid.pvs Sprache: PVS |
|||||||||
|
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.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28