LemmaStatement: AI-adaptedProof: 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.

The DARE doubling recurrence composes two Riccati steps and preserves positive semidefiniteness

Statement

For Hermitian $G, H ⪰ 0$ , define $Φ_{G} (X) = X (I + G X)^{- 1}$ and $f (X) = H + A^{*} Φ_{G} (X) A$ on $X ⪰ 0$ . One step of the exact inverse recurrence in Finite-budget structure-preserving doubling iteration for the DARE is well-defined, preserves $G_{j}, H_{j} ⪰ 0$ , and its updated triple satisfies $f \circ f (X) = H_{1} + A_{1}^{*} X (I + G_{1} X)^{- 1} A_{1},$ where $A_{1} = A (I + G H)^{- 1} A, G_{1} = G + A (I + G H)^{- 1} G A^{*}, H_{1} = H + A^{*} H (I + G H)^{- 1} A .$ Consequently, starting from $(A, G, H)$ , the exact recurrence satisfies $H_{j} = f^{2^{j}} (0)$ after $j$ updates. These claims concern exact arithmetic; the rounded branch has only its separately reported diagnostics.

Facts & Assumptions

Given: Finite matrices $A$ and Hermitian positive-semidefinite $G, H$ over $F \in {R, C}$ .

[F1]

Finite-budget structure-preserving doubling iteration for the DARE: the exact-mode update formulas are $A_{1} = A (I + G H)^{- 1} A$ , $G_{1} = G + A (I + G H)^{- 1} G A^{*}$ , and $H_{1} = H + A^{*} H (I + G H)^{- 1} A$ .

[F2]

Standard CARE and DARE data, equations, and conventions: for $G = B R^{- 1} B^{*}$ , the DARE map is $X \mapsto Q + A^{*} X (I + G X)^{- 1} A$ .

[F3]

A non-negative operator has a unique non-negative square root: a positive-semidefinite matrix has a positive-semidefinite square root.

Proof

1.1F1F3algebra

If $(I + G H) v = 0$ , then multiplication by $v^{*} H$ gives $v^{*} H v + (H v)^{*} G (H v) = 0.$ Both terms are nonnegative, so $H v = 0$ and then $v = 0$ . Thus $I + G H$ is invertible; the same argument applies to $I + H G$ . The identities $(I + G H)^{- 1} G = G (I + H G)^{- 1} = G^{1 / 2} (I + G^{1 / 2} H G^{1 / 2})^{- 1} G^{1 / 2},$ $H (I + G H)^{- 1} = (I + H G)^{- 1} H = H^{1 / 2} (I + H^{1 / 2} G H^{1 / 2})^{- 1} H^{1 / 2}$ follow by multiplication and the push-through identity. Their middle matrices are positive definite, so both displayed products are Hermitian positive semidefinite. Therefore the updates in [F1] give $G_{1}, H_{1} ⪰ 0$ and use only an inverse already proved to exist.

1.2F1F2algebra

For any invertible displayed factors, direct multiplication gives the resolvent identity $Φ_{G} (X) - Φ_{G} (Y) = (I + X G)^{- 1} (X - Y) (I + G Y)^{- 1},$ and the push-through identity $(I + U V)^{- 1} U = U (I + V U)^{- 1}$ . For $X ≻ 0$ , $Φ_{G} (X)^{- 1} = X^{- 1} + G$ . Put $U = Φ_{G} (X)$ and $Y = A^{*} U A$ . Applying the resolvent identity at $H + Y$ and $H$ gives $Φ_{G} (H + Y) - Φ_{G} (H) = (I + (H + Y) G)^{- 1} Y (I + G H)^{- 1} .$ Since $I + (H + Y) G = (I + H G) + Y G$ , multiplication verifies $(I + (H + Y) G)^{- 1} Y = (I + H G)^{- 1} Y (I + G (I + H G)^{- 1} Y)^{- 1} .$ Substituting $Y = A^{*} U A$ and applying push-through twice rewrites this difference as $(I + H G)^{- 1} A^{*} (U^{- 1} + A G (I + H G)^{- 1} A^{*})^{- 1} A (I + G H)^{- 1} .$ Using $U^{- 1} = X^{- 1} + G$ and [F1], the middle inverse is $X (I + G_{1} X)^{- 1}$ . Now $f (f (X)) - H_{1} = A^{*} (Φ_{G} (H + Y) - Φ_{G} (H)) A$ . Its left factor is $A^{*} (I + H G)^{- 1} A^{*} = A_{1}^{*}$ and its right factor is $A (I + G H)^{- 1} A = A_{1}$ . Adding $H_{1} = H + A^{*} Φ_{G} (H) A$ proves the composition formula for $X ≻ 0$ .

2.1F1step 1.1step 1.2inductionalgebra∎

For singular $X ⪰ 0$ , replace it by $X + ε I$ in step 1.2 and let $ε ↓ 0$ . Step 1.1 guarantees every $I + G (X + ε I)$ and $I + G_{1} (X + ε I)$ is invertible; matrix inversion is continuous at these invertible limits. Hence the composition identity extends to every $X ⪰ 0$ , including singular $A$ and singular $X$ . By induction on $j$ , the updated Riccati map is $f^{2^{j}}$ and its value at zero is $H_{j}$ .

Depends on

Used by

Cited to discharge well-definedness by Finite-budget structure-preserving doubling iteration for the DARE.

Dependency tree · two levels

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