Metropolized backward sampling for conditional sequential Monte Carlo: Lean formalization

7 Formalization notes

The formalization differs from the paper in the following conventions and assumptions, which do not change the results of the paper.

7.1 Indices and types

  • Times are indexed from \(0\). With \(T = n + 1\), the time \(t \in [T]\) of the paper is the element \(t - 1\) of \(\mathrm{Fin}(n + 1)\). The backward step from time \(t + 1\) to time \(t\) is indexed by \(s \colon \mathrm{Fin}(n)\), between the times s.castSucc and s.succ. The indices of the particles are the elements of \(\mathrm{Fin}(N)\), in which the index \(i \in [N]\) of the paper is \(i - 1\).

  • The particle positions are a function on \(\mathrm{Fin}(n + 1) \times \mathrm{Fin}(N)\). The ancestor index \(a_t^i\) is a s i, where \(t\) is the time s.castSucc. At the step \(s\), the matrix of the backward-sampling probabilities has the entry \(B_t(i \mid j)\) in row \(i\) and column \(j\), so that its columns are probability vectors.

  • Probability vectors are defined by a predicate, IsProbVector, on functions to \(\mathbb {R}\), because the set stdSimplex of Mathlib is deprecated in the version of Mathlib used. Markov kernels on \([N]\) are the matrices of Matrix.rowStochastic.

