Pipeline-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.

✓ 3 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

State-space models and exact Bayesian filtering — Examples

1 · Prerequisites

2 · Summary

Overview

The finite hidden Markov example computes two filtering steps and a smoothed marginal by exact finite sums. The scalar Gaussian example derives the prediction and posterior directly by convolution and completing the square. The impossible-observation example shows why a zero-evidence history cannot be normalized and why a conditional law records only a filler on that observation-null fiber. These cases illustrate exact model calculations, not finite-particle algorithms or empirical guarantees.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

A two-state hidden Markov filter and smoother

Example

Let $E_{0} = E_{1} = E_{2} = F_{1} = F_{2} = {0, 1}$ with counting measure. Take $μ_{0} = (1 / 2, 1 / 2)$ and transition matrix $M = (\begin{array}{cc} 3 / 4 & 1 / 4 \\ 1 / 4 & 3 / 4 \end{array}),$ where rows index the current state. At each time let $G_{t} (1 ∣ 0) = 1 / 4$ and $G_{t} (1 ∣ 1) = 3 / 4$ , with the complementary probabilities for observation $0$ . For observations $Y_{1} = 1, Y_{2} = 0$ , the exact filter at time $2$ is $(9 / 14, 5 / 14)$ on states $(0, 1)$ , while the smoothing law of $X_{1}$ given both observations is $(5 / 14, 9 / 14)$ . This finite model has positive evidence at both observed times.

Verification

Given: AC, the finite-horizon kernel model, and observations in the Example.

[A1] AC states that every family of nonempty sets has a choice function. The Axiom of Choice

[F1] Filtering and smoothing kernels are conditional laws given the stated observation histories. Filtering, predictive, and smoothing laws in a finite-horizon state-space model

[F2] For dominated observation kernels, the prediction and update are given by the exact recursion, with evidence computed by summing the likelihood against the predictive state law. Exact state-space filtering recursion under dominated observations

[F3] The finite-horizon model law is the ordered product of the initial, transition, and observation kernels. Finite-horizon state-space kernel law exists and is unique

[F4] Under AC the data-indexed conditional filtering and smoothing kernels exist for this finite standard-Borel model. Filtering and finite-horizon smoothing laws exist

[F5] The model supplies transition and observation probability kernels. General finite-horizon state-space models by kernels

[F6] The recursive filtering procedure uses the prediction/update formulas and predictive filler on zero or infinite evidence. Recursive Bayesian filtering under dominated observations

1.1A1givenF2F3F5F6algebra

Let $g_{t} (i, j) : = G_{t} (i, {j})$ for $i, j \in {0, 1}$ . Counting measure integrates by finite sums, so $\sum_{j} g_{t} (i, j) = G_{t} (i, {0, 1}) = 1$ and $G_{t} (i, C) = \sum_{j \in C} g_{t} (i, j)$ ; every function on these finite discrete spaces is product-measurable. Thus [F2] applies. Since $μ_{0}$ is uniform and each transition-matrix column sums to one, $X_{1}$ is uniform; hence $P (Y_{1} = 1) = \frac{1}{2} (\frac{1}{4} + \frac{3}{4}) = \frac{1}{2}$ , and Bayes' finite sum gives $P (X_{1} = 0 ∣ Y_{1} = 1) = \frac{(1 / 2) (1 / 4)}{1 / 2} = 1 / 4$ and $P (X_{1} = 1 ∣ Y_{1} = 1) = 3 / 4$ .

2.1A1givenF2F6step 1.1algebra

Predicting through $M$ gives $P (X_{2} = 0 ∣ Y_{1} = 1) = \frac{1}{4} \frac{3}{4} + \frac{3}{4} \frac{1}{4} = \frac{3}{8}$ and $P (X_{2} = 1 ∣ Y_{1} = 1) = \frac{1}{4} \frac{1}{4} + \frac{3}{4} \frac{3}{4} = \frac{5}{8}$ .

3.1A1givenF2F6step 2.1algebra

The evidence for $Y_{2} = 0$ is $(3 / 8) (3 / 4) + (5 / 8) (1 / 4) = 7 / 16$ ; thus $P (X_{2} = 0 ∣ Y_{1} = 1, Y_{2} = 0) = 9 / 14$ and $P (X_{2} = 1 ∣ Y_{1} = 1, Y_{2} = 0) = 5 / 14$ , which sum to one.

