Orderings of the selection rules at fixed particle positions

The results of Section 4 of the paper are inequalities between expectations, under the distribution of the particle positions, of quantities which depend on the positions only through the final weights W and the backward-sampling probabilities B. The orderings of these quantities are proved here for every W and B whose entries form probability vectors:

• the ordering (S1) of the supplementary material, Q_t^{M-BS}(φ) ≤ Q_t^{FM-BS}(φ) ≤ Q_t^{BS}(φ) ≤ Q_t^{AT}(φ), together with Q_t^{CM-BS}(φ) ≤ Q_t^{FM-BS}(φ), from which Theorem 1 follows;
• the decomposition of the probability that the states of the output and of the reference are equal into a sum of expected products of indicator functions, over the classes of equal particles, from which the ordering of the update rates in Theorem 1 follows without any assumption on the particles;
• the orderings for functions of the indices at two consecutive times, from which Corollary 1 follows;
• the bounds on the difference between the update rates of FM-BS and BS, from which Proposition 2 follows;
• the lower bound on the gain of M-BS and CM-BS over FM-BS, from which Proposition 3 follows.

In the item on Corollary 1, the probability that the indices of the output and of the reference coincide at the times t and t + 1 is ∑_j P_𝐱(b_{t+1} = l_{t+1} = j) ∑_i B_t(i|j) K_{t,j,j}(i, i). In the item on Proposition 3, the probability that they coincide at time t is ∑_i Q_t(1_{i}).

