The density of the extended distribution

The pointwise identities behind Lemmas 3 and 4 of the paper (proof of Lemma 3 in Section S1 of the supplementary material) are proved here.

• With x_{1:T} ∼ π, the indices b of the reference, the particle positions, and the ancestor indices generated by steps (a) and (b) of Algorithm 1 have the density π(x_1^{b_1}, …, x_T^{b_T}) N^{-T} fwdDensity b y a, because x_t = x_t^{b_t}. On the set where a_{t-1}^{b_t} = b_{t-1} for 2 ≤ t ≤ T, which is the set where b is traced back from b_T, this density is the density (6) at (y, a, b_T). It vanishes elsewhere (target_mul_fwdDensity).
• As a function of (a, b_T), the density (6) is a function of the particle positions times W_T^{b_T} ∏_{t,n} B_t(a_t^n|n) (extDensity_eq_mul). These products sum to one (sum_weight_mul_prod_bsprob).

The density (6) is also proved to be measurable.

theorem CSMC.FeynmanKac.unnormalizedTarget_mul_fwdDensity {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) (y : Pos X n N) {a : Anc n N} {b : Idx n N} (hb : ∀ (s : Fin n), a s (b s.succ) = b s.castSucc) : unnormalizedTarget M.transdens₁ M.transdens M.pot (trajOf y b) * M.fwdDensity b y a = (((M.weight y (Fin.last n) (b (Fin.last n))).toNNReal * ∏ t : Fin (n + 1), ∑ i : Fin N, M.pot t (y (t, i))) * ∏ i : Fin N, M.transdens₁ (y (0, i))) * ∏ s : Fin n, ∏ i : Fin N, (M.weight y s.castSucc (a s i)).toNNReal * M.transdens s (y (s.castSucc, a s i)) (y (s.succ, i))

If a_{t-1}^{b_t} = b_{t-1} for 2 ≤ t ≤ T, the numerator of the target density at (x_1^{b_1}, …, x_T^{b_T}) times the density of step (b) of Algorithm 1 is W_T^{b_T} ∏_t {∑_i g_t(x_t^i)} ∏_n m_1(x_1^n) ∏_{t ≥ 2} ∏_n W_{t-1}^{a_{t-1}^n} m_t(x_{t-1}^{a_{t-1}^n}, x_t^n), the numerator of the density (6) at (y, a, b_T).

theorem CSMC.FeynmanKac.target_mul_fwdDensity_eq_extDensity {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) (y : Pos X n N) {a : Anc n N} {b : Idx n N} (hb : ∀ (s : Fin n), a s (b s.succ) = b s.castSucc) : M.normconst⁻¹ * ↑(unnormalizedTarget M.transdens₁ M.transdens M.pot (trajOf y b)) * (↑N)⁻¹ ^ (n + 1) * ↑(M.fwdDensity b y a) = M.extDensity y a (b (Fin.last n))

On the set where a_{t-1}^{b_t} = b_{t-1} for 2 ≤ t ≤ T, the density of x_{1:T} ∼ π followed by steps (a) and (b) of Algorithm 1, π(x_1^{b_1}, …, x_T^{b_T}) N^{-T} fwdDensity b y a, is the density (6) at (y, a, b_T).

theorem CSMC.FeynmanKac.target_mul_fwdDensity {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) (y : Pos X n N) (a : Anc n N) (b : Idx n N) : M.normconst⁻¹ * ↑(unnormalizedTarget M.transdens₁ M.transdens M.pot (trajOf y b)) * (↑N)⁻¹ ^ (n + 1) * ↑(M.fwdDensity b y a) = if b = traceBack a (b (Fin.last n)) then M.extDensity y a (b (Fin.last n)) else 0

The density of x_{1:T} ∼ π followed by steps (a) and (b) of Algorithm 1 at (y, a, b) is the density (6) at (y, a, b_T) if b is traced back from b_T, and zero otherwise.

theorem CSMC.FeynmanKac.extDensity_eq_mul {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) (y : Pos X n N) (a : Anc n N) (bT : Fin N) : M.extDensity y a bT = (((∏ t : Fin (n + 1), ∑ i : Fin N, ↑(M.pot t (y (t, i)))) * ∏ i : Fin N, ↑(M.transdens₁ (y (0, i)))) * ∏ s : Fin n, ∏ j : Fin N, ENNReal.ofReal (∑ k : Fin N, M.weight y s.castSucc k * ↑(M.transdens s (y (s.castSucc, k)) (y (s.succ, j))))) / (M.normconst * ↑N ^ (n + 1)) * ENNReal.ofReal (M.weight y (Fin.last n) bT * ∏ s : Fin n, ∏ i : Fin N, M.bsprob y s (a s i) i)

As a function of (a, b_T), the density (6) is a function of the particle positions times W_T^{b_T} ∏_{t,n} B_t(a_t^n|n): it is the product of ∏_t {∑_i g_t(x_t^i)} ∏_n m_1(x_1^n) ∏_{t ≥ 2} ∏_j ∑_k W_{t-1}^k m_t(x_{t-1}^k, x_t^j) / (Z N^T) and of W_T^{b_T} ∏_{t,n} B_t(a_t^n|n).

theorem CSMC.FeynmanKac.sum_weight_mul_prod_bsprob {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) (hN : 0 < N) (y : Pos X n N) : ∑ a : Anc n N, ∑ bT : Fin N, M.weight y (Fin.last n) bT * ∏ s : Fin n, ∏ i : Fin N, M.bsprob y s (a s i) i = 1

With at least one particle, the products W_T^{b_T} ∏_{t,n} B_t(a_t^n|n) sum to one over the ancestor indices and the final index.

theorem CSMC.FeynmanKac.measurable_extDensity {X : Type u_1} [MeasurableSpace X] {n N : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) : Measurable fun (w : Pos X n N × Anc n N × Fin N) => M.extDensity w.1 w.2.1 w.2.2

The density (6) is a measurable function of the particle positions, the ancestor indices, and the final index.