LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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 Kalman filter is exact conditional on a nonlinear path

Statement

Assume the model of Conditionally linear-Gaussian state-space model and fix a nonlinear path $z_{0 : T}$ . Run Exact linear-Gaussian Kalman filter on the resulting deterministic linear-Gaussian model for a fixed observation path $y_{1 : T}$ . Write $m_{t ∣ t - 1}, P_{t ∣ t - 1}$ and $m_{t ∣ t}, P_{t ∣ t}$ for its predicted and updated moments, and define $v_{t} = y_{t} - C_{t} (z_{0 : t}) m_{t ∣ t - 1}, S_{t} = C_{t} (z_{0 : t}) P_{t ∣ t - 1} C_{t} (z_{0 : t})^{T} + R_{t} (z_{0 : t}) .$ Then $L (U_{t} ∣ Z_{0 : T} = z_{0 : T}, Y_{1 : t} = y_{1 : t})$ has the Gaussian version $N (m_{t ∣ t}, P_{t ∣ t})$ for every $0 \leq t \leq T$ . At time $t \geq 1$ , the conditional observation density given the nonlinear path and earlier observations is $ℓ_{t} (z_{0 : t}; y_{1 : t}) = (2 π)^{- p_{t} / 2} \det (S_{t})^{- 1 / 2} \exp ⁣ (- \frac{1}{2} v_{t}^{T} S_{t}^{- 1} v_{t}) .$ Each $S_{t}$ is positive definite, each $P_{t ∣ t}$ is positive semidefinite, and $ℓ_{t}$ is finite, strictly positive, and Borel in the nonlinear path. For every $1 \leq t \leq T$ whose observation evidence is finite positive, the conditional density of $Y_{1 : t}$ given the nonlinear path is $\prod_{s = 1}^{t} ℓ_{s} (z_{0 : s}; y_{1 : s})$ . Consequently the conditional law of $Z_{0 : t}$ given $Y_{1 : t} = y_{1 : t}$ is the normalized Feynman–Kac path measure with path-extension transitions induced by $M_{s}$ , initial potential $G_{0} \equiv 1$ , and potentials $G_{s} (z_{0 : s}) = ℓ_{s} (z_{0 : s}; y_{1 : s})$ . At $t = 0$ it is the initial nonlinear law $μ_{0}$ .

Facts & Assumptions

Given: AC, the fixed path and observations, and the conditional model in the Statement.

[A1]

AC is inherited from the Gaussian-law and Kalman conditional-law conventions. The Axiom of Choice

[F1]

Conditional on a fixed nonlinear path, the initial state and all state and observation noises are mutually independent Gaussian vectors with the displayed positive-semidefinite covariances; the coefficient matrices are deterministic for that path. Conditionally linear-Gaussian state-space model

[F2]

The finite-horizon linear-Gaussian model with independent noises has an exact Kalman filtering version whenever every innovation covariance is positive definite; state and noise covariances may be singular. The finite-horizon linear-Gaussian Kalman filter is exact

[F3]

One prediction and observation step from a Gaussian state with positive-semidefinite covariance produces a jointly Gaussian state-observation pair with innovation covariance $S$ , and when $S$ is positive definite the conditional state law has the stated Kalman update. One-step Gaussian prediction and conditioning

[F4]

A positive-definite covariance matrix gives the multivariate normal law its Lebesgue density $(2 π)^{- p / 2} \det (S)^{- 1 / 2} \exp (- v^{T} S^{- 1} v / 2)$ . A positive-definite multivariate normal law has its Gaussian density

[F5]

A joint probability with a product-measurable density has the normalized conditional-density kernel on finite-positive evidence fibers. Conditional density formula

[F6]

A normalized Feynman–Kac path measure is the Markov path law weighted by the product of its nonnegative potentials, and it is normalized only at finite positive normalizer. Feynman–Kac path targets and normalizers

[F7]

Extending a nonlinear prefix by its transition kernel gives a probability kernel on the standard-Borel path spaces, and the ordered extensions give the nonlinear path law. Nonlinear path extension is a probability kernel

Proof

Given: The hypotheses in the Statement.

1.1A1F1givenalgebra

Initially $P_{0 ∣ 0} = P_{0} (z_{0})$ is positive semidefinite. If $P_{t - 1 ∣ t - 1}$ is positive semidefinite, then $P_{t ∣ t - 1} = A_{t} P_{t - 1 ∣ t - 1} A_{t}^{T} + Q_{t}$ is positive semidefinite because $u^{T} P_{t ∣ t - 1} u = (A_{t}^{T} u)^{T} P_{t - 1 ∣ t - 1} (A_{t}^{T} u) + u^{T} Q_{t} u \geq 0$ . For every nonzero observation vector $a$ , $a^{T} S_{t} a = (C_{t}^{T} a)^{T} P_{t ∣ t - 1} (C_{t}^{T} a) + a^{T} R_{t} a > 0$ , since the first term is nonnegative and $R_{t}$ is positive definite. Induction proves all innovation matrices meet the Kalman algorithm's domain.

2.1F1F2F3F4givenstep 1.1

By [F1], for this fixed path the conditional model is the deterministic finite-horizon model of [F2]. Step 1.1 verifies its positive-innovation hypothesis, so [F2] gives the exact conditional Gaussian filter at every observation history, including singular state covariances. At each time, [F3] gives the marginal observation law $N (C_{t} m_{t ∣ t - 1}, S_{t})$ ; applying [F4] yields the displayed density.

3.1F1step 1.1step 2.1algebra

The coefficient functions are Borel by [F1]. Finite sums and products preserve Borel measurability, and matrix inversion and determinant are continuous on the positive-definite matrices established in step 1.1. The Kalman moment recursion and the displayed density are therefore Borel functions of the path. The covariance determinant is finite and positive and the exponential is finite and strictly positive, so $ℓ_{t}$ has the claimed range.

4.1F1F5F6F7step 2.1step 3.1given∎

For a fixed nonlinear path, step 2.1 gives the one-step conditional density $ℓ_{s}$ of $Y_{s}$ given $Y_{1 : s - 1}$ . By the defining event-integral identity for conditional densities, $p (y_{1 : s} ∣ z) = p (y_{1 : s - 1} ∣ z) ℓ_{s} (z_{0 : s}; y_{1 : s})$ on finite-positive fibers; induction from the empty history, whose density is one, gives the product $\prod_{s = 1}^{t} ℓ_{s}$ . By [F7], the ordered path-extension kernels are probability kernels on the standard-Borel path spaces and give the nonlinear path law. The joint law of $Z_{0 : t}$ and $Y_{1 : t}$ therefore has this product as its observation-density factor relative to that path law and Lebesgue observation measure. By [F5], conditioning on a history with finite positive evidence weights the nonlinear path law by this product and divides by its integral. Comparing with [F6] gives exactly the stated normalized Feynman–Kac path measure. This assertion is restricted to those finite-positive evidence fibers; null and infinite fibers are not normalized.

Depends on

Used by

Rao–Blackwellized particle filter Algorithm
A two-mode linear-Gaussian Rao–Blackwellized filter Example

Dependency tree · two levels

59 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 7, §7.5 (standard reference, not scraped)
Fredrik Lindsten, Pete Bunch, Simo Särkkä, Thomas B. Schön, and Simon J. Godsill, Rao-Blackwellized particle smoothers for conditionally linear Gaussian models, §3.2 (standard reference, not scraped)