Markov chains backwards in time on a finite set

In the backward passes of the paper, the indices form Markov chains backwards in time: a state is drawn at the final time T, then, for t = T - 1, …, 1, a state at time t given the state at time t + 1. For a finite state space S, the probability of a trajectory of such a chain and its marginal distributions, computed by backward recursion, are defined here.

Time is indexed by Fin (n + 1), with T = n + 1. The step from time s.succ to time s.castSucc is indexed by s : Fin n. The initial distribution μ is that of the state at time Fin.last n. The probability of moving from y at time s.succ to z at time s.castSucc is P s y z.

def CSMC.chainProb {S : Type u_1} {n : ℕ} (μ : S → ℝ) (P : Fin n → S → S → ℝ) (x : Fin (n + 1) → S) : ℝ

The probability μ(x_T) ∏_s P_s(x_{s+1}, x_s) of the trajectory x of the backward chain with initial distribution μ at the final time and transition probabilities P.

Equations

• CSMC.chainProb μ P x = μ (x (Fin.last n)) * ∏ s : Fin n, P s (x s.succ) (x s.castSucc)

def CSMC.chainMarg {S : Type u_1} [Fintype S] {n : ℕ} (μ : S → ℝ) (P : Fin n → S → S → ℝ) : Fin (n + 1) → S → ℝ

The marginal distributions of the backward chain, by backward recursion: μ at the final time and z ↦ ∑ y, m y * P s y z at time s.castSucc, if m is the marginal at time s.succ.

Equations

• CSMC.chainMarg μ P = Fin.reverseInduction (motive := fun (x : Fin (n + 1)) => S → ℝ) μ fun (s : Fin n) (m : S → ℝ) (z : S) => ∑ y : S, m y * P s y z

theorem CSMC.chainMarg_last {S : Type u_1} [Fintype S] {n : ℕ} (μ : S → ℝ) (P : Fin n → S → S → ℝ) : chainMarg μ P (Fin.last n) = μ

The marginal at the final time is the initial distribution.

theorem CSMC.chainMarg_castSucc {S : Type u_1} [Fintype S] {n : ℕ} (μ : S → ℝ) (P : Fin n → S → S → ℝ) (s : Fin n) (z : S) : chainMarg μ P s.castSucc z = ∑ y : S, chainMarg μ P s.succ y * P s y z

The backward recursion of the marginals.

theorem CSMC.chainMarg_succ {S : Type u_1} [Fintype S] {n : ℕ} (μ : S → ℝ) (P : Fin (n + 1) → S → S → ℝ) (t : Fin (n + 1)) : chainMarg μ P t.succ = chainMarg μ (fun (s : Fin n) => P s.succ) t

The marginal at time t.succ of the chain with the transitions P is the marginal at time t of the chain with the transitions P s.succ.

theorem CSMC.chainProb_cons {S : Type u_1} {n : ℕ} (μ : S → ℝ) (P : Fin (n + 1) → S → S → ℝ) (x₀ : S) (x : Fin (n + 1) → S) : chainProb μ P (Fin.cons x₀ x) = P 0 (x 0) x₀ * chainProb μ (fun (s : Fin n) => P s.succ) x

The probability of a trajectory which starts with x₀ at the first time and continues with x is P_0(x_0, x₀) times the probability of x under the chain with the transitions P s.succ.

theorem CSMC.sum_chainProb_eq_chainMarg {S : Type u_1} [Fintype S] {n : ℕ} [DecidableEq S] (μ : S → ℝ) {P : Fin n → S → S → ℝ} (hP : ∀ (s : Fin n) (y : S), ∑ z : S, P s y z = 1) (t : Fin (n + 1)) (z : S) : (∑ x : Fin (n + 1) → S, if x t = z then chainProb μ P x else 0) = chainMarg μ P t z

If the transition probabilities sum to one, the sum of the probabilities of the trajectories which are at z at time t is the marginal at time t evaluated at z.

theorem CSMC.sum_chainProb_mul {S : Type u_1} [Fintype S] {n : ℕ} (μ : S → ℝ) {P : Fin n → S → S → ℝ} (hP : ∀ (s : Fin n) (y : S), ∑ z : S, P s y z = 1) (t : Fin (n + 1)) (G : S → ℝ) : ∑ x : Fin (n + 1) → S, chainProb μ P x * G (x t) = ∑ z : S, chainMarg μ P t z * G z

If the transition probabilities sum to one, the sum over the trajectories of their probability times a function of the state at time t is the sum over the states of the marginal at time t times this function.

theorem CSMC.sum_chainProb_mul_step {S : Type u_1} [Fintype S] {n : ℕ} (μ : S → ℝ) {P : Fin n → S → S → ℝ} (hP : ∀ (s : Fin n) (y : S), ∑ z : S, P s y z = 1) (s : Fin n) (φ : S → S → ℝ) : ∑ x : Fin (n + 1) → S, chainProb μ P x * φ (x s.succ) (x s.castSucc) = ∑ y : S, chainMarg μ P s.succ y * ∑ z : S, P s y z * φ y z

If the transition probabilities sum to one, the sum over the trajectories of their probability times a function φ of the states at the times s.succ and s.castSucc is ∑_y m(y) ∑_z P_s(y, z) φ(y, z), with the marginal m at time s.succ.

theorem CSMC.sum_prod_mul_last {S : Type u_1} [Fintype S] {n : ℕ} {R : Type u_2} [CommSemiring R] {P : Fin n → S → S → R} (hP : ∀ (s : Fin n) (y : S), ∑ z : S, P s y z = 1) (F : S → R) : ∑ x : Fin (n + 1) → S, (∏ s : Fin n, P s (x s.succ) (x s.castSucc)) * F (x (Fin.last n)) = ∑ z : S, F z

If the transition probabilities, with values in a commutative semiring, sum to one, the sum over the trajectories of the product of the transition probabilities times a function of the state at the final time is the sum of this function over the states.