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.

The backward Gaussian kernel remains valid after future observations

Statement

Assume AC. Let $(X_{0}, \dots, X_{T}, Y_{1}, \dots, Y_{T})$ follow a finite-horizon linear-Gaussian model as in Linear-Gaussian state-space models with independent noises. Suppose the Kalman filter of Exact linear-Gaussian Kalman filter is admissible: every innovation covariance $S_{j}$ it solves is positive definite. Fix $0 \leq k < T$ , and let $m_{k ∣ k}, P_{k ∣ k}$ and $m_{k + 1 ∣ k}, P_{k + 1 ∣ k}$ be the corresponding filtered and one-step predicted quantities. Assume in addition that $P_{k + 1 ∣ k} ≻ 0$ . Put $C_{k} = P_{k ∣ k} F_{k + 1}^{T} P_{k + 1 ∣ k}^{- 1}, V_{k} = P_{k ∣ k} - C_{k} P_{k + 1 ∣ k} C_{k}^{T} .$ Then $V_{k} ⪰ 0$ , and the formula $Q_{k} (y_{1 : k}, x_{k + 1}, \cdot) = N ⁣ (m_{k ∣ k} (y_{1 : k}) + C_{k} (x_{k + 1} - m_{k + 1 ∣ k} (y_{1 : k})), V_{k})$ defines an everywhere probability kernel. It is a conditional law of $X_{k}$ given $(Y_{1 : k}, X_{k + 1})$ and also a version of the conditional law of $X_{k}$ given $(Y_{1 : T}, X_{k + 1})$ under the full finite-horizon model. Thus future observations do not change this backward kernel once $X_{k + 1}$ is also given. The inverse is the ordinary inverse of the positive-definite forecast covariance; no singular-forecast extension is asserted.

Facts & Assumptions

Given: AC, the finite-horizon model in the Statement, admissible filter histories, and $P_{k + 1 ∣ k} ≻ 0$ .

[A1]

AC is the Axiom of Choice assumed by the Gaussian-law and conditional-Gaussian suppliers. The Axiom of Choice.

[F1]

The model has affine state and observation equations; its initial, process, and measurement Gaussian vectors are mutually independent, and the process covariance $Q_{k + 1}$ is positive semidefinite. Linear-Gaussian state-space models with independent noises.

[F2]

The Kalman algorithm predicts $m_{k + 1 ∣ k} = F_{k + 1} m_{k ∣ k}$ and $P_{k + 1 ∣ k} = F_{k + 1} P_{k ∣ k} F_{k + 1}^{T} + Q_{k + 1}$ . Exact linear-Gaussian Kalman filter.

[F3]

For every observation history, the filtered law of $X_{k}$ is the probability kernel $N (m_{k ∣ k}, P_{k ∣ k})$ ; its covariance is positive semidefinite. The finite-horizon linear-Gaussian Kalman filter is exact.

[F4]

An independent process noise extends the supplied filtering kernel to the joint conditional law, and measurable pushforwards remain conditional laws. Independent noise extends and pushes forward a conditional law.

[F5]

A finite independent stack of Gaussian vectors is jointly Gaussian even when covariance blocks are singular. A finite stack of independent Gaussian vectors is jointly Gaussian.

[F6]

For a jointly Gaussian pair with positive-semidefinite block covariance and positive-definite observed covariance $B$ , the everywhere conditional kernel is Gaussian with the Schur-complement covariance, which is positive semidefinite. Conditional law of a jointly Gaussian block with positive-definite observed covariance.

[F7]

The finite linear-Gaussian path law is the ordered product of its transition and observation kernels. The finite linear-Gaussian state-space path is jointly Gaussian.

[F8]

Integration of a nonnegative product-measurable function against a finite probability kernel is measurable in its parameter. Measurability of integration against a kernel.

[F9]

