LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge 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.

Centered filtering Feynman–Kac operators contract terminal tests

Statement

Let $X$ be a nonempty standard-Borel space with a sigma-finite reference measure $λ$ , and let $η_{0}$ be a probability on it. For $s \geq 1$ , supply jointly measurable, strictly positive finite densities $g_{s} (z ∣ x)$ of probability transition kernels relative to $λ$ , and measurable likelihood factors $f_{s}$ with $0 < a \leq f_{s} (z) \leq b < \infty$ . These specified versions satisfy, for one $C \geq 1$ and every $s, x, x^{'}, z$ , $g_{s} (z ∣ x) \leq C g_{s} (z ∣ x^{'}) .$ Define $c_{s} = η_{s - 1} (g_{s} f_{s})$ , $η_{s} (h) = η_{s - 1} (g_{s} (f_{s} h)) / c_{s}$ , and $E_{s} h (x) = g_{s} (f_{s} h) (x) / c_{s}$ . They are the operators of Finite-horizon SMC CLT classes and variance recursions restricted to last-state tests in the corresponding filtering model. Put $ρ = 1 - C^{- 2}$ . For every bounded measurable real terminal test $ψ$ and $0 \leq k < t$ , $∥ E_{k + 1 : t} (ψ - η_{t} ψ) ∥_{\infty} \leq C ρ^{t - k} osc (ψ) .$ For $k = t$ the identity image is bounded by $osc (ψ)$ ; use $ρ^{n} = 0$ for $n \geq 1$ when $C = 1$ . This is a closed last-state-test assertion, not a contraction of arbitrary functions of the full stored path. Positivity, finiteness and the ratio bounds refer to the supplied pointwise density versions, not to unspecified unrelated null-set versions.

Facts & Assumptions

Given: The specified positive finite density versions, probability transitions, initial probability, uniform row ratio and likelihood bounds, and bounded terminal test in the Statement.

[F1]

Measurability of integration against a kernel: a nonnegative measurable function integrated against a probability kernel has a measurable section integral.

[F2]

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: nonnegative measurable product integrals equal their iterated integrals.

[F3]

Uniform density ratios bound the Dobrushin coefficient: normalized probability-kernel density rows with ratio at most $R$ have Dobrushin coefficient at most $1 - R^{- 1}$ .

[F4]

Dobrushin contraction coefficient for a probability kernel: the coefficient is the supremum event-supremum total-variation distance between two output laws.

[F5]

Layer-cake formulas for random variables: for a nonnegative bounded random variable $U \leq 1$ , $E U = \int_{0}^{1} P (U > r) d r$ .

Proof

1.1F1givenconstructalgebra

Fix $k < t$ . Define $Q_{j, t} h (x)$ by iterating the kernels $g_{j + 1}, \dots, g_{t}$ , multiplying by $f_{j + 1}, \dots, f_{t}$ , and evaluating $h$ at the final state. Put $H_{j, t} = Q_{j, t} 1$ and $H_{t, t} = 1$ . Measurability follows from [F1], while probability normalization and the bounds on $f_{s}$ give $a^{t - j} \leq H_{j, t} \leq b^{t - j}$ . Comparing the first transition row gives $H_{j, t} (x) \leq C H_{j, t} (x^{'})$ for $j < t$ . Consequently $r_{k, t} : = H_{k, t} / η_{k} (H_{k, t})$ is positive, at most $C$ , and has $η_{k}$ -mean one.

2.1F1F2F3step 1.1constructalgebra

For $j = k + 1, \dots, t$ , set $L_{j, t} (x, d z) = g_{j} (z ∣ x) f_{j} (z) H_{j, t} (z) λ (d z) / H_{j - 1, t} (x)$ . The recursion for $H$ shows that these are probability kernels, with strictly positive finite denominators. The ratio of two of their density rows is $[g_{j} (z ∣ x) / g_{j} (z ∣ x^{'})] [H_{j - 1, t} (x^{'}) / H_{j - 1, t} (x)] \leq C^{2}$ by step 1.1. Thus [F3] gives $δ (L_{j, t}) \leq 1 - C^{- 2} = ρ$ . Telescoping the $H$ factors in the product kernel $P_{k, t} = L_{k + 1, t} \dots L_{t, t}$ gives $P_{k, t} h = Q_{k, t} h / H_{k, t}$ .

3.1F4F5step 2.1constructalgebra

For any probability kernel $K$ and bounded real $h$ of positive oscillation, put $u = (h - \inf h) / osc (h)$ . Then $0 \leq u \leq 1$ , and [F5] under each output law gives $K u (x) - K u (x^{'}) = \int_{0}^{1} [K (x, {u > r}) - K (x^{'}, {u > r})] d r$ . By [F4], its absolute value is at most $δ (K)$ . If the oscillation is zero, $K$ preserves the constant and the same oscillation bound is immediate. Hence $osc (K h) \leq δ (K) osc (h)$ . Iterating this inequality along the kernels in step 2.1 gives $osc (P_{k, t} h) \leq ρ^{t - k} osc (h)$ .

4.1F2step 1.1step 2.1step 3.1givenalgebra∎

The filtering recursion and iterated integration [F2] yield $η_{t} h = η_{k} (Q_{k, t} h) / η_{k} (H_{k, t})$ and $\prod_{j = k + 1}^{t} c_{j} = η_{k} (H_{k, t})$ . Thus $E_{k + 1 : t} h = r_{k, t} P_{k, t} h$ . Take $h = ψ - η_{t} ψ$ . Then $η_{k} (r_{k, t} P_{k, t} h) = 0$ , and $r_{k, t} η_{k}$ is a probability by step 1.1. Therefore the global infimum of $P_{k, t} h$ is at most zero and its supremum is at least zero, so its sup norm is at most its oscillation. Step 3.1 bounds this by $ρ^{t - k} osc (ψ)$ ; multiplying by $r_{k, t} \leq C$ proves the claim. For $k = t$ , the mean $η_{t} ψ$ lies between $\inf ψ$ and $\sup ψ$ , giving the identity-case bound.

Source notes

The local proof supplies the normalized future-kernel argument explicitly. The density-ratio hypothesis alone does not compare a target transition to its proposal; the separate variance theorem imposes that additional domination and an initial weight bound. No finite-particle or arbitrary-path time-uniform claim is imported from the source.

Depends on

Used by

Dependency tree · two levels

27 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

Nicolas Chopin, Central Limit Theorem for Sequential Monte Carlo Methods and its Application to Bayesian Inference, Appendix A.4 (standard reference, not scraped)