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