The extended distribution

The proofs of Section 3 of the paper rely on the extended distribution of Andrieu et al. (2010) on the particle positions, the ancestor indices, and a final index b_T, with density (eq. (6)) π̄(x, a, b_T) = W_T^{b_T} / (Z N^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) with respect to the product of μ on each particle position and of the counting measures on the indices. The density and the distribution are defined here. That the distribution is a probability measure is proved in Algorithm/Validity, by Lemma 3.

noncomputable def CSMC.FeynmanKac.extDensity {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) : ENNReal

The density (6) of the extended distribution of the particle positions y, the ancestor indices a, and the final index b_T.

Equations

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

noncomputable def CSMC.FeynmanKac.exttarget {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) (N : ℕ) : MeasureTheory.Measure (Pos X n N × Anc n N × Fin N)

The extended distribution π̄ of eq. (6) on the particle positions, the ancestor indices, and the final index b_T.

Equations

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