A Matrix Positivstellensatz with lifting polynomials

Given the projections of two semialgebraic sets defined by polynomial matrix inequalities, it is in general difficult to determine whether one is contained in the other. To address this issue we propose a new matrix Positivstellensatz that uses lifting polynomials. Under the classical archimedean condition and some mild natural assumptions, we prove that such a containment holds if and only if the proposed matrix Positivstellensatz is satisfied. The corresponding certificate can be searched for by solving a semidefinite program. An important application is to certify when a spectrahedrop (i.e., the projection of a spectrahedron) is contained in another one.