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.

DARE structure-preserving doubling converges with a quantified quadratic error envelope

Statement

Under the discrete stabilizability and detectability hypotheses of Stabilizability and detectability give the unique stabilizing positive-semidefinite DARE solution, start the exact recurrence of Finite-budget structure-preserving doubling iteration for the DARE from $A_{0} = A$ , $G_{0} = B R^{- 1} B^{*}$ , and $H_{0} = Q$ . Then all inverses exist, $G_{j}, H_{j} ⪰ 0$ , and $H_{j}$ converges to the stabilizing DARE solution $X_{*}$ . More quantitatively, there are $q \in (0, 1)$ , an index $j_{0}$ , and $C > 0$ such that $∥ H_{j} - X_{*} ∥_{F, W^{- 1}} \leq C q^{2^{j + 1}} (j \geq j_{0}),$ where $W ≻ 0$ is a Stein witness constructed from the closed-loop matrix. The envelope $ϵ_{j} = C q^{2^{j + 1}}$ obeys $ϵ_{j + 1} = ϵ_{j}^{2} / C$ . The constants are conditional on the closed-loop spectral separation and its norm conditioning; no uniform constant depending only on dimension is asserted.

Facts & Assumptions

Given: The standard DARE data and the exact discrete stabilizability/detectability hypotheses.

[F1]

Stabilizability and detectability give the unique stabilizing positive-semidefinite DARE solution: the finite-horizon iterates $P_{0} = 0$ , $P_{k + 1} = f (P_{k})$ increase to $X_{*}$ , and $A_{c} (X_{*})$ is Schur stable.

[F2]

The DARE doubling recurrence composes two Riccati steps and preserves positive semidefiniteness: the recurrence is well-defined, preserves $G_{j}, H_{j} ⪰ 0$ , and $H_{j} = f^{2^{j}} (0)$ .

[F3]

Powers of a Schur-stable matrix decay geometrically up to a polynomial factor: powers of every Schur-stable matrix have a geometric bound with any rate above its spectral radius.

[F4]

A non-negative operator has a unique non-negative square root: a positive-semidefinite matrix has a positive-semidefinite square root; for $W ≻ 0$ this square root is positive definite.

[F5]

Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison: compatible matrix products satisfy the induced Frobenius/operator norm bounds.

Proof

1.1F1F2algebra

By [F2], $H_{j} = P_{2^{j}}$ and $G_{j}, H_{j}$ remain positive semidefinite. Since [F1] gives $P_{k} \to X_{*}$ , the subsequence $H_{j} = P_{2^{j}}$ also converges to $X_{*}$ . No inverse of $A$ is used.

1.2F1F3F4algebra

Put $M = A_{c} (X_{*})$ . By [F1], $M$ is Schur stable; [F3] therefore makes $W = \sum_{k = 0}^{\infty} (M^{*})^{k} M^{k}$ converge in norm. It is positive definite, $W ⪰ I$ , and $M^{*} W M = W - I$ . If $w = ∥ W ∥_{2}$ , then $v^{*} M^{*} W M v \leq (1 - w^{- 1}) v^{*} W v$ , so the induced $W$ -norm $∥ M ∥_{W} : = ∥ W^{1 / 2} M W^{- 1 / 2} ∥_{2}$ is at most $q_{0} = \sqrt{1 - w^{- 1}} < 1$ . Choose $q$ with $q_{0} < q < 1$ . Since $P_{k} \to X_{*}$ and $A_{c} (P_{k})$ is continuous on $P_{k} ⪰ 0$ , choose $k_{0}$ so $∥ A_{c} (P_{k}) ∥_{W} \leq q$ for all $k \geq k_{0}$ .

2.1F1F5step 1.2algebrainduction∎

Let $E_{k} = X_{*} - P_{k} ⪰ 0$ . The Riccati-map difference identity in [F1] gives $E_{k + 1} = M^{*} E_{k} A_{c} (P_{k}) .$ Define $∥ E ∥_{F, W^{- 1}} = ∥ W^{- 1 / 2} E W^{- 1 / 2} ∥_{F}$ . By [F5], for $k \geq k_{0}$ , $∥ E_{k + 1} ∥_{F, W^{- 1}} \leq ∥ M ∥_{W} ∥ A_{c} (P_{k}) ∥_{W} ∥ E_{k} ∥_{F, W^{- 1}} \leq q^{2} ∥ E_{k} ∥_{F, W^{- 1}} .$ Iteration gives $∥ E_{k} ∥_{F, W^{- 1}} \leq ∥ E_{k_{0}} ∥_{F, W^{- 1}} q^{2 (k - k_{0})}$ . Taking $k = 2^{j}$ and setting $C = \max {1, ∥ E_{k_{0}} ∥_{F, W^{- 1}} q^{- 2 k_{0}}}$ proves the displayed envelope for all $2^{j} \geq k_{0}$ . Since $C > 0$ , direct calculation gives $ϵ_{j + 1} = C q^{2^{j + 2}} = ϵ_{j}^{2} / C$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

28 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)