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

One-step Gaussian prediction and conditioning

Statement

Assume AC, and let $d, n, p$ be positive integers. Let $U \in R^{d}$ , $q \in R^{n}$ , and $r \in R^{p}$ be mutually independent Gaussian vectors with $U \sim N_{d} (m, P), q \sim N_{n} (0, Q), r \sim N_{p} (0, R),$ where $P, Q, R$ are symmetric positive semidefinite. Let $F \in R^{n \times d}$ and $H \in R^{p \times n}$ , and set $X = F U + q, Y = H X + r, P^{-} : = F P F^{T} + Q, S : = H P^{-} H^{T} + R .$ If $S$ is positive definite, put $K : = P^{-} H^{T} S^{- 1}$ . Then $(X, Y)$ is jointly Gaussian with mean $(F m, H F m)$ and covariance $(\begin{array}{cc} P^{-} & P^{-} H^{T} \\ H P^{-} & S \end{array}),$ and for every $y \in R^{p}$ an everywhere-defined conditional law is $L (X ∣ Y = y) = N_{n} ⁣ (F m + K (y - H F m), P^{-} - K S K^{T}) .$ The conditional covariance is positive semidefinite even if $P$ , $Q$ , or $R$ is singular. It also equals the Joseph expression $(I - K H) P^{-} (I - K H)^{T} + K R K^{T} .$ No inverse of a state, process-noise, or measurement-noise covariance is used.

Facts & Assumptions

Given: AC, mutually independent Gaussian vectors and the matrices in the Statement, with $P, Q, R$ positive semidefinite and $S$ positive definite.

[A1]

AC is used by the multivariate-normal and conditional-Gaussian suppliers. The Axiom of Choice.

[F1]

A multivariate normal law is defined for every symmetric positive-semidefinite covariance, including singular ones, and its linear projections have the corresponding scalar normal laws. Multivariate normal law, including singular covariance.

[F2]

A finite stack of mutually independent Gaussian vectors is jointly Gaussian with block-diagonal covariance; no block must be invertible. A finite stack of independent Gaussian vectors is jointly Gaussian.

[F3]

Every finite-dimensional positive-semidefinite operator has a unique positive-semidefinite square root. A non-negative operator has a unique non-negative square root.

[F4]

For a jointly Gaussian pair with positive-semidefinite block covariance and positive-definite observed block $B$ , the everywhere-defined conditional law has mean $a + C B^{- 1} (y - b)$ and covariance $A - C B^{- 1} C^{T}$ , which is positive semidefinite; the state covariance may be singular. Conditional law of a jointly Gaussian block with positive-definite observed covariance.

Proof

Given: The hypotheses in the Statement.

1.1A1F1F2F3givenalgebra

By [F2], the stack $(U, q, r)$ is jointly Gaussian with mean $(m, 0, 0)$ and covariance $diag (P, Q, R)$ . For any $a \in R^{n}$ and $b \in R^{p}$ , the scalar $a^{T} X + b^{T} Y$ is a linear projection of this stack, so it is normal by [F1]; thus $(X, Y)$ is jointly Gaussian. Since $q$ is independent of $U$ and centered, $Cov (X) = F Cov (U) F^{T} + Cov (q) = F P F^{T} + Q = P^{-}$ . Since $Y = H X + r$ and $r$ is independent of $X$ and centered, $E X = F m$ , $E Y = H F m$ , $Cov (X, Y) = P^{-} H^{T}$ , and $Cov (Y) = H P^{-} H^{T} + R = S$ . Hence the block covariance is the one displayed in the Statement and is positive semidefinite as a covariance matrix. Also $P^{-} ⪰ 0$ , since $u^{T} P^{-} u = (F^{T} u)^{T} P (F^{T} u) + u^{T} Q u \geq 0$ for every $u$ .

2.1F4givenstep 1.1algebra

Apply [F4] with $A = P^{-}$ , $C = P^{-} H^{T}$ , and $B = S$ . The observed block is positive definite by hypothesis, and the joint block is positive semidefinite by step 1.1. The conditional mean is $F m + P^{-} H^{T} S^{- 1} (y - H F m) = F m + K (y - H F m)$ . Its covariance is $P^{-} - P^{-} H^{T} S^{- 1} H P^{-} = P^{-} - K S K^{T}$ , and [F4] makes it positive semidefinite and gives a conditional-law version for every $y$ .

3.1F1F4step 1.1step 2.1algebra∎

Since $S = H P^{-} H^{T} + R$ and $K = P^{-} H^{T} S^{- 1}$ , symmetry of $P^{-}$ and $S$ gives $K H P^{-} = P^{-} H^{T} K^{T} = K S K^{T}$ . Expanding the Joseph expression yields $P^{-} - K H P^{-} - P^{-} H^{T} K^{T} + K (H P^{-} H^{T} + R) K^{T} = P^{-} - K S K^{T}$ . It is positive semidefinite because [F4] gives that covariance this property; independently, the Joseph expression is a sum of positive-semidefinite matrices. This proves the identity without inverting $P$ , $Q$ , or $R$ .

Depends on

Used by

Dependency tree · two levels

26 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

Simo Särkkä, Bayesian Filtering and Smoothing, Chapter 4, §4.3 and Appendix A.1 (standard reference, not scraped)
Kody Law, Andrew M. Stuart, and Konstantinos Zygalakis, Data Assimilation: A Mathematical Introduction, Chapter 4, §4.1 (standard reference, not scraped)