Trajectories, particle positions, and indices

With T = n + 1 time steps and N particles, the variables of the algorithms of the paper have the following types:

• trajectories x_{1:T}, Traj X n = Fin (n + 1) → X;
• particle positions x_t^i, Pos X n N = Fin (n + 1) × Fin N → X, with y (t, i) the position of the particle i at time t;
• ancestor indices a_t^i, Anc n N = Fin n → Fin N → Fin N, with a s i the index at time s.castSucc of the ancestor of the particle i at time s.succ;
• sequences of particle indices b_{1:T} and l_{1:T}, Idx n N = Fin (n + 1) → Fin N.

The other definitions are the trajectory (x_1^{l_1}, …, x_T^{l_T}) of the particles with indices l, the indices traced back through the ancestors (Section 3), the uniform distribution of the indices of the reference (Algorithm 1.a), and the measure on the particle positions with the reference trajectory at the coordinates (t, b_t) and μ at the other coordinates.

A sequence of indices b is the one traced back from b_T if and only if b_t = a_t^{b_{t+1}} for every t < T (eq_traceBack_iff).

@[reducible, inline]

abbrev CSMC.Traj (X : Type u_1) (n : ℕ) : Type u_1

Trajectories x_{1:T} in X, with T = n + 1.

Equations

• CSMC.Traj X n = (Fin (n + 1) → X)

@[reducible, inline]

abbrev CSMC.Pos (X : Type u_1) (n N : ℕ) : Type u_1

Particle positions: y (t, i) is the position x_t^i of the particle i at time t.

Equations

• CSMC.Pos X n N = (Fin (n + 1) × Fin N → X)

@[reducible, inline]

abbrev CSMC.Anc (n N : ℕ) : Type

Ancestor indices: a s i is the index a_t^i at time s.castSucc of the ancestor of the particle i at time s.succ.

Equations

• CSMC.Anc n N = (Fin n → Fin N → Fin N)

@[reducible, inline]

abbrev CSMC.Idx (n N : ℕ) : Type

Sequences of particle indices, such as the indices b_{1:T} of the reference and l_{1:T} of the output.

Equations

• CSMC.Idx n N = (Fin (n + 1) → Fin N)

def CSMC.trajOf {X : Type u_1} {n N : ℕ} (y : Pos X n N) (l : Idx n N) : Traj X n

The trajectory (x_1^{l_1}, …, x_T^{l_T}) of the particles with indices l.

Equations

• CSMC.trajOf y l t = y (t, l t)

def CSMC.traceBack {n N : ℕ} (a : Anc n N) (bT : Fin N) : Idx n N

The indices traced back from the final index b_T through the ancestors: b_t = a_t^{b_{t+1}} for t < T (Section 3).

Equations

• CSMC.traceBack a bT = Fin.reverseInduction bT fun (s : Fin n) (j : Fin N) => a s j

@[simp]

theorem CSMC.traceBack_last {n N : ℕ} (a : Anc n N) (bT : Fin N) : traceBack a bT (Fin.last n) = bT

The indices traced back from b_T take the value b_T at the final time.

theorem CSMC.traceBack_castSucc {n N : ℕ} (a : Anc n N) (bT : Fin N) (s : Fin n) : traceBack a bT s.castSucc = a s (traceBack a bT s.succ)

The indices traced back from b_T satisfy b_t = a_t^{b_{t+1}}.

theorem CSMC.eq_traceBack_iff {n N : ℕ} {a : Anc n N} {b : Idx n N} : b = traceBack a (b (Fin.last n)) ↔ ∀ (s : Fin n), a s (b s.succ) = b s.castSucc

A sequence of indices is the one traced back from its final index if and only if b_t = a_t^{b_{t+1}} for every t < T.

def CSMC.freeCoords {n N : ℕ} (b : Idx n N) : Finset (Fin (n + 1) × Fin N)

The coordinates (t, i), i ≠ b_t, of the particles other than those with indices b.

Equations

• CSMC.freeCoords b = {p : Fin (n + 1) × Fin N | p.2 ≠ b p.1}

def CSMC.embed {X : Type u_1} {n N : ℕ} (x : Traj X n) : Pos X n N

The particle positions with the state x_t at every particle of time t.

Equations

• CSMC.embed x p = x p.1

noncomputable def CSMC.refKernel {X : Type u_1} {n N : ℕ} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (b : Idx n N) : ProbabilityTheory.Kernel (Traj X n) (Pos X n N)

The measure on the particle positions, given the reference trajectory x, with x_t at the coordinate (t, b_t) and the measure μ on each other coordinate, independently.

Equations

• CSMC.refKernel μ b = CSMC.updateKernel μ (CSMC.freeCoords b) CSMC.embed

instance CSMC.instIsSFiniteKernelTrajPosRefKernel {X : Type u_1} {n N : ℕ} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (b : Idx n N) : ProbabilityTheory.IsSFiniteKernel (refKernel μ b)

noncomputable def CSMC.unifIdx (n N : ℕ) : MeasureTheory.Measure (Idx n N)

The distribution of T independent uniform indices on [N] (Algorithm 1.a).

Equations

• CSMC.unifIdx n N = MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => ProbabilityTheory.uniformOn Set.univ