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

Verified Lyapunov residual, descent, and stability checks make an inexact Newton-Kleinman step safe

Statement

Consider a trial gain $K_{t}$ in the safeguarded-inexact branch of Finite-budget exact or safeguarded inexact Newton-Kleinman policy iteration, with $A_{t} = A - B K_{t}$ . Suppose outward certificates give $W ≻ 0$ , $μ > 0$ , $A_{t}^{*} W + W A_{t} ⪯ - μ I$ , an inverse bound $κ \geq ∥ L_{A_{t}}^{- 1} ∥_{F \to F}$ , a residual bound $r$ for a Hermitian approximation $\tilde{P}$ to $A_{t}^{*} P + P A_{t} + Q + K_{t}^{*} R K_{t} = 0,$ and an upper bound $η \geq λ_{\max} (\tilde{P} - X_{j})$ with $η + κ r \leq 0$ . Then $A_{t}$ is Hurwitz, its exact cost matrix $P_{t}$ exists and is positive semidefinite, and $P_{t} ⪯ X_{j}$ . Thus every accepted line-search step preserves stability and does not increase the exact closed-loop cost matrix.

Facts & Assumptions

Given: The current exact cost matrix $X_{j}$ , trial gain, residual data, and verified bounds in the statement.

[F1]

Finite-budget exact or safeguarded inexact Newton-Kleinman policy iteration: a trial is accepted only if its Lyapunov margin, inverse bound, residual bound, and descent upper bound satisfy the stated tests.

[F2]

Standard CARE and DARE data, equations, and conventions: $Q = C^{*} C ⪰ 0$ and $R ≻ 0$ .

[F3]

The Hurwitz Lyapunov integral is the unique solution and has the stated positivity: for Hurwitz $A_{t}$ , the solution of $A_{t}^{*} P + P A_{t} + S = 0$ is the unique integral $\int_{0}^{\infty} e^{t A_{t}^{*}} S e^{t A_{t}} d t$ , and is positive semidefinite for $S ⪰ 0$ .

[F4]

A Sylvester equation is uniquely solvable exactly when the spectra are disjoint: when $A_{t}$ is Hurwitz, the Lyapunov operator $E \mapsto A_{t}^{*} E + E A_{t}$ is invertible.

[F5]

Verified point and uniform linear residual certificate data specifies bounds for an approximate-inverse defect and a preconditioned linear residual, with a usable certificate requiring $q < 1$ . The raw Lyapunov residual bound $r$ and inverse-norm bound $κ$ in this proposition are separate hypotheses of the Statement.

Proof

1.1F1givenalgebra

If $A_{t} v = λ v$ with $v \neq 0$ , the certificate gives $2 Re (λ) v^{*} W v = v^{*} (A_{t}^{*} W + W A_{t}) v \leq - μ ∥ v ∥_{2}^{2} < 0.$ Because $W ≻ 0$ , every eigenvalue has negative real part, so $A_{t}$ is Hurwitz.

2.1givenF1F2F3F4F5step 1.1algebra∎

Let $P_{t}$ be the exact solution of the Lyapunov equation; it exists uniquely by [F3] and [F4], and $P_{t} ⪰ 0$ by [F2]–[F3]. If $R_{t}$ denotes the exact residual of $\tilde{P}$ , then $L_{A_{t}} (\tilde{P} - P_{t}) = R_{t}$ . The Statement's certified inverse and raw residual bounds give $∥ \tilde{P} - P_{t} ∥_{F} \leq κ r$ ; these are distinct from the certificate quantities described in [F5]. For each unit vector $v$ , $v^{*} (P_{t} - X_{j}) v \leq v^{*} (\tilde{P} - X_{j}) v + ∥ P_{t} - \tilde{P} ∥_{2} \leq η + κ r \leq 0.$ Thus $P_{t} ⪯ X_{j}$ .

Depends on

Used by

Exact Newton-Kleinman decreases the cost while an unchecked inexact step can lose stability Example

Dependency tree · two levels

41 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

Peter Benner and Lihong Feng, Model Reduction for Dynamical Systems, Lecture 8 (standard reference, not scraped)
Daniel Liberzon, Calculus of Variations and Optimal Control Theory: A Concise Introduction, Chapter 6 (standard reference, not scraped)