The validity of Algorithm S2

In Algorithm S2 of the supplementary material, steps (a) and (b) of Algorithm S1 are run with c = b_t, that is, with the identity kernels. They are followed by a backward pass from the ancestors: l_T ∼ K_T(b_T, ·) and, for t = T - 1, …, 1, l_t ∼ K_{t,l_{t+1},l_{t+1}}(a_t^{l_{t+1}}, ·). Proposition S4 is proved here: the Markov kernel defined by Algorithm S2 leaves π invariant. With the kernels of AT and FM-AT, it is reversible with respect to π.

By Lemma S1 with the identity kernels, (𝐱, a, b_{1:T}) has the density (S4), in which the indices of the reference are those traced back from b_T. Conditionally on (𝐱, a), b_T ∼ W_T. Because K_T leaves W_T invariant, (𝐱, a, l_{1:T}) then has the density (S4) with l_{1:T} in place of b_{1:T} and with the kernels K_{t,j,j} of the selection rule, so that x̃_{1:T} ∼ π by the converse of Lemma S1. With the identity kernels of AT and FM-AT, b_{1:T} and l_{1:T} are traced back from b_T and l_T, respectively, whose probability W_T^{b_T} K_T(b_T, l_T) given (𝐱, a) does not change when the two are exchanged.

theorem CSMC.PreviousState.sum_prod_one_mul {n N : ℕ} (a : Anc n N) (F : Idx n N → ENNReal) : ∑ b : Idx n N, (∏ s : Fin n, ENNReal.ofReal (1 (a s (b s.succ)) (b s.castSucc))) * F b = ∑ bT : Fin N, F (traceBack a bT)

The product ∏_t 1{a_t^{b_{t+1}} = b_t} of the entries of the identity kernels is one if b is the sequence of indices traced back from b_T, and zero otherwise.

theorem CSMC.PreviousState.Model.lintegral_target_compProd_algLawAnc {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) [MeasureTheory.SigmaFinite μ] {resdist : Fin n → (Fin N → X) → (Fin N → ℝ) → (Fin N → Fin N) → ℝ} (hr : ∀ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : ∀ (s : Fin n) (a : Fin N → Fin N), Measurable fun (xw : (Fin N → X) × (Fin N → ℝ)) => resdist s xw.1 xw.2 a) (r : SelectionRule) {g : Traj X n × (Pos X n N × Anc n N × Idx n N) × Idx n N → ENNReal} (hg : Measurable g) : ∫⁻ (z : Traj X n × (Pos X n N × Anc n N × Idx n N) × Idx n N), g z ∂M.target.compProd (M.algLawAnc resdist r) = ∫⁻ (y : Fin (n + 1) × Fin N → X), ∑ a : Anc n N, M.posAncDensity resdist y a * ∑ bT : Fin N, ENNReal.ofReal (M.weight y a (Fin.last n) bT) * ∑ l : Idx n N, ENNReal.ofReal ((M.ruleKernels N r (y, a)).final bT (l (Fin.last n)) * ∏ s : Fin n, (M.ruleKernels N r (y, a)).step s (l s.succ) (l s.succ) (a s (l s.succ)) (l s.castSucc)) * g (trajOf y (traceBack a bT), (y, a, traceBack a bT), l) ∂MeasureTheory.Measure.pi fun (x : Fin (n + 1) × Fin N) => μ

Integrals with respect to the joint distribution of x_{1:T} ∼ π and of the variables of Algorithm S2 are integrals over the particle positions of sums over the ancestor indices of the factor of the density (S4) which depends on them, times the sum over the final index b_T of the reference of W_T^{b_T} times the integral with respect to the backward pass from the ancestors, at the indices of the reference traced back from b_T.

instance CSMC.PreviousState.Model.instIsSFiniteKernelTrajProdPosAncIdxAlgLawAnc {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) (resdist : Fin n → (Fin N → X) → (Fin N → ℝ) → (Fin N → Fin N) → ℝ) (r : SelectionRule) : ProbabilityTheory.IsSFiniteKernel (M.algLawAnc resdist r)

The joint distribution of the variables of Algorithm S2 is an s-finite kernel.

instance CSMC.PreviousState.Model.instIsSFiniteKernelTrajCsmcAnc {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) (resdist : Fin n → (Fin N → X) → (Fin N → ℝ) → (Fin N → Fin N) → ℝ) (r : SelectionRule) : ProbabilityTheory.IsSFiniteKernel (M.csmcAnc resdist r)

The kernel of Algorithm S2 is an s-finite kernel.

