The backward Markov chain of the indices of the reference and of the output

At fixed particle positions, the backward pass of Algorithm 1 of the paper depends on the normalized weights W = W_T at the final time, the backward-sampling probabilities B_s(i|j) = B s i j, and the Markov kernels K_T and K_{t,j,j'} on the indices of the particles. By Lemma 4 of the paper, the pairs (b_t, l_t) of the indices of the reference and of the output then form a Markov chain backwards in time, with initial distribution W(b_T) K_T(b_T, l_T) and transition probabilities B_t(b_t|b_{t+1}) K_{t, b_{t+1}, l_{t+1}}(b_t, l_t).

The definitions are the kernels of Algorithm 1 at fixed positions, its hypotheses (Admissible: the reversibility of K_T with respect to W and eq. (3)), the probability pathProb of a pair of sequences of indices under this chain, its marginals marg, the expected products Q_t(φ) = E_𝐱[φ(b_t) φ(l_t)] (expprod), the excess D_{t,j,j'}(φ) (excess), and the gain γ_t(j, j') (gain) of Section 4. The results are the invariance of pathProb under the exchange of the indices of the reference and of the output, which is Proposition 1 at fixed particle positions, and the recursion (7). The expected products of a function of the indices at two consecutive times, for the proof of Corollary 1, are expprodPair.

With B s ∈ Matrix ι ι ℝ, the function (B_s φ)(j) = ∑_i B_s(i|j) φ(i) is φ ᵥ* B s.

structure CSMC.BackwardKernels (ι : Type u_1) (n : ℕ) : Type u_1

The Markov kernels of Algorithm 1 at fixed particle positions, with final the kernel K_T and step s j j' the kernel K_{t,j,j'} at the step s of the backward pass, from time s.succ to time s.castSucc.

• final : Matrix ι ι ℝ

  The kernel K_T, from which the index l_T of the output is drawn given the index b_T of the reference.

