Backward passes

In steps (c) and (d) of Algorithm 1 of the paper, the indices l_{1:T} of the output are drawn given the indices b_{1:T} of the reference: l_T ∼ K_T(b_T, ·) and l_t ∼ K_{t,b_{t+1},l_{t+1}}(b_t, ·) for t = T - 1, …, 1. For the first five selection rules, Algorithm 1.d is usually implemented as l_t ∼ K_{t,l_{t+1},l_{t+1}}(a_t^{l_{t+1}}, ·), from the ancestor of the particle selected at time t + 1, without the indices of the reference at the times t < T (Section 2.1).

The kernels are functions of variables ξ : Ξ: the particle positions in Algorithm 1, and the particle positions and the ancestor indices in Section S3. Both backward passes are defined here as kernels with the product of these probabilities as mass function. The measurability of the kernels in ξ, which is left implicit in the paper, is the condition MeasurableKernels.

Both mass functions are the probabilities of the trajectories of backward Markov chains, which sum to one, so that both backward passes are Markov kernels for measurable Markov kernels K_T and K_{t,j,j'}.

def CSMC.MeasurableKernels {Ξ : Type u_1} [MeasurableSpace Ξ] {n : ℕ} {ι : Type u_2} (K : Ξ → BackwardKernels ι n) : Prop

The kernels K_T and K_{t,j,j'} are measurable functions of ξ.

Equations

• CSMC.MeasurableKernels K = ((∀ (i j : ι), Measurable fun (ξ : Ξ) => (K ξ).final i j) ∧ ∀ (s : Fin n) (j j' i i' : ι), Measurable fun (ξ : Ξ) => (K ξ).step s j j' i i')

noncomputable def CSMC.backwardPass {Ξ : Type u_1} [MeasurableSpace Ξ] {n N : ℕ} (K : Ξ → BackwardKernels (Fin N) n) : ProbabilityTheory.Kernel (Ξ × Idx n N) (Idx n N)

Steps (c) and (d) of Algorithm 1: given ξ and the indices b of the reference, the indices l of the output have the probability K_T(b_T, l_T) ∏_t K_{t,b_{t+1},l_{t+1}}(b_t, l_t).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CSMC.backwardPassAnc {Ξ : Type u_1} [MeasurableSpace Ξ] {n N : ℕ} (K : Ξ → BackwardKernels (Fin N) n) (anc : Ξ → Anc n N) : ProbabilityTheory.Kernel (Ξ × Fin N) (Idx n N)

The usual implementation of steps (c) and (d) of Algorithm 1 (Section 2.1): given ξ, with ancestor indices anc ξ, and the final index b_T of the reference, the indices l of the output have the probability K_T(b_T, l_T) ∏_t K_{t,l_{t+1},l_{t+1}}(a_t^{l_{t+1}}, l_t).

Equations

• One or more equations did not get rendered due to their size.

instance CSMC.instIsSFiniteKernelProdIdxBackwardPass {Ξ : Type u_1} [MeasurableSpace Ξ] {n N : ℕ} (K : Ξ → BackwardKernels (Fin N) n) : ProbabilityTheory.IsSFiniteKernel (backwardPass K)

instance CSMC.instIsSFiniteKernelProdFinIdxBackwardPassAnc {Ξ : Type u_1} [MeasurableSpace Ξ] {n N : ℕ} (K : Ξ → BackwardKernels (Fin N) n) (anc : Ξ → Anc n N) : ProbabilityTheory.IsSFiniteKernel (backwardPassAnc K anc)

theorem CSMC.measurable_step_anc {Ξ : Type u_1} [MeasurableSpace Ξ] {n N : ℕ} {K : Ξ → BackwardKernels (Fin N) n} {anc : Ξ → Anc n N} (hKm : MeasurableKernels K) (hanc : Measurable anc) (s : Fin n) (j i : Fin N) : Measurable fun (ξ : Ξ) => (K ξ).step s j j (anc ξ s j) i

In the usual implementation, the probability K_{t,j,j}(a_t^j, i) of l_t = i given l_{t+1} = j is measurable in ξ, through a_t^j.

theorem CSMC.lintegral_backwardPass {Ξ : Type u_1} [MeasurableSpace Ξ] {n N : ℕ} {K : Ξ → BackwardKernels (Fin N) n} (hKm : MeasurableKernels K) (ξb : Ξ × Idx n N) (g : Idx n N → ENNReal) : ∫⁻ (l : Idx n N), g l ∂(backwardPass K) ξb = ∑ l : Idx n N, ENNReal.ofReal ((K ξb.1).final (ξb.2 (Fin.last n)) (l (Fin.last n)) * ∏ s : Fin n, (K ξb.1).step s (ξb.2 s.succ) (l s.succ) (ξb.2 s.castSucc) (l s.castSucc)) * g l

Integrals with respect to the backward pass are sums over the indices of the output, weighted by K_T(b_T, l_T) ∏_t K_{t,b_{t+1},l_{t+1}}(b_t, l_t).

theorem CSMC.lintegral_backwardPassAnc {Ξ : Type u_1} [MeasurableSpace Ξ] {n N : ℕ} {K : Ξ → BackwardKernels (Fin N) n} {anc : Ξ → Anc n N} (hKm : MeasurableKernels K) (hanc : Measurable anc) (ξb : Ξ × Fin N) (g : Idx n N → ENNReal) : ∫⁻ (l : Idx n N), g l ∂(backwardPassAnc K anc) ξb = ∑ l : Idx n N, ENNReal.ofReal ((K ξb.1).final ξb.2 (l (Fin.last n)) * ∏ s : Fin n, (K ξb.1).step s (l s.succ) (l s.succ) (anc ξb.1 s (l s.succ)) (l s.castSucc)) * g l

Integrals with respect to the backward pass of the usual implementation are sums over the indices of the output, weighted by K_T(b_T, l_T) ∏_t K_{t,l_{t+1},l_{t+1}}(a_t^{l_{t+1}}, l_t).

theorem CSMC.sum_chainProb_eq_one {n : ℕ} {S : Type u_2} [Fintype S] {μ : S → ℝ} (hμ : ∑ y : S, μ y = 1) {P : Fin n → S → S → ℝ} (hP : ∀ (s : Fin n) (y : S), ∑ z : S, P s y z = 1) : ∑ x : Fin (n + 1) → S, chainProb μ P x = 1

If the initial distribution and the transition probabilities sum to one, so do the probabilities of the trajectories of a backward Markov chain.

theorem CSMC.isMarkovKernel_kernelOfMassFn_chainProb {n : ℕ} {α : Type u_2} {S : Type u_3} [MeasurableSpace α] [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S] {μ : α → S → ℝ} {P : α → Fin n → S → S → ℝ} (hμ : ∀ (a : α), IsProbVector (μ a)) (hP : ∀ (a : α) (s : Fin n) (y : S), IsProbVector (P a s y)) (hμm : ∀ (y : S), Measurable fun (a : α) => μ a y) (hPm : ∀ (s : Fin n) (y z : S), Measurable fun (a : α) => P a s y z) : ProbabilityTheory.IsMarkovKernel (kernelOfMassFn fun (a : α) (x : Fin (n + 1) → S) => (chainProb (μ a) (P a) x).toNNReal)

The kernel whose mass function is the probability of the trajectory of a backward Markov chain, with measurable initial distributions and transition probabilities which are probability vectors, is a Markov kernel.

theorem CSMC.isMarkovKernel_backwardPass {Ξ : Type u_1} [MeasurableSpace Ξ] {n N : ℕ} {K : Ξ → BackwardKernels (Fin N) n} (hK : ∀ (ξ : Ξ), (K ξ).final ∈ Matrix.rowStochastic ℝ (Fin N) ∧ ∀ (s : Fin n) (j j' : Fin N), (K ξ).step s j j' ∈ Matrix.rowStochastic ℝ (Fin N)) (hKm : MeasurableKernels K) : ProbabilityTheory.IsMarkovKernel (backwardPass K)

For measurable Markov kernels, the backward pass is a Markov kernel.

theorem CSMC.isMarkovKernel_backwardPassAnc {Ξ : Type u_1} [MeasurableSpace Ξ] {n N : ℕ} {K : Ξ → BackwardKernels (Fin N) n} {anc : Ξ → Anc n N} (hK : ∀ (ξ : Ξ), (K ξ).final ∈ Matrix.rowStochastic ℝ (Fin N) ∧ ∀ (s : Fin n) (j j' : Fin N), (K ξ).step s j j' ∈ Matrix.rowStochastic ℝ (Fin N)) (hKm : MeasurableKernels K) (hanc : Measurable anc) : ProbabilityTheory.IsMarkovKernel (backwardPassAnc K anc)

For measurable Markov kernels and measurable ancestor indices, the backward pass of the usual implementation is a Markov kernel.