theorem CSMC.PreviousState.Model.map_target_compProd_algLawAnc {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) [MeasureTheory.SigmaFinite μ] (hN : 0 < N) {resdist : Fin n → (Fin N → X) → (Fin N → ℝ) → (Fin N → Fin N) → ℝ} (hr : ∀ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : ∀ (s : Fin n) (a : Fin N → Fin N), Measurable fun (xw : (Fin N → X) × (Fin N → ℝ)) => resdist s xw.1 xw.2 a) (r : SelectionRule) : MeasureTheory.Measure.map (fun (z : Traj X n × (Pos X n N × Anc n N × Idx n N) × Idx n N) => (z.2.1.1, z.2.1.2.1, z.2.2)) (M.target.compProd (M.algLawAnc resdist r)) = M.extMeasure resdist r.diagKernel

With at least one particle, the particle positions, the ancestor indices, and the indices of the output of Algorithm S2 started from x_{1:T} ∼ π have the density (S4), with the indices of the output in place of those of the reference and with the kernels K_{t,j,j} of the selection rule.

theorem CSMC.PreviousState.Model.measurable_trajOf_output {X : Type u_1} [MeasurableSpace X] {n N : ℕ} : Measurable fun (z : (Pos X n N × Anc n N × Idx n N) × Idx n N) => trajOf z.1.1 z.2

The trajectory (x_1^{l_1}, …, x_T^{l_T}) read off the particles with the indices of the output is a measurable function of the variables of Algorithm S2.

theorem CSMC.PreviousState.Model.invariant_csmcAnc {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) [MeasureTheory.SigmaFinite μ] (hN : 0 < N) {resdist : Fin n → (Fin N → X) → (Fin N → ℝ) → (Fin N → Fin N) → ℝ} (hr : ∀ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : ∀ (s : Fin n) (a : Fin N → Fin N), Measurable fun (xw : (Fin N → X) × (Fin N → ℝ)) => resdist s xw.1 xw.2 a) (r : SelectionRule) : (M.csmcAnc resdist r).Invariant M.target

Proposition S4, first part: with at least one particle, the Markov kernel defined by Algorithm S2 leaves π invariant.

theorem CSMC.PreviousState.Model.lintegral_target_compProd_csmcAnc_of_one {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) [MeasureTheory.SigmaFinite μ] (hN : 0 < N) {resdist : Fin n → (Fin N → X) → (Fin N → ℝ) → (Fin N → Fin N) → ℝ} (hr : ∀ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : ∀ (s : Fin n) (a : Fin N → Fin N), Measurable fun (xw : (Fin N → X) × (Fin N → ℝ)) => resdist s xw.1 xw.2 a) {r : SelectionRule} (hr1 : ∀ (p : Fin N → ℝ), r.diagKernel p = 1) {g : Traj X n × Traj X n → ENNReal} (hg : Measurable g) : ∫⁻ (z : Traj X n × Traj X n), g z ∂M.target.compProd (M.csmcAnc resdist r) = ∫⁻ (y : Fin (n + 1) × Fin N → X), ∑ a : Anc n N, M.posAncDensity resdist y a * ∑ bT : Fin N, ∑ lT : Fin N, ENNReal.ofReal (M.weight y a (Fin.last n) bT) * ENNReal.ofReal ((M.ruleKernels N r (y, a)).final bT lT) * g (trajOf y (traceBack a bT), trajOf y (traceBack a lT)) ∂MeasureTheory.Measure.pi fun (x : Fin (n + 1) × Fin N) => μ

With the identity kernels K_{t,j,j} of AT and FM-AT, integrals with respect to the joint distribution of x_{1:T} ∼ π and of the output of Algorithm S2 are integrals over the particle positions of sums over the ancestor indices of the factor of the density (S4) which depends on them, times the sum over b_T and l_T of W_T^{b_T} K_T(b_T, l_T) times the integrand at the trajectories traced back from b_T and l_T.

theorem CSMC.PreviousState.Model.isReversible_csmcAnc {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) [MeasureTheory.SigmaFinite μ] (hN : 0 < N) {resdist : Fin n → (Fin N → X) → (Fin N → ℝ) → (Fin N → Fin N) → ℝ} (hr : ∀ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : ∀ (s : Fin n) (a : Fin N → Fin N), Measurable fun (xw : (Fin N → X) × (Fin N → ℝ)) => resdist s xw.1 xw.2 a) {r : SelectionRule} (hr' : r = SelectionRule.AT ∨ r = SelectionRule.FMAT) : (M.csmcAnc resdist r).IsReversible M.target

Proposition S4, second part: with at least one particle and the kernels of AT and FM-AT, the Markov kernel defined by Algorithm S2 is reversible with respect to π.