4.1A1givenF1F3F4step 1.1step 3.1algebra∎

By the ordered path law [F3], for $i = 0, 1$ the conditional probability of $Y_{2} = 0$ given $X_{1} = i, Y_{1} = 1$ is $\sum_{j = 0}^{1} M_{i j} G_{2} (j, {0})$ ; the factor $G_{1} (i, {1})$ cancels in this conditional probability because it depends only on the fixed state $i$ and event $Y_{1} = 1$ . These sums are $(3 / 4) (3 / 4) + (1 / 4) (1 / 4) = 5 / 8$ for $i = 0$ and $(1 / 4) (3 / 4) + (3 / 4) (1 / 4) = 3 / 8$ for $i = 1$ . Multiplying by the time-1 filter $(1 / 4, 3 / 4)$ gives conditional smoothing masses $(5 / 32, 9 / 32)$ ; their sum is $7 / 16$ , the conditional evidence in step 3.1, so the smoothing law of $X_{1}$ is $(5 / 14, 9 / 14)$ . The history event has positive probability by step 1.1 and step 3.1, so its conditional distribution is fixed by the event identities.

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passOpen item page →

A scalar Gaussian state-space update by completing the square

Example

Take scalar state spaces and horizon $T = 1$ . Let $X_{0} \sim N (0, 1)$ , $K_{1} (x, d x_{1}) = N (x, 1) (d x_{1})$ , and $G_{1} (x_{1}, d y) = N (x_{1}, 1) (d y)$ , with the standard Lebesgue densities. Observe $Y_{1} = 2$ . The predictive state law is $N (0, 2)$ , the evidence density at $2$ is $z_{1} (2) = e^{- 2 / 3} / \sqrt{6 π} > 0$ , and the filtering version selected by the specified dominated density formula has value $N (4 / 3, 2 / 3)$ . Since the singleton ${2}$ has observation probability zero, another conditional-law version may take a different value there.

Verification

Given: AC, the one-step scalar model, and the observed value in the Example.

[A1] AC states that every family of nonempty sets has a choice function. The Axiom of Choice

[F1] The standard normal density is $f (u) = e^{- u^{2} / 2} / \sqrt{2 π}$ , and $N (m, σ^{2})$ is its affine image $m + σ Z$ ; hence translated normal kernels have densities $f (y - m)$ . Standard normal and normal laws

[F2] $\int_{- \infty}^{\infty} e^{- u^{2}} d u = \sqrt{π}$ . The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$

[F3] Translation of a set $B$ by $a$ is $B + a$ , and Lebesgue measure is translation invariant on measurable sets. Translation of a subset of $R^{n}$ , Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation

[F4] AC implies Countable Choice. AC supplies countable selections and prescribed serial paths, The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F5] Under Countable Choice, dilation by nonzero $c$ changes Lebesgue measure by the factor $∣ c ∣$ . For a nonzero real $c$ , dilation by $c$ multiplies Lebesgue outer measure by $∣ c ∣^{n}$ , and reflection in the origin preserves it

[F6] Nonnegative measurable functions admit increasing simple approximations, and monotone limits pass through their integrals. Every nonnegative measurable function is the increasing limit of simple measurable functions, Monotone convergence for the integral

[F7] For dominated observations, the exact filtering update uses the density formula only at finite positive evidence. Exact state-space filtering recursion under dominated observations

[F8] The finite-horizon state-space law is the iterated product of its transition and observation kernels, with existence supplied by the kernel-law theorem. General finite-horizon state-space models by kernels, Finite-horizon state-space kernel law exists and is unique

[F9] The recursive procedure defines the prediction and density-update version, using the predictive measure as its bad-evidence filler. Recursive Bayesian filtering under dominated observations

[F10] Under Countable Choice, every continuous map between Euclidean spaces is Borel measurable. Continuous functions on Euclidean spaces are Borel measurable

[F11] Under Countable Choice, Borel sets are Lebesgue measurable, so Borel functions are Lebesgue measurable. Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable

[F12] $B (R) \otimes B (R) = B (R^{2})$ . The Borel product of R^m and R^n is the Borel sigma-algebra of R^{m+n}

