LemmaStatement: AI-adaptedProof: AI-generatedPipeline-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 block QR measurement update gives the canonical Kalman update

Statement

Let $P^{-} = L^{-} (L^{-})^{T}$ and $R = L_{R} L_{R}^{T}$ , with real factors of arbitrary rank. Let $H \in R^{p \times n}$ and suppose $S = H P^{-} H^{T} + R ≻ 0.$ Pad $L_{R}$ with zero columns to at least $p$ columns and $L^{-}$ with zero columns to at least $n$ columns. Denote the resulting factors by $L_{R}^{p a d}$ and $L_{p a d}^{-}$ , and form $Z = [\begin{array}{cc} L_{R}^{p a d} & H L_{p a d}^{-} \\ 0 & L_{p a d}^{-} \end{array}] .$ Then $Z^{T}$ has at least $p + n$ rows. Take an exact reduced QR factorization $Z^{T} = U R$ with $U^{T} U = I$ and set $L = R^{T}$ . For each $i = 1, \dots, p$ , multiply column $i$ of $L$ by the sign of its diagonal entry. This makes the first $p$ diagonal entries positive; the signs are well defined because $S ≻ 0$ . Partition the resulting $L$ as $L = [\begin{array}{cc} L_{11} & 0 \\ L_{21} & L_{22} \end{array}]$ at the observation and state dimensions. Then $L_{11} L_{11}^{T} = S, L_{21} L_{11}^{T} = P^{-} H^{T},$ and $L_{22} L_{22}^{T} = P^{-} - P^{-} H^{T} S^{- 1} H P^{-} .$ For innovation $v = y - H m^{-}$ , the exact solve $L_{11} z = v$ gives $m^{-} + L_{21} z = m^{-} + P^{-} H^{T} S^{- 1} v$ . Thus the factor update has exactly the canonical one-step mean and covariance; $L_{22}$ may be singular.

Facts & Assumptions

Given: AC, the real covariance factors and matrices, positive-definite innovation $S$ , and exact QR of the padded prearray.

[A1]

AC is the choice assumption of the Gaussian conditional-law supplier; the block-matrix identities below add no choice. The Axiom of Choice

[F1]

For a real matrix with at least as many rows as columns, exact successive Householder QR gives $Z^{T} = U R$ with $U^{T} U = I$ ; rank deficiency is permitted. Successive Householder or Givens transformations produce full and reduced QR factorisations with the standard dense operation counts

[F2]

Under AC, let $U \sim N_{d} (m, P)$ , $q \sim N_{n} (0, Q)$ , and $r \sim N_{p} (0, R)$ be mutually independent Gaussian vectors, with positive dimensions and positive-semidefinite covariances. Set $X = F U + q$ , $Y = H X + r$ , $m^{-} = F m$ , and $P^{-} = F P F^{T} + Q$ . If $S = H P^{-} H^{T} + R$ is positive definite, the everywhere-defined conditional law of $X$ given $Y = y$ has mean $m^{-} + P^{-} H^{T} S^{- 1} (y - H m^{-})$ and covariance $P^{-} - P^{-} H^{T} S^{- 1} H P^{-}$ , which also equals the Joseph expression. One-step Gaussian prediction and conditioning

Proof

Given: The hypotheses in the Statement.

1.1givenalgebra

Write ${\overset{ˉ}{r}}_{R}$ and ${\overset{ˉ}{r}}_{-}$ for the padded column counts. They satisfy ${\overset{ˉ}{r}}_{R} \geq p$ and ${\overset{ˉ}{r}}_{-} \geq n$ , so $Z^{T}$ has ${\overset{ˉ}{r}}_{R} + {\overset{ˉ}{r}}_{-} \geq p + n$ rows, as required for the reduced QR. Padding either factor with zero columns leaves its Gram matrix unchanged. Multiplication of the prearray by its transpose therefore gives $Z Z^{T} = [\begin{array}{cc} L_{R}^{p a d} (L_{R}^{p a d})^{T} + H L_{p a d}^{-} (L_{p a d}^{-})^{T} H^{T} & H L_{p a d}^{-} (L_{p a d}^{-})^{T} \\ L_{p a d}^{-} (L_{p a d}^{-})^{T} H^{T} & L_{p a d}^{-} (L_{p a d}^{-})^{T} \end{array}] = [\begin{array}{cc} S & H P^{-} \\ P^{-} H^{T} & P^{-} \end{array}] .$

2.1F1step 1.1algebra

Initially set $L^{0} = R^{T}$ and partition it at dimensions $p, n$ . Since $Z^{T} = U R$ and $U^{T} U = I$ , $L^{0} (L^{0})^{T} = R^{T} R = Z Z^{T}$ . Block multiplication gives $L_{11}^{0} (L_{11}^{0})^{T} = S$ , $L_{21}^{0} (L_{11}^{0})^{T} = P^{-} H^{T}$ , and $L_{21}^{0} (L_{21}^{0})^{T} + L_{22}^{0} (L_{22}^{0})^{T} = P^{-}$ . The positive-definite matrix $S = L_{11}^{0} (L_{11}^{0})^{T}$ makes $L_{11}^{0}$ invertible, so its diagonal entries are nonzero. Let $D$ be the diagonal matrix whose entries are the signs of those entries, and set $L = L^{0} diag (D, I_{n})$ . This flips the first $p$ columns of $L^{0}$ , making the diagonal of $L_{11} = L_{11}^{0} D$ positive. Because $diag (D, I_{n})$ is orthogonal, $L L^{T} = L^{0} (L^{0})^{T}$ ; moreover $L_{21} = L_{21}^{0} D$ and $L_{22} = L_{22}^{0}$ . Hence all three displayed block identities remain true.

3.1givenstep 2.1algebra

Because $S ≻ 0$ and $S = L_{11} L_{11}^{T}$ , the square matrix $L_{11}$ is invertible. From the cross-block identity, $L_{21} = P^{-} H^{T} L_{11}^{- T}$ ; hence $L_{21} L_{21}^{T} = P^{-} H^{T} L_{11}^{- T} L_{11}^{- 1} H P^{-} = P^{-} H^{T} S^{- 1} H P^{-} .$ Subtracting this equality from the lower-right identity in step 2.1 gives the stated posterior covariance. Since it is also $L_{22} L_{22}^{T}$ , it is positive semidefinite even when $L_{22}$ is singular.

4.1A1F2step 2.1step 3.1givenalgebra∎

The solve $L_{11} z = v$ gives $L_{21} z = L_{21} L_{11}^{- 1} v = P^{-} H^{T} L_{11}^{- T} L_{11}^{- 1} v = P^{-} H^{T} S^{- 1} v .$ When $n, p \geq 1$ and these blocks arise in a model satisfying [F2], these are its one-step Gaussian conditional update formulas; for zero-dimensional blocks this lemma asserts only the matrix identities. The matrix calculations themselves are deterministic and use no choice beyond [A1].

Depends on

Used by

Dependency tree · two levels

11 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)
Simo Särkkä, Bayesian Filtering and Smoothing (standard reference, not scraped)