TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

A proved rational shift bound implies low-rank ADI convergence

Statement

Let $A$ be Hurwitz, let $B \in F^{n \times r}$ , and let $p_{1}, p_{2}, \dots$ be admissible shifts for Low-rank ADI for a continuous Lyapunov equation. Define

ρ_{j} (z) = \prod_{i = 1}^{j} \frac{z - \overline{p_{i}}}{z + p_{i}} .

Suppose a proved rational shift estimate gives $∥ ρ_{j} (A) ∥_{2} \leq η_{j}$ for a sequence $η_{j} \to 0$ . Then the ADI iterates converge in Frobenius norm to the unique integral solution $X = \int_{0}^{\infty} e^{t A} B B^{*} e^{t A^{*}} d t$ , with

∥ X - X_{j} ∥_{F} \leq \frac{η_{j}^{2} ∥ B ∥_{F}^{2}}{sep (A, - A^{*})} .

No convergence assertion is made without this rational operator bound.

Facts & Assumptions

Given: A Hurwitz matrix, a forcing factor $B$ , admissible shifts, and the stated proved rational estimate.

[F1]

Low-rank ADI for a continuous Lyapunov equation: $R_{0} = B$ , $R_{j} = R_{j - 1} - 2 Re (p_{j}) (A + p_{j} I)^{- 1} R_{j - 1}$ .

[F2]

Low-rank ADI has an exact residual factor identity: $A X_{j} + X_{j} A^{*} + B B^{*} = R_{j} R_{j}^{*}$ .

[F3]

A Sylvester equation is uniquely solvable exactly when the spectra are disjoint: The operator $X \mapsto A X + X B$ is invertible exactly when $σ (A) \cap (- σ (B)) = \emptyset$ , equivalently when $sep (A, - B) > 0$ .

[F4]

Sylvester separation converts a residual into a forward error bound: For a unique Sylvester solution, the Frobenius forward error is at most the Frobenius equation residual divided by separation.

[F5]

The Hurwitz Lyapunov integral is the unique solution and has the stated positivity: For Hurwitz $A$ , the integral $X$ exists uniquely and satisfies $A X + X A^{*} + B B^{*} = 0$ .

[F6]

Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison: The Frobenius norm is unitarily invariant and its square is the sum of squared singular values.

[F7]

In orthonormal bases, the matrix of the adjoint is the conjugate transpose of the matrix: In the standard orthonormal basis, the matrix of the adjoint is the conjugate transpose.

[F8]

For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$ : Transposition preserves the determinant.

[F9]

Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive: Complex conjugation is a field automorphism.

[F10]

For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix: The determinant is given by the signed Leibniz formula.

[A1]

For every $j$ , the chosen shifts satisfy the operator rational estimate $∥ ρ_{j} (A) ∥_{2} \leq η_{j}$ , with $η_{j} \to 0$ .

Proof

1.1F1algebra

From [F1], $R_{j} = (I - 2 Re (p_{j}) (A + p_{j} I)^{- 1}) R_{j - 1} = (A - \overline{p_{j}} I) (A + p_{j} I)^{- 1} R_{j - 1}$ , since $- 2 Re (p_{j}) = - (p_{j} + \overline{p_{j}})$ . All factors are rational functions of $A$ and commute, so iterating gives $R_{j} = ρ_{j} (A) B$ .

1.2F2F3F5F7F8F9F10algebra

In the standard orthonormal basis, [F7] represents $A^{*}$ by ${\overline{A}}^{T}$ . For $z \in C$ , [F8] and [F10] give $\det (z I - A^{*}) = \det ((z I - \overline{A})^{T}) = \det (z I - \overline{A})$ , and [F9] applied to the Leibniz formula gives $\det (z I - \overline{A}) = \overline{\det (\overline{z} I - A)}$ . Hence $σ (A^{*}) = \overline{σ (A)}$ , so both $A$ and $A^{*}$ have spectrum in the open left half-plane; therefore $σ (A) \cap (- σ (A^{*})) = \emptyset$ . By [F3], $sep (A, - A^{*}) > 0$ . Subtracting the equation for $X_{j}$ in [F2] from the exact equation in [F5] gives $S_{A, A^{*}} (X - X_{j}) = - R_{j} R_{j}^{*}$ .

2.1A1step 1.1algebra

Applying the operator bound in [A1] to each column of $B$ and summing squared column norms gives $∥ R_{j} ∥_{F} \leq η_{j} ∥ B ∥_{F}$ .

3.1F4F5F6step 2.1step 1.2algebra∎

Apply [F4] to step 1.2. If $R_{j} = U Σ V^{*}$ is an SVD, then $R_{j} R_{j}^{*} = U Σ Σ^{*} U^{*}$ , so unitary invariance and [F6] give $∥ R_{j} R_{j}^{*} ∥_{F}^{2} = \sum_{i} s_{i} (R_{j})^{4} \leq (\sum_{i} s_{i} (R_{j})^{2})^{2} = ∥ R_{j} ∥_{F}^{4}$ . Therefore $∥ X - X_{j} ∥_{F} \leq ∥ R_{j} R_{j}^{*} ∥_{F} / sep (A, - A^{*}) \leq η_{j}^{2} ∥ B ∥_{F}^{2} / sep (A, - A^{*})$ . Since $η_{j} \to 0$ and the separation is positive, the right side tends to zero.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

54 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

Valeria Simoncini, Computational Methods for Linear Matrix Equations, SIAM Review 58(3), 2016 (standard reference, not scraped)
Elias Jarlebring, Numerical Methods for Lyapunov Equations, lecture notes in numerical linear algebra, 2017 (standard reference, not scraped)