7.2 The model

  • The densities and the potential functions take values in \([0, \infty )\). Their measurability, the normalization \(\int m_1 \mathrm{d}x = 1\) and \(\int m_{t+1}(x, x') \mathrm{d}x' = 1\) for every \(x\), the positivity of the potential functions, and \(Z\in (0, \infty )\) are fields of the structures FeynmanKac and PreviousState.Model. The measure \(\mathrm{d}x\) is a parameter of the model, assumed to be \(\sigma \)-finite in the statements.

  • Where the denominator of the backward-sampling probabilities (2) or (S3) vanishes, which happens on a null set, \(B_t(\cdot \mid j)\) is defined as \(\mathbf{W}_t\), so that it is a probability vector for all particle positions. Where the denominator is positive, \(B_t(i \mid j)\) is given by (2), by Lemma 20.

  • The statements of Section 3 of the paper and of the later sections assume \(N \geq 2\), as the paper does. The statements which do not involve the particle filter, that is, Lemmas 12 and 16 and the claims for two particles, hold for every \(N\) and are stated without this assumption.

7.3 The algorithms

  • The kernels of Algorithms 1 and S1 are assumed to be measurable functions of the particle positions and, for Algorithm S1, of the ancestor indices. This assumption is the hypothesis MeasurableKernels. The kernels of the six selection rules satisfy it (Lemma 25).

  • The resampling schemes \(r_t\) of Section S3 are assumed to be measurable functions of the particles and of the weights. The condition of Definition 79 is required for every probability vector of weights, including those with zero entries, which do not occur in the algorithms. Multinomial resampling satisfies it for all of them.

  • Steps (c) and (d) of Algorithm 1 are defined as the kernel whose mass function is the product of the probabilities of the successive draws.

  • The forward passes are defined by densities with respect to the product of the counting measure on the ancestor indices and of a measure on the particle positions. This measure is the Dirac measure at the state \(x_t\) of the reference at each coordinate \((t, b_t)\) and \(\mathrm{d}x\) at the other coordinates. The density of the forward pass of Algorithm 1 contains the factor \(\mathbf{1}\{ a_{t-1}^{b_t} = b_{t-1}\} \).

  • In Algorithm S1.b, the probabilities of \((b_{t+1}, a_t)\) are normalized by their sum over the set where \(a_t^{b_{t+1}} = c\), which is \(N W_t^c\) by Definition 79. The forward pass is defined for \(c\) drawn from a Markov kernel which is a function of \(B_t(\cdot \mid x_{t+1})\), started from \(b_t\). This kernel is the Gibbs kernel in Algorithm S1, the identity kernel in Algorithm S2, and the kernel \(K_{t,j,j}\) of the selection rule in Lemma 86.

  • Algorithm S2 is defined for each of the six selection rules. Proposition 94 is stated for the five rules other than CM-BS, for which Algorithm S2 is given in the paper.

  • The results of the paper on Algorithm 1 are proved as stated, with the indices of the reference drawn uniformly in Algorithm 1.a. The claim of Section 2 of the paper that the law of the output does not change if the indices of the reference are fixed is not formalized. This claim is used in the experiments of the paper but not in its proofs.

7.4 The statements

  • A statement on \(x_{1:T} \sim \pi \) and a run of an algorithm is a statement on the joint distribution of \(x_{1:T}\) and of the variables of the algorithm, that is, on \(\pi \) followed by the kernel of the distribution of these variables given the reference trajectory (Measure.compProd). A conditional distribution is stated as a disintegration: the joint distribution is the distribution of the conditioning variables followed by a kernel. In Lemma 49, the successive conditional distributions are those of the backward Markov chain of Definition 44, whose probabilities are their products. The distribution of the particle positions in this disintegration is their distribution under \(\bar{\pi }\). In Lemma 41, the claim that \(x_{1:T}\) is the trajectory traced back from \(b_T\) is stated as follows: the joint distribution of \(x_{1:T}\) and \((\mathbf{x}, a, b_T)\) is the image of \(\bar{\pi }\) under the map which adds the trajectory traced back from \(b_T\). In Lemma 86, the claim that \(x_{1:T} = (x_1^{b_1}, \dotsc , x_T^{b_T})\) is stated as follows: the joint distribution of \(x_{1:T}\) and \((\mathbf{x}, a, b_{1:T})\) is the image of the distribution with density (S4) under the map which adds \((x_1^{b_1}, \dotsc , x_T^{b_T})\). Unlike almost-sure equalities, these identities of distributions do not require the diagonal of \(\mathsf{X}^2\) to be measurable.

  • Probabilities are real numbers, given by Measure.real. Expectations are Bochner integrals. The square-integrability conditions of Theorem 61 and Corollary 63 are stated as the measurability of \(f\) and MemLp with exponent \(2\) under \(\pi \). Since MemLp includes the measurability of \(x_{1:T} \mapsto f(x_t)\), respectively \(x_{1:T} \mapsto f(x_t, x_{t+1})\), up to a null set, the measurability of \(f\) is not used in the proofs.

  • The statements on update rates assume that the diagonal of \(\mathsf{X}^2\) is measurable (MeasurableEq), so that the events \(\{ \tilde{x}_t \neq x_t\} \) are measurable. Theorem 61 and Corollary 63 are therefore stated as two Lean statements each, one on autocovariances and one on update rates. Proposition 91 is stated as six Lean statements, two for each of Theorem 61 and Corollary 63, and one for each of Propositions 67 and 70.

  • In Corollary 63, the assumption that the particles at time \(t\) and those at time \(t + 1\) are pairwise distinct is the assumption that the particles at time \(t\) are pairwise distinct and that the particles at time \(t + 1\) are pairwise distinct.

  • In Proposition 67, the condition \(m_{s+1}(x, \cdot ) \geq \varepsilon m_{s+1}(x', \cdot )\) is assumed at every point. In the indexing from \(0\), the exponent \(T - t\) is \(n - t\).

  • In Proposition 70, the inequality \(\gamma _t(j, j') \geq 0\) is proved for all particle positions and all \(j, j' \in [N]\).

  • In Proposition 73, the condition that \(m_{s+1}(x, x')\) does not depend on \(x\) is assumed for every \(x' \in \mathsf{X}\), not only for almost every \(x'\). The conditional independence of the output indices is stated as follows: the joint distribution of \((\mathbf{x}, b_{1:T}, l_{1:T})\) is that of \((\mathbf{x}, b_{1:T})\) followed by the kernel with mass function \(\prod _t F_{\mathbf{W}_t}(b_t, l_t)\).

  • In Proposition 91, the distribution (S4) in place of \(\bar{\pi }\) is that of Algorithm S1, with the Gibbs kernels.

  • In Proposition 92, the model of Section S3 has the densities of a model of the main text and the potential functions \(g_1\) and \(g_t(x_{t-1}, x_t) = g_t(x_t)\) of that model.

  • The results of Liu (1996), Tierney (1998, Lemma 3), and Dobrushin (1956) on which the proofs depend are proved, as is the computation of Andrieu et al. (2010) and Chopin and Singh (2015) on which Lemma 41 rests. That stratified, systematic, residual, and killing resampling are resampling schemes in the sense of Definition 79 (Finke et al., 2026, Section 3) is not formalized. The condition of Definition 79 is a hypothesis on the \(r_t\) in the statements, and is proved for multinomial resampling.