Algorithm S1 with multinomial resampling and potential functions of the current state

By Proposition S3 of the supplementary material, with multinomial resampling and potential functions g_t(x_{t-1}, x_t) = g_t(x_t) of the current state, the reference and the output have the same joint distribution under Algorithm S1 as under Algorithm 1, for any kernels as in Algorithm 1.

The model M' of Section S3 has the densities and the potential functions of the model M of the main text. Its weights and backward-sampling probabilities (S3) are then those of M, so that, given the particle positions, the backward Markov chains pairChain of the two algorithms coincide. With multinomial resampling, the factor of the density (S4) which depends on the particle positions and the ancestor indices is the sum over b_T of the density (6), so that the particle positions have the same distribution under the density (S4) as under π̄.

theorem CSMC.PreviousState.weight_eq_of_pot {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} {M : FeynmanKac μ n} {M' : Model μ n} (h₃ : M'.pot₁ = M.pot 0) (h₄ : ∀ (s : Fin n) (x x' : X), M'.pot s x x' = M.pot s.succ x') (y : Pos X n N) (a : Anc n N) (t : Fin (n + 1)) : M'.weight y a t = M.weight y t

If the potential functions of M' are those of M, the weights of M' are those of M.

theorem CSMC.PreviousState.bsprob_eq_of_pot {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} {M : FeynmanKac μ n} {M' : Model μ n} (h₂ : M'.transdens = M.transdens) (h₃ : M'.pot₁ = M.pot 0) (h₄ : ∀ (s : Fin n) (x x' : X), M'.pot s x x' = M.pot s.succ x') (y : Pos X n N) (a : Anc n N) (s : Fin n) : M'.bsprob y a s = M.bsprob y s

If M' has the transition densities and the potential functions of M, its backward-sampling probabilities (S3) are those of M: the factor g_{t+1}(x_{t+1}^j) cancels.

theorem CSMC.PreviousState.normconst_eq_of_pot {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} {M : FeynmanKac μ n} {M' : Model μ n} (h₁ : M'.transdens₁ = M.transdens₁) (h₂ : M'.transdens = M.transdens) (h₃ : M'.pot₁ = M.pot 0) (h₄ : ∀ (s : Fin n) (x x' : X), M'.pot s x x' = M.pot s.succ x') : M'.normconst = M.normconst

If M' has the densities and the potential functions of M, the two models have the same normalizing constant.

theorem CSMC.PreviousState.sum_extDensity_eq {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} {M : FeynmanKac μ n} {M' : Model μ n} (hN : 0 < N) (h₁ : M'.transdens₁ = M.transdens₁) (h₂ : M'.transdens = M.transdens) (h₃ : M'.pot₁ = M.pot 0) (h₄ : ∀ (s : Fin n) (x x' : X), M'.pot s x x' = M.pot s.succ x') (y : Pos X n N) (a : Anc n N) : ∑ b : Idx n N, M'.extDensity (fun (x : Fin n) => multinomial) gibbs y a b = ∑ bT : Fin N, M.extDensity y a bT

With multinomial resampling, if M' has the densities and the potential functions of M, the sum over the indices of the reference of the density (S4) with the Gibbs kernels is the sum over b_T of the density (6).

theorem CSMC.PreviousState.measurable_multinomial {X : Type u_1} [MeasurableSpace X] {N : ℕ} (a : Fin N → Fin N) : Measurable fun (xw : (Fin N → X) × (Fin N → ℝ)) => multinomial xw.1 xw.2 a

Multinomial resampling is a measurable function of the particles and the weights.

theorem CSMC.PreviousState.map_fst_extMeasure_eq {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} {M : FeynmanKac μ n} {M' : Model μ n} (hN : 0 < N) (h₁ : M'.transdens₁ = M.transdens₁) (h₂ : M'.transdens = M.transdens) (h₃ : M'.pot₁ = M.pot 0) (h₄ : ∀ (s : Fin n) (x x' : X), M'.pot s x x' = M.pot s.succ x') : MeasureTheory.Measure.map Prod.fst (M'.extMeasure (fun (x : Fin n) => multinomial) gibbs) = MeasureTheory.Measure.map Prod.fst (M.exttarget N)

With multinomial resampling, if M' has the densities and the potential functions of M, the particle positions have the same distribution under the density (S4) with the Gibbs kernels as under π̄.

theorem CSMC.PreviousState.target_compProd_csmc_eq {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} {M : FeynmanKac μ n} {M' : Model μ n} [MeasureTheory.SigmaFinite μ] (hN : 0 < N) (h₁ : M'.transdens₁ = M.transdens₁) (h₂ : M'.transdens = M.transdens) (h₃ : M'.pot₁ = M.pot 0) (h₄ : ∀ (s : Fin n) (x x' : X), M'.pot s x x' = M.pot s.succ x') {K : Pos X n N → BackwardKernels (Fin N) n} (hK : ∀ (y : Pos X n N), Admissible (M.weight y (Fin.last n)) (M.bsprob y) (K y)) (hKm : MeasurableKernels K) : M'.target.compProd (M'.csmc (fun (x : Fin n) => multinomial) fun (ya : Pos X n N × Anc n N) => K ya.1) = M.target.compProd (M.csmc K)

Proposition S3: with multinomial resampling, if M' has the densities and the potential functions of M, then, for x_{1:T} ∼ π and measurable kernels as in Algorithm 1, the reference and the output have the same joint distribution under Algorithm S1 as under Algorithm 1.