theorem CSMC.marg_kernels_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} (r : SelectionRule) {W : ι → ℝ} {B : Fin n → Matrix ι ι ℝ} (hW : IsProbVector W) (hB : ∀ (s : Fin n) (j : ι), IsProbVector fun (i : ι) => B s i j) (t : Fin (n + 1)) (i i' : ι) : 0 ≤ marg W B (r.kernels W B) t i i'

Under the kernels of a selection rule, the probabilities P_𝐱(b_t = i, l_t = i') are nonnegative.

theorem CSMC.expprod_ordering {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {W : ι → ℝ} {B : Fin n → Matrix ι ι ℝ} (hW : IsProbVector W) (hB : ∀ (s : Fin n) (j : ι), IsProbVector fun (i : ι) => B s i j) (t : Fin (n + 1)) (φ : ι → ℝ) : expprod W B (SelectionRule.MBS.kernels W B) t φ ≤ expprod W B (SelectionRule.FMBS.kernels W B) t φ ∧ expprod W B (SelectionRule.FMBS.kernels W B) t φ ≤ expprod W B (SelectionRule.BS.kernels W B) t φ ∧ expprod W B (SelectionRule.BS.kernels W B) t φ ≤ expprod W B (SelectionRule.AT.kernels W B) t φ ∧ expprod W B (SelectionRule.CMBS.kernels W B) t φ ≤ expprod W B (SelectionRule.FMBS.kernels W B) t φ

The ordering (S1) of the expected products Q_t(φ) under the selection rules, together with Q_t^{CM-BS}(φ) ≤ Q_t^{FM-BS}(φ).

theorem CSMC.sum_marg_eq_sum_expprod {ι : Type u_1} [Fintype ι] {n : ℕ} {α : Type u_2} [DecidableEq α] (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) (t : Fin (n + 1)) (v : ι → α) : (∑ i : ι, ∑ i' : ι, if v i = v i' then marg W B K t i i' else 0) = ∑ c ∈ Finset.image v Finset.univ, expprod W B K t fun (i : ι) => if v i = c then 1 else 0

For the positions v i of the particles at time t, the probability that the states of the output and of the reference at time t are equal is the sum of Q_t(1_S) over the classes S of indices whose particles are equal.

theorem CSMC.sum_sum_gibbs {ι : Type u_1} [Fintype ι] (p q ψ ψ' : ι → ℝ) : ∑ i : ι, ∑ i' : ι, p i * gibbs q i i' * ψ i * ψ' i' = expect p ψ * expect q ψ'

For the Gibbs kernel K(i, ·) = q, ∑_{i, i'} p_i K(i, i') ψ(i) ψ'(i') = p(ψ) q(ψ').

theorem CSMC.expprod_indicator {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) (t : Fin (n + 1)) (j : ι) : (expprod W B K t fun (i : ι) => if i = j then 1 else 0) = marg W B K t j j

Q_t(1_{j}) = P_𝐱(b_t = l_t = j).

theorem CSMC.expprodPair_ordering {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {W : ι → ℝ} {B : Fin n → Matrix ι ι ℝ} (hW : IsProbVector W) (hB : ∀ (s : Fin n) (j : ι), IsProbVector fun (i : ι) => B s i j) (s : Fin n) (φ : ι → ι → ℝ) : expprodPair W B (SelectionRule.MBS.kernels W B) s φ ≤ expprodPair W B (SelectionRule.FMBS.kernels W B) s φ ∧ expprodPair W B (SelectionRule.FMBS.kernels W B) s φ ≤ expprodPair W B (SelectionRule.BS.kernels W B) s φ ∧ expprodPair W B (SelectionRule.BS.kernels W B) s φ ≤ expprodPair W B (SelectionRule.AT.kernels W B) s φ

The ordering of the expected products of a function of the indices at two consecutive times, under AT, BS, FM-BS, and M-BS (proof of Corollary 1).

theorem CSMC.coincidence_pair_ordering {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {W : ι → ℝ} {B : Fin n → Matrix ι ι ℝ} (hW : IsProbVector W) (hB : ∀ (s : Fin n) (j : ι), IsProbVector fun (i : ι) => B s i j) (s : Fin n) : have P := fun (r : SelectionRule) => ∑ j : ι, marg W B (r.kernels W B) s.succ j j * ∑ i : ι, B s i j * (r.kernels W B).step s j j i i; P SelectionRule.MBS ≤ P SelectionRule.FMBS ∧ P SelectionRule.FMBS ≤ P SelectionRule.BS ∧ P SelectionRule.BS ≤ P SelectionRule.AT ∧ P SelectionRule.CMBS ≤ P SelectionRule.FMBS

The ordering of the probabilities that the indices of the output and of the reference coincide at two consecutive times, ∑_j P_𝐱(b_{t+1} = l_{t+1} = j) ∑_i B_t(i|j) K_{t,j,j}(i, i) (proof of Corollary 1).

noncomputable def CSMC.stepProd {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} (B : Fin n → Matrix ι ι ℝ) : Fin (n + 1) → Matrix ι ι ℝ

The product B_t B_{t+1} ⋯ B_{T-1} of the matrices of the backward steps from time t, which is the identity matrix at the final time.

Equations

• CSMC.stepProd B = Fin.reverseInduction 1 fun (s : Fin n) (M : Matrix ι ι ℝ) => B s * M

theorem CSMC.stepProd_last {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} (B : Fin n → Matrix ι ι ℝ) : stepProd B (Fin.last n) = 1

At the final time, stepProd is the identity matrix.

theorem CSMC.stepProd_castSucc {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} (B : Fin n → Matrix ι ι ℝ) (s : Fin n) : stepProd B s.castSucc = B s * stepProd B s.succ

The backward recursion of stepProd.

theorem CSMC.isProbVector_stepProd {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {B : Fin n → Matrix ι ι ℝ} (hB : ∀ (s : Fin n) (j : ι), IsProbVector fun (i : ι) => B s i j) (t : Fin (n + 1)) (j : ι) : IsProbVector fun (i : ι) => stepProd B t i j

If the columns of the B_s are probability vectors, so are those of their products.

theorem CSMC.dobrushin_stepProd_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {B : Fin n → Matrix ι ι ℝ} (hB : ∀ (s : Fin n) (j : ι), IsProbVector fun (i : ι) => B s i j) (t : Fin (n + 1)) : dobrushin (stepProd B t) ≤ ∏ s : Fin n with t ≤ s.castSucc, dobrushin (B s)

The Dobrushin coefficient of B_t ⋯ B_{T-1} is at most ∏_{s=t}^{T-1} β_s.

theorem CSMC.expprod_eq_expprod_last {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {W : ι → ℝ} {B : Fin n → Matrix ι ι ℝ} {K : BackwardKernels ι n} (hD : ∀ (s : Fin n) (j j' : ι) (φ : ι → ℝ), excess B K s j j' φ = 0) (t : Fin (n + 1)) (φ : ι → ℝ) : expprod W B K t φ = expprod W B K (Fin.last n) (Matrix.vecMul φ (stepProd B t))

If the excess vanishes, as for BS and FM-BS, then Q_t(φ) = Q_T(B_{T-1} ⋯ B_t φ).

theorem CSMC.sum_variance_le_dobrushin {ι : Type u_1} [Fintype ι] {α : Type u_2} [DecidableEq α] {M : Matrix ι ι ℝ} (hM : ∀ (j : ι), IsProbVector fun (i : ι) => M i j) {W : ι → ℝ} (hW : IsProbVector W) (v : ι → α) : ∑ c ∈ Finset.image v Finset.univ, (expect W (Matrix.vecMul (fun (i : ι) => if v i = c then 1 else 0) M ^ 2) - expect W (Matrix.vecMul (fun (i : ι) => if v i = c then 1 else 0) M) ^ 2) ≤ dobrushin M

For a matrix M whose columns are probability vectors, a probability vector W, and the positions v i of the particles, the sum over the classes c of equal positions of the variances under W of ψ_c = 1_{v = c} ᵥ* M is at most the Dobrushin coefficient of M (proof of Proposition 2).

theorem CSMC.washout_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {W : ι → ℝ} {B : Fin n → Matrix ι ι ℝ} (hW : IsProbVector W) (hB : ∀ (s : Fin n) (j : ι), IsProbVector fun (i : ι) => B s i j) (t : Fin (n + 1)) {α : Type u_2} [DecidableEq α] (v : ι → α) : have D := ∑ c ∈ Finset.image v Finset.univ, ((expprod W B (SelectionRule.BS.kernels W B) t fun (i : ι) => if v i = c then 1 else 0) - expprod W B (SelectionRule.FMBS.kernels W B) t fun (i : ι) => if v i = c then 1 else 0); 0 ≤ D ∧ D ≤ ∏ s : Fin n with t ≤ s.castSucc, dobrushin (B s)

Proposition 2 at fixed particle positions: for the positions v i of the particles at time t, the probability that the states of the output and of the reference at time t are equal is larger under BS than under FM-BS, by at most the product of the Dobrushin coefficients of the B_s for s ≥ t.

theorem CSMC.sum_excess_indicator {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) (s : Fin n) (j j' : ι) : (∑ i : ι, excess B K s j j' fun (k : ι) => if k = i then 1 else 0) = -gain B K s j j'

The sum over i of the excess at the indicator of {i} is minus the gain: ∑_i D_{t,j,j'}(1_{i}) = -γ_t(j, j').

theorem CSMC.gain_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {r : SelectionRule} (hr : r = SelectionRule.MBS ∨ r = SelectionRule.CMBS) {W : ι → ℝ} {B : Fin n → Matrix ι ι ℝ} (hW : IsProbVector W) (hB : ∀ (s : Fin n) (j : ι), IsProbVector fun (i : ι) => B s i j) (s : Fin n) : (∀ (j j' : ι), 0 ≤ gain B (r.kernels W B) s j j') ∧ (∑ i : ι, expprod W B (r.kernels W B) s.castSucc fun (k : ι) => if k = i then 1 else 0) ≤ (∑ i : ι, expprod W B (SelectionRule.FMBS.kernels W B) s.castSucc fun (k : ι) => if k = i then 1 else 0) - ∑ j : ι, ∑ j' : ι, marg W B (r.kernels W B) s.succ j j' * gain B (r.kernels W B) s j j'

Proposition 3 at fixed particle positions: for M-BS and CM-BS, the gains γ_t(j, j') are nonnegative. Under either rule, the probability that the indices of the output and of the reference coincide at time t is smaller than under FM-BS by at least the expected gain ∑_{j, j'} P_𝐱(b_{t+1} = j, l_{t+1} = j') γ_t(j, j').