Sums over the ancestor indices along a genealogy

Let the ancestor indices a_t^i be independent, with the distributions B_t(·|i), as they are under the extended distribution conditionally on the particle positions (Lemma 3). The indices b traced back from b_T depend on one ancestor index at each time, b_t = a_t^{b_{t+1}}, so that, given b_T, they form a backward Markov chain with the transition probabilities B_t(b_t|b_{t+1}). This property is proved here for sums over the ancestor indices of a product of weights (sum_prod_traceBack), in a form which also covers a summand which depends, at each time, on the ancestor index a_t^{l_{t+1}} of the usual implementation of the backward pass. The finite identities behind both parts of Lemma 4 of the paper follow (sum_traceBack_backwardPass and sum_traceBack_backwardPassAnc).

theorem CSMC.traceBack_cons {n N : ℕ} (a₀ : Fin N → Fin N) (a : Anc n N) (bT : Fin N) : traceBack (Fin.cons a₀ a) bT = Fin.cons (a₀ (traceBack a bT 0)) (traceBack a bT)

The indices traced back through the ancestor indices Fin.cons a₀ a are those traced back through a, preceded by the ancestor through a₀ of the first of them.

theorem CSMC.sum_prod_mul_apply {N : ℕ} {R : Type u_1} [CommSemiring R] {P : Fin N → Fin N → R} (hP : ∀ (i : Fin N), ∑ k : Fin N, P k i = 1) (j : Fin N) (H : Fin N → R) : ∑ v : Fin N → Fin N, (∏ i : Fin N, P (v i) i) * H (v j) = ∑ k : Fin N, P k j * H k

Under the product of the weights P(·, i), which sum to one, the coordinate v j has the weights P(·, j).

