CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Computed singular-value error is bounded by backward perturbation plus readout error

Statement

Let $A \in F^{m \times n}$ and put $C = A$ when $m \geq n$ , $C = A^{*}$ when $m < n$ . Suppose a successful computed SVD path in this tall orientation supplies $C + E = \hat{U} [\begin{array}{c} \hat{B} \\ 0 \end{array}] {\hat{V}}^{*}$ , where $\hat{U} \in F^{M \times M}$ and $\hat{V} \in F^{p \times p}$ are the exact unitary products represented by the stored local transformations, $M = \max (m, n)$ , $p = \min (m, n)$ , and the returned square $\hat{B} \in F^{p \times p}$ is the diagonal final bidiagonal matrix from Finite budget implicit shifted QR for bidiagonal singular values. These are the theoretical factors in Local stable reflectors and rotations give an aggregate SVD backward error, separate from the rounded dense accumulators returned for candidate triplets. If the returned values are the exact singular values of $\hat{B}$ , then for every $1 \leq i \leq p$ , $∣ {\hat{σ}}_{i} - σ_{i} (A) ∣ \leq ∥ E ∥_{2} \leq ∥ E ∥_{F} .$ For actual rounded modulus readout from a diagonal $\hat{B}$ , let $d_{i} = {\hat{B}}_{i i}$ and $ϵ_{r e a d} = ((1 + u)^{4} - 1) \max ({0} \cup {∣ d_{i} ∣ : 1 \leq i \leq p})$ for the successful scaled complex modulus algorithm; use zero for exact real absolute values. Thus $ϵ_{r e a d} = 0$ when $p = 0$ . After ordering the candidates, the bound is $∣ {\hat{σ}}_{i} - σ_{i} (A) ∣ \leq ∥ E ∥_{2} + ϵ_{r e a d}$ . This assertion applies to a successful, fully reduced result; a finite-budget budget-exhausted output has residual reports but no such accuracy conclusion.

Facts & Assumptions

Given: The successful nearby-factorization relation, exact values $s_{i} = σ_{i} (\hat{B})$ , and either exact readout ${\hat{σ}}_{i} = s_{i}$ or the specified rounded diagonal-modulus readout.

[F1]

Local stable reflectors and rotations give an aggregate SVD backward error supplies $C + E = \hat{U} [\begin{array}{c} \hat{B} \\ 0 \end{array}] {\hat{V}}^{*}$ under its local arithmetic hypotheses, with the same tall-orientation dimensions.

[F2]

Singular values are Lipschitz in the spectral norm bounds each singular-value change by the spectral norm of the matrix perturbation.

[F3]

Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison: unitary factors preserve singular values and $∥ E ∥_{2} \leq ∥ E ∥_{F}$ .

[F4]

Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition: taking the adjoint of an SVD interchanges its two orthonormal singular-vector bases and leaves the $p$ ordered singular values unchanged.

[F5]

Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add supplies the successful real square-root and component-operation relative model.

Proof

1.1F1F3F4algebra

By [F1], $C + E = \hat{U} [\begin{array}{c} \hat{B} \\ 0 \end{array}] {\hat{V}}^{*}$ . The tall matrix $[\begin{array}{c} \hat{B} \\ 0 \end{array}]$ has the singular values of $\hat{B}$ , since its adjoint times itself is ${\hat{B}}^{*} \hat{B}$ ; unitary invariance in [F3] therefore gives the ordered singular values $s_{i}$ for $C + E$ . By [F4], $C$ and $A$ have the same $p$ singular values.

2.1step 1.1F2F3algebra

Apply [F2] to $C$ and $C + E$ . It gives $∣ σ_{i} (C + E) - σ_{i} (C) ∣ \leq ∥ E ∥_{2}$ ; step 1.1 identifies these singular values with $s_{i}$ and $σ_{i} (A)$ , respectively, and [F3] gives $∥ E ∥_{2} \leq ∥ E ∥_{F}$ .

3.1F5step 2.1algebra∎

A scaled modulus of two real components has relative norm factors between $(1 - u)^{4}$ and $(1 + u)^{4}$ , by expanding the two scaling operations, square products and sum, square root and rescaling. Hence each rounded magnitude differs from $∣ d_{i} ∣$ by at most $ϵ_{r e a d}$ . If two finite lists differ coordinatewise by at most $ϵ$ , their ordered lists do too: otherwise at the violating rank the count of entries above or below the corresponding threshold contradicts the coordinatewise bounds. Apply this to the diagonal magnitudes and combine with step 2.1. For exact readout ${\hat{σ}}_{i} = s_{i}$ the first bound follows already from step 2.1; for rounded readout the additional modulus allowance gives the stated extension. Real sign removal is exact.

Depends on

Used by

A certified computed smallest singular value encloses pseudospectrum membership Theorem

Dependency tree · two levels

26 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Wen-Wei Lin, Lecture Notes of Matrix Computations, §6.3 (standard reference, not scraped)
James Demmel and W. Kahan, Accurate Singular Values of Bidiagonal Matrices, Theorem 3 (standard reference, not scraped)