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

An innovation solve residual gives a singular-value forward bound

Statement

Let $p \geq 1$ and $T \in R^{p \times p}$ be nonsingular, define

σ_{\min} (T) : = \min_{∥ x ∥_{2} = 1} ∥ T x ∥_{2},

and let $z_{*} = T^{- 1} y$ . For any computed vector $\hat{z}$ with residual $r = T \hat{z} - y$ ,

∥ \hat{z} - z_{*} ∥_{2} \leq \frac{∥ r ∥_{2}}{σ_{\min} (T)} .

If $S = T T^{T}$ also satisfies $x^{T} S x \geq ν ∥ x ∥_{2}^{2}$ for all $x$ , with $ν > 0$ , then $σ_{\min} (T) \geq \sqrt{ν}$ and therefore

∥ \hat{z} - z_{*} ∥_{2} \leq \frac{∥ r ∥_{2}}{\sqrt{ν}} .

Facts & Assumptions

Given: The real nonsingular matrix $T$ , vector $y$ , computed vector $\hat{z}$ , and, for the second bound, the stated quadratic lower bound $ν > 0$ .

[F1]

The operator norm is the maximum Euclidean stretch on unit vectors. The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||

[F2]

For every linear map $A$ , $∥ A^{T} A ∥_{2} = ∥ A ∥_{2}^{2}$ . The operator norm is submultiplicative and satisfies ||T^*T|| = ||T||^2

[F3]

Euclidean inner products satisfy $∣ x^{T} y ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ . Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs

Proof

Given: The hypotheses in the Statement.

1.1F1givenalgebra

Set $M = ∥ T^{- 1} ∥_{2}$ . For any vector $w$ , $∥ w ∥_{2} = ∥ T^{- 1} T w ∥_{2} \leq M ∥ T w ∥_{2}$ by the operator norm definition. Thus $∥ T w ∥_{2} \geq ∥ w ∥_{2} / M$ .

1.2F3givenalgebra

Suppose $S = T T^{T}$ has the stated lower bound. If $b = S x$ , then $ν ∥ x ∥_{2}^{2} \leq x^{T} S x = x^{T} b \leq ∥ x ∥_{2} ∥ b ∥_{2}$ by [F3]. For $x \neq 0$ this yields $∥ S^{- 1} b ∥_{2} \leq ∥ b ∥_{2} / ν$ ; it is also true for $x = 0$ . Thus $∥ S^{- 1} ∥_{2} \leq 1 / ν$ .

2.1F1step 1.1givenalgebra

Since $p \geq 1$ and $T^{- 1}$ is invertible, $M > 0$ . By [F1], the maximum defining $M$ is attained at a unit vector $u$ . Set $v = T^{- 1} u / M$ . Then $∥ v ∥_{2} = 1$ and $∥ T v ∥_{2} = 1 / M$ . Combining this with step 1.1 shows that the minimum in the definition of $σ_{\min} (T)$ exists and equals $1 / M$ .

3.1step 1.1step 2.1givenalgebra

Since $T z_{*} = y$ , $r = T (\hat{z} - z_{*})$ . Step 1.1 gives $∥ \hat{z} - z_{*} ∥_{2} \leq M ∥ r ∥_{2}$ , and step 2.1 gives $M = 1 / σ_{\min} (T)$ . This proves the first residual bound.

4.1F2step 2.1step 3.1step 1.2algebra∎

Since $(T^{- 1})^{T} T^{- 1} = (T T^{T})^{- 1} = S^{- 1}$ , [F2] and step 1.2 give $∥ T^{- 1} ∥_{2}^{2} = ∥ S^{- 1} ∥_{2} \leq 1 / ν .$ Step 2.1 then yields $σ_{\min} (T) = 1 / ∥ T^{- 1} ∥_{2} \geq \sqrt{ν}$ . Substituting this lower bound into step 3.1 proves the final residual estimate.

Depends on

Used by

The square-root filter has an explicit conditioned finite-horizon error bound Theorem

Dependency tree · two levels

12 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

Kevin S. Tracy, A Square-Root Kalman Filter Using Only QR Decompositions (standard reference, not scraped)
M. A. Salzmann, Some Aspects of Kalman Filtering, Technical Report 140 (standard reference, not scraped)