theorem CSMC.sum_prod_mul_apply_mul_apply {N : ℕ} {R : Type u_1} [CommSemiring R] {P : Fin N → Fin N → R} (hP : ∀ (i : Fin N), ∑ k : Fin N, P k i = 1) {j j' : Fin N} (hj : j ≠ j') (H A : Fin N → R) : ∑ v : Fin N → Fin N, (∏ i : Fin N, P (v i) i) * H (v j) * A (v j') = (∑ k : Fin N, P k j * H k) * ∑ k : Fin N, P k j' * A k

Under the product of the weights P(·, i), which sum to one, the coordinates v j and v j', for j ≠ j', are independent, with the weights P(·, j) and P(·, j').

theorem CSMC.sum_prod_traceBack {n N : ℕ} {R : Type u_1} [CommSemiring R] (G : Fin n → (Fin N → Fin N) → R) (Q : Fin n → Fin N → Fin N → R) (hG : ∀ (s : Fin n) (j : Fin N) (H : Fin N → R), ∑ v : Fin N → Fin N, G s v * H (v j) = ∑ k : Fin N, Q s k j * H k) (bT : Fin N) (h : Idx n N → R) : ∑ a : Anc n N, (∏ s : Fin n, G s (a s)) * h (traceBack a bT) = ∑ b : Idx n N, if b (Fin.last n) = bT then (∏ s : Fin n, Q s (b s.castSucc) (b s.succ)) * h b else 0

Let the ancestor indices a s at each time be weighted by G s, under which, for every j, the index a s j has the weights Q s (·) j. The sum over the ancestor indices of the product of the weights times a function h of the indices traced back from b_T is the sum, over the sequences b with final index b_T, of ∏_s Q s (b s.castSucc) (b s.succ) times h b.

theorem CSMC.ofReal_mul_prod {ι : Type u_2} [Fintype ι] {x : ℝ} (hx : 0 ≤ x) {f : ι → ℝ} (hf : ∀ (i : ι), 0 ≤ f i) : ENNReal.ofReal (x * ∏ i : ι, f i) = ENNReal.ofReal x * ∏ i : ι, ENNReal.ofReal (f i)

For nonnegative factors, ENNReal.ofReal (x ∏_i f i) is the product of ENNReal.ofReal x and of the ENNReal.ofReal (f i).

theorem CSMC.sum_ofReal_of_isProbVector {N : ℕ} {p : Fin N → ℝ} (hp : IsProbVector p) : ∑ k : Fin N, ENNReal.ofReal (p k) = 1

The entries of a probability vector, as extended nonnegative real numbers, sum to one.

theorem CSMC.sum_traceBack {n N : ℕ} {W : Fin N → ℝ} {B : Fin n → Matrix (Fin N) (Fin N) ℝ} (hB : ∀ (s : Fin n) (j : Fin N), IsProbVector fun (i : Fin N) => B s i j) (hW : ∀ (i : Fin N), 0 ≤ W i) (F : Idx n N → ENNReal) : ∑ a : Anc n N, ∑ bT : Fin N, ENNReal.ofReal (W bT * ∏ s : Fin n, ∏ i : Fin N, B s (a s i) i) * F (traceBack a bT) = ∑ b : Idx n N, ENNReal.ofReal (W (b (Fin.last n)) * ∏ s : Fin n, B s (b s.castSucc) (b s.succ)) * F b

Let the final index b_T have the weights W and the ancestor indices a_t^i the weights B_t(·|i), independently. Then the indices traced back from b_T have the probabilities W(b_T) ∏_t B_t(b_t|b_{t+1}).

theorem CSMC.sum_traceBack_backwardPass {n N : ℕ} {W : Fin N → ℝ} {B : Fin n → Matrix (Fin N) (Fin N) ℝ} {K : BackwardKernels (Fin N) n} (hB : ∀ (s : Fin n) (j : Fin N), IsProbVector fun (i : Fin N) => B s i j) (hW : ∀ (i : Fin N), 0 ≤ W i) (hK : Admissible W B K) (g : Idx n N → Idx n N → ENNReal) : ∑ a : Anc n N, ∑ bT : Fin N, ENNReal.ofReal (W bT * ∏ s : Fin n, ∏ i : Fin N, B s (a s i) i) * ∑ l : Idx n N, ENNReal.ofReal (K.final (traceBack a bT (Fin.last n)) (l (Fin.last n)) * ∏ s : Fin n, K.step s (traceBack a bT s.succ) (l s.succ) (traceBack a bT s.castSucc) (l s.castSucc)) * g (traceBack a bT) l = ∑ b : Fin (n + 1) → Fin N, ∑ l : Fin (n + 1) → Fin N, ENNReal.ofReal (pathProb W B K b l) * g b l

The finite identity behind the first two sentences of Lemma 4: if the final index b_T has the weights W and the ancestor indices a_t^i the weights B_t(·|i), independently, and the indices l of the output are drawn as in steps (c) and (d) of Algorithm 1 from the indices b traced back from b_T, then (b, l) has the probabilities pathProb W B K.

theorem CSMC.sum_traceBack_backwardPassAnc {n N : ℕ} {W : Fin N → ℝ} {B : Fin n → Matrix (Fin N) (Fin N) ℝ} {K : BackwardKernels (Fin N) n} (hB : ∀ (s : Fin n) (j : Fin N), IsProbVector fun (i : Fin N) => B s i j) (hW : ∀ (i : Fin N), 0 ≤ W i) (hK : Admissible W B K) (hoff : ∀ (s : Fin n) (j j' i i' : Fin N), j ≠ j' → K.step s j j' i i' = B s i' j') (g : Idx n N → Idx n N → ENNReal) : ∑ a : Anc n N, ∑ bT : Fin N, ENNReal.ofReal (W bT * ∏ s : Fin n, ∏ i : Fin N, B s (a s i) i) * ∑ l : Idx n N, ENNReal.ofReal (K.final bT (l (Fin.last n)) * ∏ s : Fin n, K.step s (l s.succ) (l s.succ) (a s (l s.succ)) (l s.castSucc)) * g (traceBack a bT) l = ∑ b : Fin (n + 1) → Fin N, ∑ l : Fin (n + 1) → Fin N, ENNReal.ofReal (pathProb W B K b l) * g b l

The finite identity behind the last sentence of Lemma 4: if, moreover, K_{t,j,j'}(i, ·) = B_t(·|j') for j ≠ j', the same holds when Algorithm 1.d is implemented as l_t ∼ K_{t,l_{t+1},l_{t+1}}(a_t^{l_{t+1}}, ·).