The forward pass of Algorithm 1

In step (b) of Algorithm 1 of the paper, the particle positions and the ancestor indices are drawn given the reference trajectory x_{1:T} and its indices b_{1:T}. First, x_1^{b_1} = x_1 and x_1^i ∼ m_1 for i ≠ b_1. Then, for t = 2, …, T, a_{t-1}^{b_t} = b_{t-1}, x_t^{b_t} = x_t, and, for i ≠ b_t, a_{t-1}^i ∼ W_{t-1} and x_t^i ∼ m_t(x_{t-1}^{a_{t-1}^i}, ·).

This step is defined here as a kernel from the reference trajectory and its indices to the particle positions and the ancestor indices. For fixed indices b, this kernel has a density with respect to the product of refKernel μ b, with x_t at the coordinates (t, b_t) and μ at the other coordinates, and of the counting measure on the ancestor indices.

With at least one particle, the forward pass is a Markov kernel: summed over the ancestor indices, its density is the product over the coordinates (t, i), i ≠ b_t, of m_1(x_1^i) at the first time and of ∑_k W_{t-1}^k m_t(x_{t-1}^k, x_t^i) afterwards. This product integrates to one by sequential normalization, backwards in time.

theorem CSMC.sum_ite_mul_prod_filter_ne {N : ℕ} {R : Type u_2} [CommSemiring R] (j k₀ : Fin N) (G : Fin N → Fin N → R) : ∑ c : Fin N → Fin N, (if c j = k₀ then 1 else 0) * ∏ i : Fin N with i ≠ j, G i (c i) = ∏ i : Fin N with i ≠ j, ∑ k : Fin N, G i k

Summing over the ancestor indices a_t with a_t^{b_{t+1}} = b_t and the other indices free: ∑_{a_t} 1{a_t^{b_{t+1}} = b_t} ∏_{i ≠ b_{t+1}} G(i, a_t^i) = ∏_{i ≠ b_{t+1}} ∑_k G(i, k).

noncomputable def CSMC.FeynmanKac.fwdDensity {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) (b : Idx n N) (y : Pos X n N) (a : Anc n N) : NNReal

The density of step (b) of Algorithm 1 at the particle positions y and the ancestor indices a, given the indices b of the reference: ∏_{i ≠ b_1} m_1(x_1^i) ∏_{t ≥ 2} 1{a_{t-1}^{b_t} = b_{t-1}} ∏_{i ≠ b_t} W_{t-1}^{a_{t-1}^i} m_t(x_{t-1}^{a_{t-1}^i}, x_t^i).

Equations

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

noncomputable def CSMC.FeynmanKac.forwardPass {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) (N : ℕ) : ProbabilityTheory.Kernel (Traj X n × Idx n N) (Pos X n N × Anc n N)

Step (b) of Algorithm 1, as a kernel from the reference trajectory and its indices to the particle positions and the ancestor indices.

Equations

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

theorem CSMC.FeynmanKac.isMarkovKernel_forwardPass {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) [MeasureTheory.SigmaFinite μ] (hN : 0 < N) : ProbabilityTheory.IsMarkovKernel (M.forwardPass N)

With at least one particle, the forward pass is a Markov kernel.