TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Stabilizability and detectability give the unique stabilizing positive-semidefinite DARE solution

Statement

Let $A \in F^{n \times n}$ , $B \in F^{n \times m}$ , $C \in F^{p \times n}$ , $R = R^{*} ≻ 0$ , and $Q = C^{*} C$ . Assume $(A, B)$ is discretely stabilizable and $(A, C)$ discretely detectable, using Stabilizability and detectability for continuous and discrete linear systems. Then the DARE of Standard CARE and DARE data, equations, and conventions has exactly one Hermitian positive-semidefinite solution $X$ . For the equivalent Riccati map $f (P) = Q + A^{*} P (I + G P)^{- 1} A$ , its finite-horizon iterates $P_{0} = 0$ , $P_{k + 1} = f (P_{k})$ satisfy $0 ⪯ P_{k} ↑ X$ . For all Hermitian positive-semidefinite $Y, Z$ , $f (Y) - f (Z) = A_{c} (Y)^{*} (Y - Z) A_{c} (Z), A_{c} (Y) = (I + G Y)^{- 1} A .$ The solution satisfies $R + B^{*} X B ≻ 0$ , and its closed loop $A_{c} = A - B (R + B^{*} X B)^{- 1} B^{*} X A$ is Schur stable. For each $x_{0}$ , the infinite-horizon discrete cost $\inf_{(u_{k})} \sum_{k = 0}^{\infty} (x_{k}^{*} Q x_{k} + u_{k}^{*} R u_{k}), x_{k + 1} = A x_{k} + B u_{k},$ over sequences with finite cost equals $x_{0}^{*} X x_{0}$ and is attained by $u_{k} = - K_{d} x_{k}$ . Singular $A$ is allowed throughout; no inverse of $A$ is used.

Facts & Assumptions

Given: The finite matrices in the statement, discrete stabilizability/detectability, $R ≻ 0$ , $Q = C^{*} C$ , and the discrete-time dynamics.

[F1]

Stabilizability and detectability for continuous and discrete linear systems: discrete stabilizability/detectability mean there exist a feedback/injection making the corresponding matrix Schur stable.

[F2]

Standard CARE and DARE data, equations, and conventions: $G = B R^{- 1} B^{*}$ and the DARE residual and feedback are defined there.

[F3]

Powers of a Schur-stable matrix decay geometrically up to a polynomial factor: if $M$ is Schur stable, then for any $r$ with $ρ (M) < r < 1$ , $∥ M^{k} ∥_{2} \leq C_{r} r^{k}$ .

[F4]

A matrix admits a Cholesky factorisation with positive diagonal exactly when it is Hermitian positive definite, and that factor is unique: $R ≻ 0$ gives an invertible factor $R = L L^{*}$ .

[F5]

A non-negative operator has a unique non-negative square root: if $P ⪰ 0$ and $v^{*} P v = 0$ , then $P v = 0$ .

[F6]

Rank-nullity: $\dim_{F} V = nullity T + rank T$ : an injective endomorphism of a finite-dimensional space is invertible.

Proof

1.1F2F4algebrainduction

Define $P_{0} = 0$ and recursively $S_{j} = R + B^{*} P_{j} B, K_{j} = S_{j}^{- 1} B^{*} P_{j} A, P_{j + 1} = Q + A^{*} P_{j} A - A^{*} P_{j} B S_{j}^{- 1} B^{*} P_{j} A .$ If $P_{j} ⪰ 0$ , then for nonzero $v$ , $v^{*} S_{j} v = v^{*} R v + (B v)^{*} P_{j} (B v) > 0$ , so $S_{j}^{- 1}$ exists. For each $x, u$ , expansion and completion of the positive square gives $x^{*} Q x + u^{*} R u + (A x + B u)^{*} P_{j} (A x + B u) = x^{*} P_{j + 1} x + (u + K_{j} x)^{*} S_{j} (u + K_{j} x) .$ Thus $x^{*} P_{j + 1} x$ is the finite-horizon value for $j + 1$ stages, attained by the minimizing first control; induction gives $P_{j} ⪰ 0$ .

1.2F2F5F6algebra

For positive-semidefinite $P, Q$ , if $(I + P Q) v = 0$ , multiplication by $v^{*} Q$ gives $v^{*} Q v + (Q v)^{*} P (Q v) = 0$ . Both terms are nonnegative, so [F5] gives $Q v = 0$ and then $v = 0$ . Interchanging $P, Q$ proves the same for $I + Q P$ . Thus $I + Y G$ , $I + G Y$ , $I + G Z$ , and $I + Z G$ are injective and hence invertible by [F6]. Since $(I + Y G) Y = Y (I + G Y)$ , multiplication by the established inverses gives $(I + Y G)^{- 1} Y = Y (I + G Y)^{- 1}$ . Further, multiplying both sides of $Y (I + G Y)^{- 1} - Z (I + G Z)^{- 1} = (I + Y G)^{- 1} (Y - Z) (I + G Z)^{- 1}$ by $I + Y G$ on the left and $I + G Z$ on the right reduces both sides to $Y - Z$ . Substitution into $f (Y) - f (Z)$ proves the difference identity in the Statement.