[F13] Under Countable Choice, Lebesgue measure is a measure extending half-open interval length and is sigma-finite with the exhaustion $(- k, k]$ , $k \geq 1$ . Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume, Lebesgue measure is sigma-finite, and every metrically bounded subset of $R^{n}$ has finite outer measure

[F14] A probability kernel has probability-measure sections and measurable evaluations. Integration of a nonnegative product-measurable function against a uniformly sigma-finite kernel with a specified common exhaustion is measurable. Measure kernel and probability kernel, Measurability of integration against a kernel

[F15] Measures are monotone, and the integral of a nonnegative measurable function over a measurable null set is zero. Measures are monotone, A nonnegative integral over a null set vanishes

[F16] For a nonnegative product-measurable function on two sigma-finite measure spaces, Tonelli's theorem gives measurable section integrals and permits either order of integration. Tonelli's theorem for nonnegative measurable functions on a sigma-finite product

1.1A1F4F10F11F12F13F14givenconstruct

Equip all scalar state and observation spaces with $B (R)$ , and let $ν_{1}$ be Lebesgue measure restricted to this sigma-algebra. By [A1] and [F4], Countable Choice is available. By [F13], $(- k, k]$ is a common finite-mass exhaustion, so both $ν_{1}$ and the constant measure kernel $L (x, B) = ν_{1} (B)$ are sigma-finite in the required sense. The constant evaluations are measurable. By [F10] and [F12], $(x, y) \mapsto f (y - x)$ is measurable for the product Borel sigma-algebra. By [F11], its one-variable Borel sections and the simple approximations used below are also Lebesgue measurable.

2.1F1F3F6F7F8F11F14step 1.1construct

For a Borel set $B$ , $P (x + Z \in B) = \int_{B - x} f (u) d u = \int_{B} f (y - x) d y$ : [F3] gives the translated integral identity for indicators, finite sums give it for simple functions, and [F6] and [F11] extend it to nonnegative Borel functions. Thus the transition and observation sections are the probability laws $N (x, 1)$ and have densities $f (x_{1} - x)$ and $f (y - x_{1})$ , whose integrals are one. For fixed Borel $B$ , apply [F14] to the product-measurable integrand $1_{B} (y) f (y - x)$ and the constant kernel $L$ from step 1.1. Its integral is Borel measurable in $x$ . Hence these location families are probability kernels, and their product-measurable normalized densities with sigma-finite $ν_{1}$ meet the premises of [F7] and [F8].

3.1F1F2F3F5F6F8F11F16step 1.1step 2.1algebra

For every Borel set $B$ , the path law [F8], step 2.1 and simple approximation [F6] give $P (X_{1} \in B) = \int_{R} \int_{B} f (u) f (x - u) ν_{1} (d x) ν_{1} (d u)$ . The integrand $1_{B} (x) f (u) f (x - u)$ is nonnegative and product-measurable, and both copies of $ν_{1}$ are sigma-finite by step 1.1. Thus [F16] gives $P (X_{1} \in B) = \int_{B} [\int_{R} f (u) f (x - u) ν_{1} (d u)] ν_{1} (d x)$ . The predictive density is therefore $\int f (u) f (x - u) d u = \frac{e^{- x^{2} / 4}}{2 π} \int e^{- (u - x / 2)^{2}} d u = \frac{1}{\sqrt{4 π}} e^{- x^{2} / 4}$ by [F2] and translation. This is the density of $N (0, 2)$ by [F1], dilation [F5], and the simple-approximation argument [F6].

4.1A1F2F4F5F6F11step 3.1algebra

At $y = 2$ , the product density from step 3.1 has exponent $- x^{2} / 4 - (2 - x)^{2} / 2 = - \frac{3}{4} (x - \frac{4}{3})^{2} - \frac{2}{3}$ . By [F5] and [F6], $\int e^{- \frac{3}{4} (x - 4 / 3)^{2}} d x = 2 \sqrt{π / 3}$ , so $z_{1} (2) = \frac{e^{- 2 / 3}}{\sqrt{8 π^{2}}} 2 \sqrt{π / 3} = \frac{e^{- 2 / 3}}{\sqrt{6 π}} \in (0, \infty)$ .

5.1A1F1F3F5F7F9F11F13F15step 4.1algebra∎

