Conditional sequential Monte Carlo with a general backward pass

Algorithm 1 of the paper, given the reference trajectory x_{1:T} and kernels K_T and K_{t,j,j'} which are functions of the particle positions, consists of the following steps.

(a) Draw b_1, …, b_T independent uniforms on [N]. (b) Draw the particle positions and the ancestor indices in the forward pass. (c), (d) Draw the indices l_{1:T} of the output in the backward pass. (e) Return (x_1^{l_1}, …, x_T^{l_T}).

The objects defined here are the joint distribution algLaw of the variables (b, (y, a), l) of the algorithm given the reference trajectory, the same joint distribution with the usual implementation of the backward pass (algLawUsual), the Markov kernel csmc of the algorithm, and the backward Markov chain pairChain of the indices of the reference and of the output given the particle positions (Lemma 4).

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

The joint distribution, given the reference trajectory, of the indices b of the reference, the particle positions and ancestor indices (y, a), and the indices l of the output generated by Algorithm 1 with the kernels K.

Equations

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

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

The joint distribution of the same variables when Algorithm 1.d is implemented as l_t ∼ K_{t,l_{t+1},l_{t+1}}(a_t^{l_{t+1}}, ·) (the usual implementation of Section 2.1).

Equations

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

noncomputable def CSMC.FeynmanKac.csmc {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) (K : Pos X n N → BackwardKernels (Fin N) n) : ProbabilityTheory.Kernel (Traj X n) (Traj X n)

The Markov kernel defined by Algorithm 1 with the kernels K: the distribution of the output (x_1^{l_1}, …, x_T^{l_T}) given the reference trajectory.

Equations

• M.csmc K = (M.algLaw K).map fun (z : (CSMC.Idx n N × CSMC.Pos X n N × CSMC.Anc n N) × CSMC.Idx n N) => CSMC.trajOf z.1.2.1 z.2

noncomputable def CSMC.FeynmanKac.pairChain {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) (K : Pos X n N → BackwardKernels (Fin N) n) : ProbabilityTheory.Kernel (Pos X n N) (Idx n N × Idx n N)

The backward Markov chain of the indices of the reference and of the output given the particle positions (Lemma 4): the kernel from the particle positions to the pairs (b, l) with mass function pathProb W_T B K b l.

Equations

• M.pairChain K = CSMC.kernelOfMassFn fun (y : CSMC.Pos X n N) (bl : CSMC.Idx n N × CSMC.Idx n N) => (CSMC.pathProb (M.weight y (Fin.last n)) (M.bsprob y) (K y) bl.1 bl.2).toNNReal