2.1F1F3step 1.1algebra

Longer horizons add nonnegative stage costs, so their value matrices increase in the Loewner order: $0 ⪯ P_{j} ⪯ P_{j + 1}$ . By stabilizability [F1], choose $K_{0}$ so $A_{0} = A - B K_{0}$ is Schur stable. Under that fixed feedback the cost is bounded by $\sum_{k \geq 0} (∥ C ∥_{2}^{2} + ∥ K_{0}^{*} R K_{0} ∥_{2}) ∥ A_{0}^{k} x_{0} ∥_{2}^{2} \leq c ∥ x_{0} ∥_{2}^{2},$ because [F3] gives a summable geometric-square bound. Therefore $P_{j} ⪯ c I$ . The forms on $e_{i}$ , $e_{i} + e_{j}$ , and $e_{i} + i e_{j}$ are bounded and monotone; they determine the diagonal entries and the real and imaginary parts of each Hermitian off-diagonal entry. Thus all entries converge to a Hermitian $X ⪰ 0$ .

3.1F2F4step 1.1step 2.1algebra

The update map is continuous on $P ⪰ 0$ : $R + B^{*} P B ⪰ R ≻ 0$ , so its inverse varies continuously there. Passing to the limit in step 1.1 gives the DARE for $X$ , and the same inequality gives $R + B^{*} X B ≻ 0$ .

4.1F1F2step 1.1step 3.1algebra

Put $S = R + B^{*} X B$ , $K = S^{- 1} B^{*} X A$ , and $A_{c} = A - B K$ . The square identity in step 1.1 with $P_{j} = X$ yields $x^{*} Q x + u^{*} R u + (A x + B u)^{*} X (A x + B u) - x^{*} X x = (u + K x)^{*} S (u + K x) .$ For $u = - K x$ , summing from $k = 0$ to $N - 1$ gives total stage cost $x_{0}^{*} X x_{0} - x_{N}^{*} X x_{N} \leq x_{0}^{*} X x_{0}$ . Thus $u, C x \in ℓ^{2}$ .

5.1F1F3step 4.1algebracontradiction

By detectability [F1], choose $L$ such that $A_{o} = A - L C$ is Schur stable. Along the feedback trajectory, $x_{k + 1} = A_{o} x_{k} + w_{k}, w_{k} = B u_{k} + L C x_{k} \in ℓ^{2} .$ Variation of constants gives $x_{k} = A_{o}^{k} x_{0} + \sum_{j = 0}^{k - 1} A_{o}^{k - 1 - j} w_{j}$ . The first term tends to zero by [F3]. For any fixed $J$ , the finite sum over $j < J$ also tends to zero. The remaining sum is bounded by $(\sum_{ℓ \geq 0} ∥ A_{o}^{ℓ} ∥_{2}^{2})^{1 / 2} (\sum_{j \geq J} ∥ w_{j} ∥_{2}^{2})^{1 / 2} .$ The first factor is finite by [F3], and the second tends to zero as $J \to \infty$ . Hence $x_{k} \to 0$ . This holds for every initial state, so no eigenvalue of $A_{c}$ can satisfy $∣ λ ∣ \geq 1$ ; therefore $A_{c}$ is Schur stable.

6.1F1F2step 4.1step 5.1algebra

For any finite-cost control, $u, C x \in ℓ^{2}$ ; the same detectability argument in step 5.1, now with its state equation, gives $x_{k} \to 0$ . Summing the square identity in step 4.1 and taking $N \to \infty$ gives cost at least $x_{0}^{*} X x_{0}$ . The stabilizing feedback makes the square term zero and has $x_{N} \to 0$ , so it attains equality.

7.1F2F3step 5.1step 1.2algebra∎

Let $Y ⪰ 0$ be another DARE solution. Step 5.1 applied to $Y$ shows its closed loop $A_{Y} = (I + G Y)^{- 1} A$ is Schur stable. Since both $X$ and $Y$ are fixed points, step 1.2 gives $X - Y = A_{c} (X)^{*} (X - Y) A_{Y}$ . Iteration yields $X - Y = (A_{c} (X)^{*})^{k} (X - Y) A_{Y}^{k}$ . By [F3], both powers tend to zero, so the right side tends to zero and $X = Y$ .

Depends on

Used by

Dependency tree · two levels

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