The results of the paper #
Each result of the paper Metropolized backward sampling for conditional sequential Monte Carlo and of its supplementary material is stated here, in the order of the paper, with the hypotheses of the paper and the formalization assumptions listed in the notes of the blueprint. The docstring of each statement contains a quotation of the paper and the label of the result.
Conventions:
- With
T = n + 1time steps,t : Fin (n + 1)is the timet.val + 1 ∈ [T]of the paper. The timet ∈ [T - 1]of a backward step of the paper iss : Fin n, the step between the timess.castSuccands.succ. x ∼ πfollowed by a run of an algorithm fromxis the measureM.target ⊗ₘ κon the pairs(x, z), whereκis the kernel of the conditional distribution of the variableszof the algorithm givenx. A conditional distribution given some variables is a kernelκ'such that the joint distribution is the distribution of these variables⊗ₘ κ'.- Probabilities and expectations conditional on the particle positions, as in Lemma 4, are stated
as identities of joint distributions. The statements on update rates and autocovariances concern
the joint distribution of the reference and the output, with
x ∼ π. - That a variable is a function of other variables, as in Lemmas 3 and S1, is stated as an
identity of joint distributions: the joint distribution of all the variables is the image of the
distribution of the other variables under the map which adds the value of the function.
Unlike an almost-sure equality, this does not need any measurability of the diagonal of
X × X. - The events
{x̃_t ≠ x_t}are measurable underMeasurableEq X, the measurability of the diagonal ofX × X.
Section 2: the forced move and the coupling kernel #
Lemma 1 (lem:forced, Section 2.2).
'The kernel F_p is reversible with respect to p. For i ≠ j, F_p(i, j) ≥ p_j. For every
φ : [N] → ℝ, ⟨φ, F_p φ⟩_p ≤ p(φ)².'
The forced move for two particles (Section 2.2).
'For N = 2 and p_1, p_2 > 0, F_p(1, 2) = min{1, p_2/p_1} is the Metropolis acceptance
probability'. The indices 1 and 2 are 0 and 1 in Lean.
Lemma 2 (lem:coupling, Section 2.3).
'Let p and q be probability vectors on [N]. For all i, i' ∈ [N],
p_i C_{p,q}(i, i') = q_{i'} C_{q,p}(i', i). For i ≠ i', C_{p,q}(i, i') ≥ q_{i'}. For every
φ : [N] → ℝ, ⟨φ, C_{p,q} φ⟩_p ≤ p(φ) q(φ).'
Section 3: validity #
The six selection rules satisfy the hypotheses of Algorithm 1 (Section 3).
'Proposition 1 applies to the six selection rules of Section 2, because the identity kernel, the
Gibbs kernel, and, by Lemma 1, F_p are reversible with respect to p, whereas, for j ≠ j', the
kernels K_{t,j,j'}(i, ·) = B_t(·|j') satisfy (3), and so do the kernels
K_{t,j,j'} = C_{B_t(·|j), B_t(·|j')} of CM-BS, by the first part of Lemma 2.'
Formalization: the kernels are also measurable functions of the particle positions, which is a
hypothesis of Lemma 4 and of Proposition 1.
Lemma 3 (lem:extended, Section 3).
'Let x_{1:T} ∼ π and run steps (a) and (b) of Algorithm 1. Then (x, a, b_T) ∼ π̄, with
x_{1:T} the trajectory traced back from b_T. Under π̄, conditionally on x, the indices
b_T and a_t^n, t ∈ [T - 1], n ∈ [N], are independent, with the distributions W_T and
B_t(·|n), respectively.'
The first conjunct states that the distribution of (x, a, b_T) is π̄.
The second states that the joint distribution of the reference trajectory and of (x, a, b_T) is
the image of π̄ under the map which adds the trajectory traced back from b_T, so that the
reference trajectory is the trajectory traced back from b_T.
The third states that π̄ is the distribution of the particle positions under π̄ followed by the
kernel with mass function (a, b_T) ↦ W_T^{b_T} ∏_{t,n} B_t(a_t^n|n).
The proof of Lemma 3 in the supplement is not ours and is provided for completeness and ease of
reference. The first part of Lemma 3 is due to Andrieu et al. (2010), in the form of Chopin and
Singh (2015, Section 2.3). The second part is the observation of Chopin and Singh (2015, proof of
Proposition 9).
Lemma 4 (lem:pair, Section 3).
'Let x_{1:T} ∼ π and run Algorithm 1. Conditionally on x, b_T ∼ W_T and, given b_T,
l_T ∼ K_T(b_T, ·). For t ∈ [T - 1], conditionally on x and (b_{t+1:T}, l_{t+1:T}),
b_t ∼ B_t(·|b_{t+1}) and, given b_t, l_t ∼ K_{t,b_{t+1},l_{t+1}}(b_t, ·). If
K_{t,j,j'}(i, ·) = B_t(·|j') for all j ≠ j' and t ∈ [T - 1], the same holds with
l_t ∼ K_{t,l_{t+1},l_{t+1}}(a_t^{l_{t+1}}, ·) in Algorithm 1.d.'
The conditional distributions of the first two sentences are those of the backward Markov chain
pairChain K on pairs of indices, whose trajectories have the probabilities
W_T^{b_T} K_T(b_T, l_T) ∏_t B_t(b_t|b_{t+1}) K_{t,b_{t+1},l_{t+1}}(b_t, l_t). By Lemma 3, the
particle positions have their distribution under π̄.
Proposition 1 (prop:reversible, Section 3).
'For any kernels K_T and K_{t,j,j'} as in Algorithm 1, the Markov kernel defined by
Algorithm 1 is reversible with respect to π. In particular, it leaves π invariant.'
The three conjuncts state that the kernel defined by Algorithm 1 is a Markov kernel, is reversible
with respect to π, and leaves π invariant.
Section 4: comparison of the selection rules #
Theorem 1 (thm:ordering, Section 4.1), first part.
'Let t ∈ [T] and let f : X → ℝ be measurable with ∫ f(x_t)² π(x_{1:T}) dx_{1:T} < ∞. Then
E_{M-BS}{f(x_t) f(x̃_t)} ≤ E_{FM-BS}{f(x_t) f(x̃_t)} ≤ E_{BS}{f(x_t) f(x̃_t)} ≤ E_{AT}{f(x_t) f(x̃_t)},
and the first inequality also holds with CM-BS in place of M-BS.'
Formalization: the square-integrability is MemLp with exponent 2, which includes the
measurability of x ↦ f(x_t) up to a null set, so that the measurability of f is not used in the
proof.
Theorem 1 (thm:ordering, Section 4.1), second part.
'Moreover, P_{M-BS}(x̃_t ≠ x_t) ≥ P_{FM-BS}(x̃_t ≠ x_t) ≥ P_{BS}(x̃_t ≠ x_t) ≥ P_{AT}(x̃_t ≠ x_t),
and the first inequality also holds with CM-BS in place of M-BS.'
Formalization: the diagonal of X × X is measurable.
Corollary 1 (cor:pairs, Section 4.1), first part.
'Let t ∈ [T - 1] and let f : X² → ℝ be measurable with
∫ f(x_t, x_{t+1})² π(x_{1:T}) dx_{1:T} < ∞. Then
E_{M-BS}{f(x_t, x_{t+1}) f(x̃_t, x̃_{t+1})} ≤ E_{FM-BS}{f(x_t, x_{t+1}) f(x̃_t, x̃_{t+1})} ≤ E_{BS}{f(x_t, x_{t+1}) f(x̃_t, x̃_{t+1})} ≤ E_{AT}{f(x_t, x_{t+1}) f(x̃_t, x̃_{t+1})}.'
Formalization: the square-integrability is MemLp with exponent 2, which includes the
measurability of x ↦ f(x_t, x_{t+1}) up to a null set, so that the measurability of f is not
used in the proof.
Corollary 1 (cor:pairs, Section 4.1), second part.
'If, moreover, the particles at time t and those at time t + 1 are almost surely pairwise
distinct under π̄, then the probabilities of {(x̃_t, x̃_{t+1}) ≠ (x_t, x_{t+1})} are
nonincreasing from M-BS to FM-BS, BS, and AT, and are at least as large under CM-BS as under
FM-BS.'
Formalization: the diagonal of X × X is measurable.
Proposition 2 (prop:washout, Section 4.2).
'Let t ∈ [T]. Then
0 ≤ P_{FM-BS}(x̃_t ≠ x_t) - P_{BS}(x̃_t ≠ x_t) ≤ E(∏_{s=t}^{T-1} β_s),
where the expectation is taken under π̄. If there is ε ∈ (0, 1] such that
m_{s+1}(x, ·) ≥ ε m_{s+1}(x', ·) for all x, x' ∈ X and s ∈ [T - 1], then the right-hand side
is at most (1 - ε)^{T-t}.'
With T = n + 1 and the time t.val + 1 of the paper, T - t = n - t.val. The backward steps
s ≥ t are those with t ≤ s.castSucc. The inequality between the densities is assumed at every
point.
Formalization: the diagonal of X × X is measurable.
Proposition 3 (prop:gain, Section 4.2).
'Let t ∈ [T - 1] and assume that the particles x_t^1, …, x_t^N are almost surely pairwise
distinct under π̄. For j, j' ∈ [N], let
γ_t(j, j') := ∑_i B_t(i|j) {B_t(i|j') - K_{t,j,j'}(i, i)}, with the kernels K_{t,j,j'} of
M-BS. Then γ_t(j, j') ≥ 0 and
P_{M-BS}(x̃_t ≠ x_t) - P_{FM-BS}(x̃_t ≠ x_t) ≥ E_{M-BS}{γ_t(b_{t+1}, l_{t+1})}.
The same holds with CM-BS in place of M-BS, in both the kernels and the inequality.'
Formalization: the diagonal of X × X is measurable.
Values of the gains for two particles (Section 4.2).
'For N = 2, γ_t(j, j) = 2{1 - max_i B_t(i|j)}² for both rules. [...] For CM-BS, the gain is
also made at the other times, with γ_t(j, j') = 2 min_i B_t(i|j) B_t(i|j') for N = 2 and
j ≠ j'.'
The coupling kernel for two particles (Section 4.3).
'With two particles, C_{p,p} = F_p for every probability vector p'.
Proposition 4 (prop:imh, Section 4.3).
'Let N = 2, and assume that, for s ∈ [T - 1], m_{s+1}(x, x') does not depend on x. Then,
under CM-BS and conditionally on x and b_{1:T}, the indices l_1, …, l_T are independent, with
l_t ∼ F_{W_t}(b_t, ·).'
The conclusion states that the joint distribution of the particle positions, the indices of the
reference, and the indices of the output is the distribution of the first two followed by the
kernel with mass function l ↦ ∏_t F_{W_t}(b_t, l_t).
Probabilities with uniform weights (Section 4.3).
'If the probabilities W_T and B_t(·|j), t ∈ [T - 1], j ∈ [N], are uniform [...] By Lemma 4,
l_t ≠ b_t almost surely for every t ∈ [T] under CM-BS, whereas P_𝐱(l_t = b_t) = 1/N under
BS, and under FM-BS for t < T. Under M-BS, [...] P_𝐱(l_t = b_t) = (1 - (-1/N)^{T-t}) / (N + 1)'.
P_𝐱 is the probability conditional on the particle positions 𝐱: by Lemma 4, P_𝐱(l_t = b_t) is
∑_i marg W B K t i i with the final weights W, the backward-sampling probabilities B, and the
kernels K of the rule. With T = n + 1 and the time t.val + 1 of the paper,
T - t = n - t.val.
Section S3: potential functions of the previous state and other resampling schemes #
Lemma S1 (lem:extended-previous, Section S3.2).
'Let x_{1:T} ∼ π and run steps (a) and (b) of Algorithm S1, with c drawn from the kernels
K_{t,j,j} of one of the six selection rules. Then x_{1:T} = (x_1^{b_1}, …, x_T^{b_T}) and
(x, a, b_{1:T}) has the density (S4).'
The resampling schemes r_t (Definition S1) are resdist.
The first conjunct states that the joint distribution of the reference trajectory and of
(x, a, b_{1:T}) is the image of the distribution of (x, a, b_{1:T}) under the map which adds
(x_1^{b_1}, …, x_T^{b_T}), so that x_{1:T} = (x_1^{b_1}, …, x_T^{b_T}).
Formalization: the resampling schemes are measurable functions of the particles and the weights.
The marginal density of (x, a) (Section S3.2, after Lemma S1).
'The density (S4) is the product of a function of (x, a) and of
W_T^{b_T} ∏_{t=1}^{T-1} K_{t,b_{t+1},b_{t+1}}(a_t^{b_{t+1}}, b_t), which is a probability
distribution of b_{1:T}. Hence the marginal density of (x, a) does not depend on the selection
rule. Conditionally on (x, a), b_T ∼ W_T and, for t = T - 1, …, 1, given also b_{t+1:T},
b_t ∼ K_{t,b_{t+1},b_{t+1}}(a_t^{b_{t+1}}, ·).'
The function of (x, a) is posAncDensity. The distribution with this density, posAncMeasure,
does not depend on the selection rule. The kernel refChain r.diagKernel has
the mass function b_{1:T} ↦ W_T^{b_T} ∏_t K_{t,b_{t+1},b_{t+1}}(a_t^{b_{t+1}}, b_t), under which
b_T ∼ W_T and, given b_{t+1:T}, b_t ∼ K_{t,b_{t+1},b_{t+1}}(a_t^{b_{t+1}}, ·).
The three conjuncts state that this mass function is a probability distribution of b_{1:T},
that (x, a) has the distribution posAncMeasure, and that (x, a, b_{1:T}) has the distribution
of (x, a) followed by refChain r.diagKernel.
Formalization: the resampling schemes are measurable functions of the particles and the weights.
Converse of Lemma S1 (Section S3.2).
'Conversely, by Lemma S1, if (x, a, b_{1:T}) has the density (S4), then
(x_1^{b_1}, …, x_T^{b_T}) ∼ π.'
Formalization: the resampling schemes are measurable functions of the particles and the weights.
Proposition S1 (prop:previous-state, Section S3.2).
'For any kernels K_T and K_{t,j,j'} as in Algorithm S1, the Markov kernel defined by
Algorithm S1 is reversible with respect to π.'
The two conjuncts state that the kernel defined by Algorithm S1 is a Markov kernel and is
reversible with respect to π.
Formalization: the resampling schemes are measurable functions of the particles and the weights.
Proposition S2 (prop:orderings, Section S3.2), first part of Theorem 1.
'Let x̃_{1:T} be the output of Algorithm S1 started from x_{1:T} ∼ π. Theorem 1, Corollary 1,
and Propositions 2 and 3 of the main text hold with the probabilities (S3), with the distribution
(S4) in place of π̄, and, in Proposition 2, with
m_{s+1}(x, ·) g_{s+1}(x, ·) ≥ ε m_{s+1}(x', ·) g_{s+1}(x', ·) in place of the condition on
m_{s+1}.'
Formalization: the resampling schemes are measurable functions of the particles and the weights.
Proposition S2 (prop:orderings, Section S3.2), second part of Theorem 1: the update rates
of Algorithm S1 are ordered as in Theorem 1.
Formalization: the resampling schemes are measurable functions of the particles and the weights.
The diagonal of X × X is measurable.
Proposition S2 (prop:orderings, Section S3.2), first part of Corollary 1 for
Algorithm S1.
Formalization: the resampling schemes are measurable functions of the particles and the weights.
Proposition S2 (prop:orderings, Section S3.2), second part of Corollary 1 for
Algorithm S1, with the distribution (S4) of Algorithm S1 in place of π̄.
Formalization: the resampling schemes are measurable functions of the particles and the weights.
The diagonal of X × X is measurable.
Proposition S2 (prop:orderings, Section S3.2), Proposition 2 for Algorithm S1, with the
distribution (S4) of Algorithm S1 in place of π̄ and the condition
m_{s+1}(x, ·) g_{s+1}(x, ·) ≥ ε m_{s+1}(x', ·) g_{s+1}(x', ·).
Formalization: the resampling schemes are measurable functions of the particles and the weights.
The diagonal of X × X is measurable.
Proposition S2 (prop:orderings, Section S3.2), Proposition 3 for Algorithm S1, with the
distribution (S4) of Algorithm S1 in place of π̄ and the probabilities (S3) in the gains.
Formalization: the resampling schemes are measurable functions of the particles and the weights.
The diagonal of X × X is measurable.
Proposition S3 (prop:reduction, Section S3.2).
'Assume multinomial resampling, and that g_t(x_{t-1}, x_t) does not depend on x_{t-1} for
2 ≤ t ≤ T. Then, for x_{1:T} ∼ π and any kernels as in Algorithm 1, the reference and the output
have the same joint distribution under Algorithm S1 as under Algorithm 1.'
The model M' of Section S3 has the densities of the model M of the main text, with the
potential functions g_1 and g_t(x_{t-1}, x_t) = g_t(x_t) of M.
Proposition S4 (prop:ancestors, Section S3.3).
'The Markov kernel defined by Algorithm S2 leaves π invariant. With the kernels of AT and FM-AT,
it is reversible with respect to π.'
In Algorithm S2, the kernels are those of AT, FM-AT, BS, FM-BS, or M-BS.
Formalization: the resampling schemes are measurable functions of the particles and the weights.
Ancestor sampling in Algorithm S2 (Section S3.3, after Proposition S4).
'The proof uses Algorithm S2.a only through b_T ∼ W_T conditionally on (x, a), which holds for
all the kernels of Lemma S1, so that the invariance also holds with ancestor sampling in
Algorithm S2.a.'
In the Markov kernel csmcAncWith resdist C r, c is drawn in Algorithm S2.a from
C(B_t(·|x_{t+1}))(b_t, ·), as in Lemma S1, in place of c = b_t. The kernels of steps (b) and
(c) are those of the selection rule r.
The first conjunct is the invariance with ancestor sampling, that is, with the Gibbs kernels
C(p)(i, ·) = p. The second is the invariance with the kernels K_{t,j,j} of each of the six
selection rules r', those of Lemma S1.
In Algorithm S2, the kernels are those of AT, FM-AT, BS, FM-BS, or M-BS.
Formalization: the resampling schemes are measurable functions of the particles and the weights.