A data-indexed state-space conditional law is an everywhere probability kernel whose composition with the data vector is an RCD; its values on null-data sets may vary. Filtering, predictive, and smoothing laws in a finite-horizon state-space model.

[F10]

Under AC, $N_{d} (m, P)$ is defined for every finite-dimensional symmetric positive-semidefinite $P$ , including singular $P$ . Multivariate normal law, including singular covariance.

Proof

Given: The hypotheses in the Statement.

1.1A1F1F2F3F4F5F6F8F10givenalgebra

Fix a history $h = y_{1 : k}$ . By [F3], the conditional law of $X_{k}$ is $N (m_{k ∣ k} (h), P_{k ∣ k})$ . The next process noise is independent of the past by [F1], so [F4] extends this filtering kernel by $q_{k + 1}$ and pushes it forward through $(x, q) \mapsto (x, F_{k + 1} x + q)$ . By [F5], $(X_{k}, q_{k + 1})$ is jointly Gaussian, and the projection characterization in [F10] makes its linear image $(X_{k}, X_{k + 1})$ jointly Gaussian. Its mean is $(m_{k ∣ k}, F_{k + 1} m_{k ∣ k})$ , its state covariance is $P_{k ∣ k}$ , its cross-covariance is $P_{k ∣ k} F_{k + 1}^{T}$ , and its next-state covariance is $P_{k + 1 ∣ k}$ . The latter block is positive definite by hypothesis. Apply [F6] with that observed block: the conditional mean and covariance are exactly the displayed $Q_{k}$ parameters, so $V_{k} ⪰ 0$ . The history mean is affine by [F2], and representing each Gaussian section as a translate of fixed $N (0, V_{k})$ plus [F8] gives joint measurability in $(h, x_{k + 1})$ . Thus $Q_{k}$ is an everywhere probability kernel.

2.1F1F3F4F7F8F9step 1.1construct

Write $H = Y_{1 : k}$ , $V = X_{k + 1}$ , and $Z = Y_{k + 1 : T}$ . By [F7], the full path law factors by taking the law of $(H, X_{k})$ , applying the transition kernel at $k + 1$ , and then a future observation kernel $R (V, d z)$ formed by the remaining transition and observation kernels. The first two factors disintegrate as $π_{k} (h, d x_{k}) K_{k + 1} (x_{k}, d v) = ρ_{k} (h, d v) Q_{k} (h, v, d x_{k})$ by step 1.1, where $ρ_{k}$ is the one-step predictive law. Substitution gives the joint factorization as the law of $H$ followed by $ρ_{k}$ , $Q_{k}$ , and $R$ . The future kernel depends on the past only through $V$ , and its iterated integrals are measurable by [F8].

3.1F7F8F9step 1.1step 2.1algebra∎

For any Borel set $A$ of $X_{k}$ and any Borel set $D$ in the product space of $(H, V, Z)$ , integrate $1_{A} (x_{k}) 1_{D} (h, v, z)$ in the factorization from step 2.1. This gives $P (X_{k} \in A, (H, V, Z) \in D) = \int_{D} Q_{k} (h, v, A) P_{(H, V, Z)} (d h, d v, d z)$ . This is the RCD event identity for $Q_{k}$ given $(H, V, Z)$ ; its kernel properties were established in step 1.1. Since $(H, Z) = Y_{1 : T}$ , it is also a version of the conditional law given $(Y_{1 : T}, X_{k + 1})$ . The factorization uses model kernels rather than observation densities, and the only inverse is of $P_{k + 1 ∣ k} ≻ 0$ .

Depends on

Used by

The Rauch–Tung–Striebel recursion gives fixed-interval Gaussian smoothing laws Theorem

Dependency tree · two levels

50 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 8, §§8.1–8.2 (standard reference, not scraped)
Kody Law, Andrew M. Stuart, and Konstantinos Zygalakis, Data Assimilation: A Mathematical Introduction, Chapter 3, §3.1 (standard reference, not scraped)