• step : Fin n → ι → ι → Matrix ι ι ℝ

  The kernels K_{t,j,j'}: step s j j' i i' is the probability that the index of the output at time s.castSucc is i', given that the index of the reference at that time is i and that the indices of the reference and of the output at time s.succ are j and j'.

structure CSMC.Admissible {ι : Type u_1} [Fintype ι] {n : ℕ} [DecidableEq ι] (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) : Prop

The hypotheses of Algorithm 1 on its kernels, at fixed particle positions with final weights W and backward-sampling probabilities B: K_T is a Markov kernel reversible with respect to W, the kernels K_{t,j,j'} are Markov kernels, and eq. (3) holds: B_t(i|j) K_{t,j,j'}(i, i') = B_t(i'|j') K_{t,j',j}(i', i).

• final_mem : K.final ∈ Matrix.rowStochastic ℝ ι

  K_T is a Markov kernel.

• final_isReversible : IsReversible W K.final

  K_T is reversible with respect to W.

• step_mem (s : Fin n) (j j' : ι) : K.step s j j' ∈ Matrix.rowStochastic ℝ ι

  The kernels K_{t,j,j'} are Markov kernels.

• symmetry (s : Fin n) (j j' i i' : ι) : B s i j * K.step s j j' i i' = B s i' j' * K.step s j' j i' i

  Eq. (3).

def CSMC.pairInit {ι : Type u_1} {n : ℕ} (W : ι → ℝ) (K : BackwardKernels ι n) (jj : ι × ι) : ℝ

The distribution W(j) K_T(j, j') of the pair (b_T, l_T) at the final time.

Equations

• CSMC.pairInit W K jj = W jj.1 * K.final jj.1 jj.2

def CSMC.pairStep {ι : Type u_1} {n : ℕ} (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) (s : Fin n) (jj ii : ι × ι) : ℝ

The probability B_t(i|j) K_{t,j,j'}(i, i') of the transition of the pairs (b_t, l_t) from (j, j') at time s.succ to (i, i') at time s.castSucc.

Equations

• CSMC.pairStep B K s jj ii = B s ii.1 jj.1 * K.step s jj.1 jj.2 ii.1 ii.2

def CSMC.pathProb {ι : Type u_1} {n : ℕ} (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) (b l : Fin (n + 1) → ι) : ℝ

The probability of the indices b of the reference and l of the output, given the particle positions, by Lemma 4: W(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).

Equations

• CSMC.pathProb W B K b l = CSMC.chainProb (CSMC.pairInit W K) (CSMC.pairStep B K) fun (t : Fin (n + 1)) => (b t, l t)

def CSMC.marg {ι : Type u_1} [Fintype ι] {n : ℕ} (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) (t : Fin (n + 1)) (i i' : ι) : ℝ

The probability P_𝐱(b_t = i, l_t = i'), conditional on the particle positions 𝐱, by backward recursion.

Equations

• CSMC.marg W B K t i i' = CSMC.chainMarg (CSMC.pairInit W K) (CSMC.pairStep B K) t (i, i')

def CSMC.expprod {ι : Type u_1} [Fintype ι] {n : ℕ} (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) (t : Fin (n + 1)) (φ : ι → ℝ) : ℝ

The expected product Q_t(φ) = E_𝐱[φ(b_t) φ(l_t)], conditional on the particle positions 𝐱 (Section 4.1).

Equations

• CSMC.expprod W B K t φ = ∑ i : ι, ∑ i' : ι, CSMC.marg W B K t i i' * φ i * φ i'

def CSMC.excess {ι : Type u_1} [Fintype ι] {n : ℕ} (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) (s : Fin n) (j j' : ι) (φ : ι → ℝ) : ℝ

The excess D_{t,j,j'}(φ) = ⟨φ, K_{t,j,j'} φ⟩_{B_t(·|j)} - (B_t φ)(j) (B_t φ)(j') (Section 4.1).

Equations

• CSMC.excess B K s j j' φ = CSMC.dirForm (fun (i : ι) => B s i j) (K.step s j j') φ - Matrix.vecMul φ (B s) j * Matrix.vecMul φ (B s) j'

def CSMC.gain {ι : Type u_1} [Fintype ι] {n : ℕ} (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) (s : Fin n) (j j' : ι) : ℝ

The gain γ_t(j, j') = ∑_i B_t(i|j) (B_t(i|j') - K_{t,j,j'}(i, i)) (Proposition 3).

Equations

• CSMC.gain B K s j j' = ∑ i : ι, B s i j * (B s i j' - K.step s j j' i i)

def CSMC.expprodPair {ι : Type u_1} [Fintype ι] {n : ℕ} (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) (s : Fin n) (φ : ι → ι → ℝ) : ℝ

The expected product E_𝐱[φ(b_t, b_{t+1}) φ(l_t, l_{t+1})], conditional on the positions, for a function φ of the indices at the times s.castSucc and s.succ: the sum over j and j' of P_𝐱(b_{t+1} = j, l_{t+1} = j') times the expression (8), ∑_{i, i'} B_t(i|j) K_{t,j,j'}(i, i') φ(i, j) φ(i', j') (Section 4.1).

Equations

• CSMC.expprodPair W B K s φ = ∑ j : ι, ∑ j' : ι, CSMC.marg W B K s.succ j j' * ∑ i : ι, ∑ i' : ι, B s i j * K.step s j j' i i' * φ i j * φ i' j'

theorem CSMC.sum_comm_four {ι : Type u_1} [Fintype ι] {M : Type u_2} [AddCommMonoid M] (F : ι → ι → ι → ι → M) : ∑ i : ι, ∑ i' : ι, ∑ j : ι, ∑ j' : ι, F i i' j j' = ∑ j : ι, ∑ j' : ι, ∑ i : ι, ∑ i' : ι, F i i' j j'

Exchange of the order of summation over four indices: (i, i', j, j') to (j, j', i, i').

theorem CSMC.pathProb_eq {ι : Type u_1} {n : ℕ} (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) (b l : Fin (n + 1) → ι) : pathProb W B K b l = W (b (Fin.last n)) * K.final (b (Fin.last n)) (l (Fin.last n)) * ∏ s : Fin n, B s (b s.castSucc) (b s.succ) * K.step s (b s.succ) (l s.succ) (b s.castSucc) (l s.castSucc)

pathProb is the product of Lemma 4.

theorem CSMC.pathProb_swap {ι : Type u_1} [Fintype ι] {n : ℕ} [DecidableEq ι] {W : ι → ℝ} {B : Fin n → Matrix ι ι ℝ} {K : BackwardKernels ι n} (hK : Admissible W B K) (b l : Fin (n + 1) → ι) : pathProb W B K l b = pathProb W B K b l

Proposition 1 at fixed particle positions: under the hypotheses of Algorithm 1, the probability of the indices of the reference and of the output does not change when they are exchanged.

theorem CSMC.marg_last {ι : Type u_1} [Fintype ι] {n : ℕ} (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) (i i' : ι) : marg W B K (Fin.last n) i i' = W i * K.final i i'

The probability P_𝐱(b_T = i, l_T = i') is W i * K_T(i, i').

theorem CSMC.marg_castSucc {ι : Type u_1} [Fintype ι] {n : ℕ} (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) (s : Fin n) (i i' : ι) : marg W B K s.castSucc i i' = ∑ j : ι, ∑ j' : ι, marg W B K s.succ j j' * (B s i j * K.step s j j' i i')

The backward recursion of the probabilities P_𝐱(b_t = i, l_t = i').

theorem CSMC.marg_nonneg {ι : Type u_1} [Fintype ι] {n : ℕ} {W : ι → ℝ} {B : Fin n → Matrix ι ι ℝ} {K : BackwardKernels ι n} (hW : ∀ (i : ι), 0 ≤ W i) (hB : ∀ (s : Fin n) (i j : ι), 0 ≤ B s i j) (hKf : ∀ (i i' : ι), 0 ≤ K.final i i') (hKs : ∀ (s : Fin n) (j j' i i' : ι), 0 ≤ K.step s j j' i i') (t : Fin (n + 1)) (i i' : ι) : 0 ≤ marg W B K t i i'

If the weights, the backward-sampling probabilities, and the kernels are nonnegative, so are the probabilities P_𝐱(b_t = i, l_t = i').

theorem CSMC.sum_marg {ι : Type u_1} [Fintype ι] {n : ℕ} [DecidableEq ι] {W : ι → ℝ} {B : Fin n → Matrix ι ι ℝ} {K : BackwardKernels ι n} (hW : ∑ i : ι, W i = 1) (hKf : K.final ∈ Matrix.rowStochastic ℝ ι) (hB : ∀ (s : Fin n) (j : ι), ∑ i : ι, B s i j = 1) (hKs : ∀ (s : Fin n) (j j' : ι), K.step s j j' ∈ Matrix.rowStochastic ℝ ι) (t : Fin (n + 1)) : ∑ i : ι, ∑ i' : ι, marg W B K t i i' = 1

If W and the columns of the B_s sum to one and if K_T and the K_{t,j,j'} are Markov kernels, then the probabilities P_𝐱(b_t = i, l_t = i') sum to one.

theorem CSMC.sum_pathProb_eq_marg {ι : Type u_1} [Fintype ι] {n : ℕ} [DecidableEq ι] {W : ι → ℝ} {B : Fin n → Matrix ι ι ℝ} {K : BackwardKernels ι n} (hB : ∀ (s : Fin n) (j : ι), ∑ i : ι, B s i j = 1) (hK : ∀ (s : Fin n) (j j' : ι), K.step s j j' ∈ Matrix.rowStochastic ℝ ι) (t : Fin (n + 1)) (i i' : ι) : (∑ b : Fin (n + 1) → ι, ∑ l : Fin (n + 1) → ι, if b t = i ∧ l t = i' then pathProb W B K b l else 0) = marg W B K t i i'

If the columns of the B_s sum to one and the K_{t,j,j'} are Markov kernels, the sum of pathProb over the sequences of indices with b_t = i and l_t = i' is marg t i i'.

theorem CSMC.expprod_last {ι : Type u_1} [Fintype ι] {n : ℕ} (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) (φ : ι → ℝ) : expprod W B K (Fin.last n) φ = dirForm W K.final φ

The expected product at the final time: Q_T(φ) = ⟨φ, K_T φ⟩_W.

theorem CSMC.expprod_castSucc {ι : Type u_1} [Fintype ι] {n : ℕ} (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (K : BackwardKernels ι n) (s : Fin n) (φ : ι → ℝ) : expprod W B K s.castSucc φ = expprod W B K s.succ (Matrix.vecMul φ (B s)) + ∑ j : ι, ∑ j' : ι, marg W B K s.succ j j' * excess B K s j j' φ

The recursion (7): Q_t(φ) = Q_{t+1}(B_t φ) + ∑_{j, j'} P_𝐱(b_{t+1} = j, l_{t+1} = j') D_{t,j,j'}(φ).

theorem CSMC.pathProb_nonneg {ι : Type u_1} {n : ℕ} {W : ι → ℝ} {B : Fin n → Matrix ι ι ℝ} {K : BackwardKernels ι n} (hW : ∀ (i : ι), 0 ≤ W i) (hB : ∀ (s : Fin n) (i j : ι), 0 ≤ B s i j) (hKf : ∀ (i i' : ι), 0 ≤ K.final i i') (hKs : ∀ (s : Fin n) (j j' i i' : ι), 0 ≤ K.step s j j' i i') (b l : Fin (n + 1) → ι) : 0 ≤ pathProb W B K b l

If the weights, the backward-sampling probabilities, and the kernels are nonnegative, so is pathProb.

theorem CSMC.sum_pairStep {ι : Type u_1} [Fintype ι] {n : ℕ} [DecidableEq ι] {B : Fin n → Matrix ι ι ℝ} {K : BackwardKernels ι n} (hB : ∀ (s : Fin n) (j : ι), ∑ i : ι, B s i j = 1) (hK : ∀ (s : Fin n) (j j' : ι), K.step s j j' ∈ Matrix.rowStochastic ℝ ι) (s : Fin n) (jj : ι × ι) : ∑ ii : ι × ι, pairStep B K s jj ii = 1

If the columns of the B_s sum to one and the K_{t,j,j'} are Markov kernels, the transition probabilities pairStep from each pair (j, j') sum to one.

theorem CSMC.sum_pathProb_mul {ι : Type u_1} [Fintype ι] {n : ℕ} [DecidableEq ι] {W : ι → ℝ} {B : Fin n → Matrix ι ι ℝ} {K : BackwardKernels ι n} (hB : ∀ (s : Fin n) (j : ι), ∑ i : ι, B s i j = 1) (hK : ∀ (s : Fin n) (j j' : ι), K.step s j j' ∈ Matrix.rowStochastic ℝ ι) (t : Fin (n + 1)) (φ : ι → ι → ℝ) : ∑ b : Fin (n + 1) → ι, ∑ l : Fin (n + 1) → ι, pathProb W B K b l * φ (b t) (l t) = ∑ i : ι, ∑ i' : ι, marg W B K t i i' * φ i i'

If the columns of the B_s sum to one and the K_{t,j,j'} are Markov kernels, the expectation E_𝐱[φ(b_t, l_t)] is ∑_{i, i'} P_𝐱(b_t = i, l_t = i') φ(i, i').

theorem CSMC.sum_pathProb_mul_step {ι : Type u_1} [Fintype ι] {n : ℕ} [DecidableEq ι] {W : ι → ℝ} {B : Fin n → Matrix ι ι ℝ} {K : BackwardKernels ι n} (hB : ∀ (s : Fin n) (j : ι), ∑ i : ι, B s i j = 1) (hK : ∀ (s : Fin n) (j j' : ι), K.step s j j' ∈ Matrix.rowStochastic ℝ ι) (s : Fin n) (φ : ι → ι → ι → ι → ℝ) : ∑ b : Fin (n + 1) → ι, ∑ l : Fin (n + 1) → ι, pathProb W B K b l * φ (b s.castSucc) (b s.succ) (l s.castSucc) (l s.succ) = ∑ j : ι, ∑ j' : ι, marg W B K s.succ j j' * ∑ i : ι, ∑ i' : ι, B s i j * K.step s j j' i i' * φ i j i' j'

If the columns of the B_s sum to one and the K_{t,j,j'} are Markov kernels, the expectation E_𝐱[φ(b_t, b_{t+1}, l_t, l_{t+1})] is ∑_{j, j'} P_𝐱(b_{t+1} = j, l_{t+1} = j') ∑_{i, i'} B_t(i|j) K_{t,j,j'}(i, i') φ(i, j, i', j').