TheoremStatement: 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.

A DARE residual, Stein inverse bound, and Lyapunov margin certify a stabilizing root

Statement

Let $\hat{X} = {\hat{X}}^{*}$ be a DARE candidate, $S (X) = R + B^{*} X B$ , $K (X) = S (X)^{- 1} B^{*} X A$ , $A_{c} (X) = A - B K (X)$ , and let $F_{d} (X) = Q + A^{*} X A - A^{*} X B S (X)^{- 1} B^{*} X A - X .$ Suppose $S (\hat{X}) ⪰ δ_{0} I$ is outward-certified. For a proposed radius $ρ > 0$ put $a = ∥ A ∥_{2}, b = ∥ B ∥_{2}, m = ∥ \hat{X} ∥_{F} + ρ, δ = δ_{0} - b^{2} ρ .$ Require $δ > 0$ and define $L_{K} = \frac{a b}{δ} + \frac{a b^{3} m}{δ^{2}}, M_{c} = a + \frac{a b^{2} m}{δ}, L_{c} = b L_{K}, L_{D} = 2 M_{c} L_{c} .$ Let $D (E) = A_{c} (\hat{X})^{*} E A_{c} (\hat{X}) - E$ be invertible on Hermitian matrices, with outward-certified $κ \geq ∥ D^{- 1} ∥_{F \to F}$ and $r \geq ∥ F_{d} (\hat{X}) ∥_{F}$ . If $κ (r + L_{D} ρ^{2} / 2) \leq ρ, κ L_{D} ρ < 1,$ there is exactly one Hermitian DARE root in the closed Frobenius $ρ$ -ball, and $R + B^{*} X B ⪰ δ I$ throughout that ball.

For the stabilizing branch, additionally suppose ${\hat{A}}_{c} = A_{c} (\hat{X})$ is Schur stable and an outward-certified $W ≻ 0$ satisfies $W - {\hat{A}}_{c}^{*} W {\hat{A}}_{c} ⪰ γ I .$ If, with $η = L_{c} ρ$ , $∥ W ∥_{2} (2 M_{c} η + η^{2}) < γ,$ then the root is Schur-stabilizing. Under the standard DARE hypotheses of Stabilizability and detectability give the unique stabilizing positive-semidefinite DARE solution, it is the unique stabilizing positive-semidefinite solution.

Facts & Assumptions

Given: The DARE data and residual map of Standard CARE and DARE data, equations, and conventions, a Hermitian candidate, and the verified constants in the Statement.

[F1]

Standard CARE and DARE data, equations, and conventions: $S (X) = R + B^{*} X B$ , $A_{c} (X) = A - B S (X)^{- 1} B^{*} X A$ , and $F_{d} (X) = Q + A^{*} X A - A^{*} X B S (X)^{- 1} B^{*} X A - X$ .

[F2]

Verified point and uniform linear residual certificate data specifies mathematical bounds for a linear approximate-inverse defect and preconditioned residual, and does not prescribe how to establish them. The DARE bounds used here are the separate hypotheses in [A1].

[F3]

Outward-rounded operations are inclusion-isotone and enclose DAG evaluations: a finite outward-rounded expression DAG encloses every exact node value.

[F4]

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

[F5]

The operator norm is submultiplicative and satisfies ||T^*T|| = ||T||^2: operator norms are submultiplicative.

[F6]

Stabilizability and detectability give the unique stabilizing positive-semidefinite DARE solution: under the standard discrete hypotheses there is a unique stabilizing positive-semidefinite DARE solution.

[F7]

Powers of a Schur-stable matrix decay geometrically up to a polynomial factor: if $A_{c}$ is Schur stable, then $∣ A_{c}^{k} ∣_{2} \to 0$ geometrically.

[F8]

Every finite-dimensional normed space is Banach: every finite-dimensional normed space is complete, so a Cauchy sequence in the Hermitian matrix ball converges there.

[A1]

The lower eigenvalue bound $δ_{0}$ , norm bounds, residual bound, inverse bound $κ$ , and Lyapunov margin are outward-verified inputs. If any bound is unavailable, this item supplies no certificate.

Proof

1.1F1A1F3F4F5algebra

For any Hermitian $E$ with $∥ E ∥_{F} \leq ρ$ , [F3] and [F4] give $S (\hat{X} + E) = S (\hat{X}) + B^{*} E B ⪰ (δ_{0} - b^{2} ρ) I = δ I .$ Thus $S (X)$ is invertible on the ball and $∥ S (X)^{- 1} ∥_{2} \leq δ^{- 1}$ . The resolvent identity gives $∥ S (X)^{- 1} - S (Y)^{- 1} ∥_{2} \leq b^{2} δ^{- 2} ∥ X - Y ∥_{F} .$ Using $K (X) = S (X)^{- 1} B^{*} X A$ and splitting the difference into the change in $X$ and the change in $S^{- 1}$ yields $∥ K (X) - K (Y) ∥_{F} \leq L_{K} ∥ X - Y ∥_{F}, ∥ A_{c} (X) ∥_{2} \leq M_{c}, ∥ A_{c} (X) - A_{c} (Y) ∥_{2} \leq L_{c} ∥ X - Y ∥_{F} .$

