Verified error bounds for the singular values of structured matrices with applications to computer-assisted proofs for differential equations

TL;DR

This paper presents two efficient methods for verifying singular values of structured matrices, aiding in computer-assisted proofs for differential equations by providing tight bounds and lower estimates, especially for sparse matrices.

Contribution

Introduces two novel methods for verifying singular values of structured matrices, improving efficiency and accuracy in computational proofs for differential equations.

Findings

Methods verify all singular values with tight error bounds

Lower bound estimation is effective for sparse matrices

Applications improve computational efficiency in differential equation proofs

Abstract

This paper introduces two methods for verifying the singular values of the structured matrix denoted by $R^{-H}AR^{-1}$, where $R$ is a nonsingular matrix and $A$ is a general nonsingular square matrix. The first of the two methods uses the computed factors from a singular value decomposition (SVD) to verify all singular values; the second estimates a lower bound of the minimum singular value without performing the SVD. The proposed approach for verifying all singular values efficiently computes tight error bounds. The method for estimating a lower bound of the minimum singular value is particularly effective for sparse matrices. These methods have proven to be efficient in verifying solutions to differential equation problems, that were previously challenging due to the extensive computational time and memory requirements.