Resampling schemes

By Definition S1 of the supplementary material, a resampling scheme at time t is a distribution r_t on [N]^N, which may depend on the particles at time t and on their weights, such that, for every i, the expected number of indices n with a_t^n = i under r_t is N W_t^i. The vector a_t = (a_t^1, …, a_t^N) of the indices of the ancestors at time t of the particles at time t + 1 is drawn from a resampling scheme r_t.

The condition of Definition S1 is stated here for a function r of the particles xs, the weights w, and the ancestor indices a. Multinomial resampling, r(a) = ∏_n w_{a^n}, satisfies it. In the statements, the condition is a hypothesis on r. That stratified, systematic, residual, and killing resampling satisfy it (Finke et al., 2026, Section 3) is not proved here.

Under the condition, the probabilities r(a) sum to one. Their sum over the pairs (b, a) with a^b = c is N w_c, the normalizing constant of the probabilities in Algorithm S1.b.

structure CSMC.PreviousState.IsUnbiasedResampling {X : Type u_1} {N : ℕ} (r : (Fin N → X) → (Fin N → ℝ) → (Fin N → Fin N) → ℝ) : Prop

The condition of Definition S1 on a resampling scheme r: for the particles xs and every probability vector of weights w, r xs w is a nonnegative function on [N]^N under which the expected number of indices k with a k = i is N w_i, for every i. Summing over i shows that r xs w sums to one.

• nonneg (xs : Fin N → X) (w : Fin N → ℝ) (a : Fin N → Fin N) : IsProbVector w → 0 ≤ r xs w a

  The probabilities are nonnegative.

• expected_count (xs : Fin N → X) (w : Fin N → ℝ) : IsProbVector w → ∀ (i : Fin N), ∑ a : Fin N → Fin N, r xs w a * ↑{k : Fin N | a k = i}.card = ↑N * w i

  The expected number of indices k with a k = i is N w_i.

def CSMC.PreviousState.multinomial {X : Type u_1} {N : ℕ} (_xs : Fin N → X) (w : Fin N → ℝ) (a : Fin N → Fin N) : ℝ

Multinomial resampling: r(a) = ∏_k w_{a^k}, which does not depend on the particles.

Equations

• CSMC.PreviousState.multinomial _xs w a = ∏ k : Fin N, w (a k)

theorem CSMC.PreviousState.IsUnbiasedResampling.sum_eq_one {X : Type u_1} {N : ℕ} {r : (Fin N → X) → (Fin N → ℝ) → (Fin N → Fin N) → ℝ} (hr : IsUnbiasedResampling r) (hN : 0 < N) (xs : Fin N → X) {w : Fin N → ℝ} (hw : IsProbVector w) : ∑ a : Fin N → Fin N, r xs w a = 1

Under the condition of Definition S1, the probabilities of a resampling scheme sum to one.

theorem CSMC.PreviousState.IsUnbiasedResampling.sum_sum_ite_eq {X : Type u_1} {N : ℕ} {r : (Fin N → X) → (Fin N → ℝ) → (Fin N → Fin N) → ℝ} (hr : IsUnbiasedResampling r) (xs : Fin N → X) {w : Fin N → ℝ} (hw : IsProbVector w) (c : Fin N) : (∑ b : Fin N, ∑ a : Fin N → Fin N, if a b = c then r xs w a else 0) = ↑N * w c

Under the condition of Definition S1, the sum of the probabilities r(a) over the pairs (b, a) with a^b = c is N w_c.

theorem CSMC.PreviousState.isUnbiasedResampling_multinomial {X : Type u_1} {N : ℕ} : IsUnbiasedResampling multinomial

Multinomial resampling satisfies the condition of Definition S1.