Dividing the product density by the evidence in step 4.1 leaves $\frac{1}{\sqrt{4 π / 3}} e^{- \frac{3}{4} (x - 4 / 3)^{2}}$ , the normal density with mean $4 / 3$ and variance $2 / 3$ by [F1,F5]; since $0 < z_{1} (2) < \infty$ , [F7] and [F9] identify it as the filtering-kernel value returned by the recursive procedure. The closed singleton ${0}$ is measurable by [F11]; [F13] and [F15] give $0 \leq a : = λ ({0}) \leq λ ([0, 1)) = 1$ . Dilation by $2$ in [F5] gives $a = 2 a$ , so $a = 0$ ; translation [F3] gives $ν_{1} ({2}) = 0$ . The observation marginal has density $z_{1}$ by [F7], so [F15] yields $P (Y_{1} = 2) = \int_{{2}} z_{1} (y) ν_{1} (d y) = 0$ . Thus this selected value is a valid version, not a pointwise uniqueness claim. There is no numerical approximation or asymptotic argument.

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

An impossible observation has zero evidence and only a filler filter value

Example

Let $E_{0} = E_{1} = {0, 1}$ and $F_{1} = {a, b}$ with counting measure. Set $μ_{0} = δ_{0}$ and let the transition kernel preserve the state, $K_{1} (x, \cdot) = δ_{x}$ . Let $G_{1} (0, {a}) = 1$ and $G_{1} (1, {b}) = 1$ . Then the predictive law is $δ_{0}$ , and the evidence for observing $b$ is zero. The update at $b$ is therefore the supplied predictive filler $δ_{0}$ ; it is not a quotient posterior. Because $P (Y_{1} = b) = 0$ , any probability assigned at $b$ would satisfy the same RCD identities.

Verification

Given: AC and the finite model and kernels in the Example.

[A1] AC states that every family of nonempty sets has a choice function. The Axiom of Choice

[F1] Filtering laws are conditional kernels defined by event identities; their values on observation-null fibers may be replaced by a fixed probability. Filtering, predictive, and smoothing laws in a finite-horizon state-space model

[F2] For dominated observations, zero and infinite evidence fibers receive the predictive probability as a conditional-kernel filler. Exact state-space filtering recursion under dominated observations

[F3] The state-space path law is the ordered product of the supplied probability kernels. Finite-horizon state-space kernel law exists and is unique

[F4] The recursive filtering procedure uses the predictive measure on zero or infinite evidence fibers. Recursive Bayesian filtering under dominated observations

1.1A1F2F3F4given

With counting measure on $F_{1}$ , set $g_{1} (x, y) = G_{1} (x, {y})$ ; it is jointly measurable on the finite discrete spaces, sums to one over $y$ , and gives $G_{1} (x, C) = \sum_{y \in C} g_{1} (x, y)$ . The predictive state law is $δ_{0}$ , so the evidence is $z_{1} (a) = 1$ and $z_{1} (b) = 0$ ; the update at $a$ is $δ_{0}$ and [F2] and [F4] make the update at $b$ the predictive filler $δ_{0}$ . The factorized law [F3] gives $P (Y_{1} = b) = 0$ .

2.1A1F1step 1.1algebra∎

Let $ρ$ be any probability measure on $E_{1}$ and define $q (a, \cdot) = δ_{0}$ and $q (b, \cdot) = ρ$ . This is a measurable probability kernel because the observation space is finite discrete. For every $A \subseteq {0, 1}$ and $C \subseteq {a, b}$ , the path law gives $P (X_{1} \in A, Y_{1} \in C) = 1_{A} (0) 1_{C} (a)$ , while $E [1_{{Y_{1} \in C}} q (Y_{1}, A)] = 1_{C} (a) δ_{0} (A) + 0 \cdot 1_{C} (b) ρ (A) = 1_{A} (0) 1_{C} (a)$ . These are all conditioning events in the finite observation space, so every probability $ρ$ at $b$ gives the same conditional identities.

State-space models and exact Bayesian filtering — Examples

1 · Prerequisites

2 · Summary

Overview

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

A two-state hidden Markov filter and smoother

Example

Verification

A scalar Gaussian state-space update by completing the square

Example

Verification

An impossible observation has zero evidence and only a filler filter value

Example

Verification

Sources