Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Takeshi Terao, Yoshitaka Watanabe, Katsuhisa Ozaki

TL;DR

This work tackles the problem of obtaining rigorous enclosures for the singular values of $R^{-H}AR^{-1}$, where $B=R^HR$ is Hermitian positive definite and $A$ is nonsingular, with applications to computer-assisted proofs for differential equations. It introduces a generalized HSVD-like decomposition $AV_B = BU_B\Sigma$ that yields $R^{-H}AR^{-1} = U_B\Sigma V_B^H$, and presents two verification strategies: (i) a tight, SVD-based method to certify all $\sigma_i$ from approximate factors, and (ii) a fast, non-SVD method to bound $\sigma_{\min}$, suitable for large sparse matrices via a 2$\!$n-by-2$\!$n generalized eigenproblem. The paper demonstrates accuracy, stability, and computational efficiency through dense-matrix experiments and an elliptic PDE discretization, showing practical viability for high-dimensional problems. Overall, the proposed approaches enable reliable, scalable, certified bounds for singular values that support robust computer-assisted proofs in differential equations and related applications.

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.

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

TL;DR

This work tackles the problem of obtaining rigorous enclosures for the singular values of , where is Hermitian positive definite and is nonsingular, with applications to computer-assisted proofs for differential equations. It introduces a generalized HSVD-like decomposition that yields , and presents two verification strategies: (i) a tight, SVD-based method to certify all from approximate factors, and (ii) a fast, non-SVD method to bound , suitable for large sparse matrices via a 2n-by-2n generalized eigenproblem. The paper demonstrates accuracy, stability, and computational efficiency through dense-matrix experiments and an elliptic PDE discretization, showing practical viability for high-dimensional problems. Overall, the proposed approaches enable reliable, scalable, certified bounds for singular values that support robust computer-assisted proofs in differential equations and related applications.

Abstract

This paper introduces two methods for verifying the singular values of the structured matrix denoted by , where is a nonsingular matrix and 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.

Paper Structure

This paper contains 17 sections, 5 theorems, 57 equations, 5 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Previous works
  3. Notation
  4. Estimation of singular values and the matrix norm
  5. Estimation of eigenvalues
  6. Previous work regarding the issue
  7. The proposed method
  8. A new matrix decomposition
  9. Verification methods
  10. For all singular values
  11. For the minimum singular value
  12. Numerical examples
  13. Example 1
  14. Example 2
  15. Example 3
  16. ...and 2 more sections

Key Result

Theorem 1

Let $A\in\mathbb{C}^{n\times n}$ and $B=B^H\in\mathbb{C}^{n\times n}$ be given, and $\widehat{U}_B, \widehat{\Sigma}=\mathrm{diag}(\widehat{\sigma}_i)$, and $\widehat{V}_B$ be approximate results of Algorithm alg:GHSVD. Define Assume that Then, is satisfied for $1\leq i\leq n$.

Theorems & Definitions (11)

  • Theorem 1
  • proof
  • Corollary 1
  • proof
  • Theorem 2
  • Remark 1
  • proof
  • Theorem 3
  • proof
  • Theorem 4
  • ...and 1 more