TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Time-uniform SMC asymptotic variance under uniform weight and operator bounds

Statement

Use multinomial offspring resampling and the covariance $V_{t}$ of Finite-horizon SMC CLT classes and variance recursions. Suppose all normalized incremental weights satisfy $υ_{s} \leq B < \infty$ almost everywhere under their proposals, including $s = 0$ . For a chosen bounded real terminal test $ϕ$ and every $0 \leq k \leq t$ , assume the bounded versions of its centered backward images satisfy $∥ E_{k + 1 : t} (ϕ - π_{t} ϕ) ∥_{\infty} \leq A ρ^{t - k} Δ ϕ,$ with fixed $A \geq 1$ and $0 \leq ρ < 1$ , uniformly over the horizons considered; use $ρ^{0} = 1$ . Then $V_{t} (ϕ) \leq \frac{A^{2} B^{2} (Δ ϕ)^{2}}{1 - ρ^{2}} .$ The one-step centered oscillation condition of Uniform SMC backward-operator contraction controls oscillation gives the original specialization $A = 1$ , $ρ = β$ and bound $B^{2} (Δ ϕ)^{2} / (1 - β^{2})$ .

There is a separate filtering-density sufficient branch. Use the strictly positive finite density versions, true-transition row-ratio bound $C \geq 1$ , likelihood bounds $0 < a \leq f_{s} \leq b < \infty$ and normalized filtering operators in Centered filtering Feynman–Kac operators contract terminal tests. Additionally require strictly positive finite proposal densities $q_{s} (z ∣ x)$ with $g_{s} (z ∣ x) \leq D q_{s} (z ∣ x)$ uniformly for a finite $D$ , and an initial normalized weight $υ_{0} \leq B_{i n i t} < \infty$ under its proposal. Put $B = \max (B_{i n i t}, D b / a)$ and $ρ = 1 - C^{- 2}$ . For bounded last-state tests $ϕ (x_{0 : t}) = ψ (x_{t})$ , the bound holds with $A = C$ : $V_{t} (ψ) \leq \frac{B^{2} C^{2} (osc ψ)^{2}}{1 - (1 - C^{- 2})^{2}} .$ This branch concerns the closed last-state test subspace and its backward images, not all path observables. Both bounds concern fixed-horizon CLT variances, uniform in the time index; neither is a finite-particle time-uniform error bound.

Facts & Assumptions

Given: The multinomial SMC flow, the uniform incremental-weight bound $B$ , and the stated multistep centered-image constants $A, ρ$ ; for the filtering branch, the explicit density, domination and initial-weight hypotheses.

[A1]

The Axiom of Choice: AC is inherited through the finite-horizon SMC path-law and Radon–Nikodym construction.

[F1]

Finite-horizon SMC CLT classes and variance recursions: $V_{t}$ is the weighted-estimator covariance, $υ_{s}$ is the normalized incremental Radon–Nikodym weight, and $Φ_{s}, Ψ_{s}$ are the recursive moment classes.

[F2]

Multinomial SMC variance unrolls into local contributions: $V_{t} (ϕ)$ is the sum over $k = 0, \dots, t$ of ${\tilde{π}}_{k} [υ_{k}^{2} (E_{k + 1 : t} (ϕ - π_{t} ϕ))^{2}]$ .

[F3]

Uniform SMC backward-operator contraction controls oscillation: the stated one-step centered contraction gives the multistep image bound with $A = 1$ and $ρ = β$ .

[F4]

Centered filtering Feynman–Kac operators contract terminal tests: for the stated filtering density model and bounded last-state tests, the multistep image bound holds with $A = C$ and $ρ = 1 - C^{- 2}$ .

Proof

Given: The hypotheses in the Statement.

1.1A1F1F2given

Put $h_{t} = ϕ - π_{t} (ϕ)$ and $h_{k} = E_{k + 1 : t} h_{t}$ for $0 \leq k < t$ , with $h_{t}$ itself at $k = t$ . The multistep hypothesis supplies bounded versions of these centered images. By [F1], $π_{k} (h_{k}) = 0$ and $E_{k} h_{k} = h_{k - 1}$ for $1 \leq k \leq t$ . At $k = 0$ , boundedness and $υ_{0} \leq B$ almost everywhere give $h_{0} \in Ψ_{0}$ . If $h_{k - 1} \in Ψ_{k - 1}$ , then boundedness of $h_{k}$ and $υ_{k} \leq B$ almost everywhere give ${\tilde{π}}_{k} (∣ υ_{k} h_{k} ∣^{2 + δ}) < \infty$ and $E_{k} h_{k} = h_{k - 1} \in Φ_{k - 1}$ , so $h_{k} \in Φ_{k}$ . Also $π_{k} (h_{k}^{2}) < \infty$ and $E_{k} h_{k} = h_{k - 1} \in Ψ_{k - 1}$ , hence $h_{k} \in Ψ_{k}$ . Induction gives $h_{t} \in Ψ_{t}$ , so [F2] applies to $V_{t} (h_{t}) = V_{t} (ϕ)$ . Its summands are nonnegative and finite because $υ_{k} \leq B$ almost everywhere and each $h_{k}$ has a bounded version.

2.1F2F3step 1.1givenalgebra

The multistep bound in the Statement makes the $k$ th summand at most $B^{2} A^{2} ρ^{2 (t - k)} (Δ ϕ)^{2}$ . Summing the geometric series gives $V_{t} (ϕ) \leq A^{2} B^{2} (Δ ϕ)^{2} / (1 - ρ^{2})$ . Applying [F3] yields the original one-step specialization.

3.1F1F4step 2.1givenalgebra∎

In the filtering branch, the actual increment is $υ_{s} (x, z) = g_{s} (z ∣ x) f_{s} (z) / (c_{s} q_{s} (z ∣ x))$ , with $c_{s} = η_{s - 1} (g_{s} f_{s}) \in [a, b]$ . Hence $υ_{s} \leq D b / a$ for $s \geq 1$ ; the initial bound gives $υ_{s} \leq B$ at every time. The last-state subspace is preserved by the filtering operators, and [F4] supplies its centered-image estimate with $A = C$ , $ρ = 1 - C^{- 2}$ . Step 2.1 proves the displayed filtering bound; when $C = 1$ , all earlier images vanish and the same formula applies.

Remarks

Uniform predecessor ratios for $g_{s}$ and $q_{s}$ alone do not bound $g_{s} / q_{s}$ or the incremental weights when proposals vary with time. The B-page finite-state counterexample refutes that displayed source/design implication. The additional domination and initial-weight assumptions above are explicit corrections, not consequences ascribed to those predecessor ratios. The abstract branch remains available under its own actual operator assumptions.

Depends on

Used by

Dependency tree · two levels

15 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, §3.3 and Appendix A.4 (standard reference, not scraped)
Hans R. Künsch, Recursive Monte Carlo Filters: Algorithms and Theoretical Analysis, §4.3.1 (standard reference, not scraped)
Arnaud Doucet and Adam M. Johansen, A Tutorial on Particle Filtering and Smoothing: Fifteen Years Later, §3.6 (standard reference, not scraped)