2.1F1A1F4F5step 1.1algebra

Differentiating $S^{- 1} S = I$ gives $d (S^{- 1}) [E] = - S^{- 1} (B^{*} E B) S^{- 1}$ . Substituting this in the derivative of $F_{d}$ and using $K = S^{- 1} B^{*} X A$ gives $F_{d}^{'} (X) [E] = A_{c} (X)^{*} E A_{c} (X) - E .$ Consequently, for $D_{X} = F_{d}^{'} (X)$ and $D_{Y} = F_{d}^{'} (Y)$ , [F4]–[F5] give $∥ D_{X} - D_{Y} ∥_{F \to F} \leq (∥ A_{c} (X) ∥_{2} + ∥ A_{c} (Y) ∥_{2}) ∥ A_{c} (X) - A_{c} (Y) ∥_{2} \leq L_{D} ∥ X - Y ∥_{F} .$ Integrating the derivative along the segment from $\hat{X}$ to $\hat{X} + E$ gives a Taylor remainder $R (E)$ with $F_{d} (\hat{X} + E) = F_{d} (\hat{X}) + D (E) + R (E), ∥ R (E) ∥_{F} \leq L_{D} ∥ E ∥_{F}^{2} / 2.$

3.1A1F2F8step 2.1algebra

The root equation is the fixed-point equation $E = T (E) : = - D^{- 1} F_{d} (\hat{X}) - D^{- 1} R (E) .$ The bounds in [A1], separate from the linear certificate data in [F2], make $T$ a self-map of the closed ball. For $E, F$ in that ball, integrating $D_{X} - D$ along the segment between them gives $∥ R (E) - R (F) ∥_{F} \leq L_{D} ρ ∥ E - F ∥_{F},$ so $T$ has contraction factor at most $κ L_{D} ρ < 1$ . Iteration from zero has successive differences bounded by a geometric sequence, hence is Cauchy. The closed Hermitian ball is complete by [F8], so the sequence converges in the ball; continuity makes its limit a fixed point. The same contraction inequality makes it unique.

4.1A1F1F6F7step 3.1algebra∎

Let $X = \hat{X} + E$ be the root. Then $∥ A_{c} (X) - {\hat{A}}_{c} ∥_{2} \leq L_{c} ρ = η$ . Expanding the Stein form, $A_{c} (X)^{*} W A_{c} (X) - {\hat{A}}_{c}^{*} W {\hat{A}}_{c} = {\hat{A}}_{c}^{*} W Δ + Δ^{*} W {\hat{A}}_{c} + Δ^{*} W Δ,$ where $Δ = A_{c} (X) - {\hat{A}}_{c}$ . Its norm is at most $∥ W ∥_{2} (2 M_{c} η + η^{2}) < γ$ . Hence $W - A_{c} (X)^{*} W A_{c} (X) ≻ 0$ . For an eigenvector $A_{c} (X) v = λ v$ , this gives $(1 - ∣ λ ∣^{2}) v^{*} W v > 0$ , so $∣ λ ∣ < 1$ . Let $K = K (X)$ , $S = R + B^{*} X B$ , and $x_{k + 1} = A_{c} (X) x_{k}$ , $u_{k} = - K x_{k}$ . Since $S K = B^{*} X A$ , we have $K^{*} S K = A^{*} X B S^{- 1} B^{*} X A$ . Expanding $A_{c}^{*} X A_{c} = (A - B K)^{*} X (A - B K)$ gives $A_{c}^{*} X A_{c} = A^{*} X A - K^{*} S K - K^{*} S K + K^{*} B^{*} X B K = A^{*} X A - K^{*} S K - K^{*} R K .$ The DARE root equation therefore gives $X = Q + K^{*} R K + A_{c}^{*} X A_{c}$ , which along $x_{k + 1} = A_{c} x_{k}$ and $u_{k} = - K x_{k}$ is the exact square identity $x_{k}^{*} Q x_{k} + u_{k}^{*} R u_{k} + x_{k + 1}^{*} X x_{k + 1} = x_{k}^{*} X x_{k} .$ Summing to $N - 1$ yields $x_{0}^{*} X x_{0} = \sum_{k < N} (x_{k}^{*} Q x_{k} + u_{k}^{*} R u_{k}) + x_{N}^{*} X x_{N}$ . By [F7], $x_{N} \to 0$ , so $x_{0}^{*} X x_{0}$ is a sum of nonnegative terms; hence $X ⪰ 0$ . Now [F6] identifies it as the unique stabilizing positive-semidefinite solution.

Depends on

Used by

Dependency tree · two levels

44 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

Federico Poloni, Lecture notes on Riccati-type matrix equations (standard reference, not scraped)
A.A. Stoorvogel and A. Saberi, The discrete algebraic Riccati equation and linear matrix inequality, Memorandum COSOR 94-16 (standard reference, not scraped)