Verified error bounds for solutions of Sylvester matrix equations

We develop methods for computing verified solutions of Sylvester matrix equations AX+XB=C. To this purpose we propose a variant of the Krawczyk interval operator with a factorized preconditioner so that the complexity is reduced to cubic when A and B are dense and diagonalizable. Block diagonalizations can be used in cases where A or B are not diagonalizable. The Lyapunov equation, as a special case, is also considered.