Hidden Markov models

StructureHidden Markov model#✓fully proved

A hidden Markov model with a set of states \(S\), a set of observations \(O\) and weights in \(R\) consists of an initial weight \(\pi(s) \in R\) for each state \(s\), a transition weight \(a(s, s') \in R\) for each pair of states, the weight of a transition from \(s\) to \(s'\), and an emission weight \(e(s, o) \in R\) for each state \(s\) and observation \(o\), the weight of emitting \(o\) from \(s\).

No structure on \(R\) and no normalization of the weights is required.

structure HMM (S O R : Type*) where
  /-- The initial weight of each state. -/
  init : S → R
  /-- The weight of a transition from the first state to the second. -/
  trans : S → S → R
  /-- The weight of emitting an observation from a state. -/
  emit : S → O → R
Used by 74
Used byThe ChromHMM update maximizes Q(· | θ) · Positivity of the ChromHMM joint weight · The log-likelihood is monotone along the ChromHMM iterates · Each ChromHMM step does not decrease the log-likelihood · The ChromHMM M-step · The ChromHMM update is a valid parameter · HMM of ChromHMM parameters · Valid ChromHMM parameters give a valid HMM · Valid HMM built from a valid ChromHMM parameter · The collapsed forward recursion computes the forward variables · The Li–Stephens copying model · Uniform initial law over haplotypes sums to one · The Baum-Welch objective in terms of expected counts · The Baum-Welch update maximizes the EM objective · One Baum-Welch step · The expected emissions from forward-backward · The expected starts from forward-backward · The EM model of a hidden Markov model · The log path weight is linear in the path's counts · The Baum-Welch log-likelihood is the HMM log-likelihood · The log-likelihood is monotone along the Baum-Welch iterates · Each Baum-Welch step does not decrease the log-likelihood · The Baum-Welch M-step · The EM marginal of an HMM is its likelihood · Pairwise state marginal of a hidden Markov model · Pairwise forward-backward · Path weight as a product · Pairwise path sums with a fixed endpoint · The expected transitions from forward-backward · Valid hidden Markov model parameters · Valid HMMs · The chain CRF of a hidden Markov model · The chain CRF of a hidden Markov model has the same path weights · Backpointer of the tabulated Viterbi algorithm · Backward variables of a hidden Markov model · One step of the tabulated backward algorithm · The tabulated backward algorithm · Backtracked path of the tabulated Viterbi algorithm · Bridge weights of a hidden Markov model · Front decomposition of the bridge weights · The Viterbi variables are attained · Posterior expected number of correctly decoded states · The expected number of correct states is a sum of posteriors · Posterior decoding maximizes the expected number of correctly decoded states · Forward variables of a hidden Markov model · The forward variables are path sums · One step of the tabulated forward algorithm · Tabulated forward algorithm · Likelihood of the observations · The forward algorithm computes the likelihood · The likelihood from the forward and backward variables · Tabulated likelihood of a hidden Markov model · Hidden Markov models with nonnegative weights · Joint weight of a state path and the observations · The backtracked path of a hidden Markov model attains the Viterbi variable · Path weights of a hidden Markov model are bounded by the Viterbi variables · The Viterbi path is a most probable path · Posterior decoding · Smoothed state weights · Forward-backward smoothing is a joint-to-likelihood ratio · Smoothed posterior as a sum over state paths · Posterior path maximizes the posterior at each time · Smoothing weights are nonnegative · Tabulated forward-backward smoothing · Joint weight of the observations and a state · Forward-backward identity · Bridge weights sum to the backward variable · Paths through two fixed states · Smoothed weights sum to one · Viterbi computes the MAP value · The Viterbi variables of a hidden Markov model · Viterbi's MAP path · One step of the tabulated Viterbi recursion for a hidden Markov model · The tabulated Viterbi variables of a hidden Markov model

DefinitionJoint weight of a state path and the observations#✓fully proved

For a hidden Markov model \(h\) with initial weights \(\pi\), transition weights \(a\) and emission weights \(b\) in a semiring, observations \(x_0, x_1, \dots\) and \(t \in \mathbb{N}\), the joint weight of a state path \(z = (z_0, \dots, z_t)\) and \(x_0, \dots, x_t\) is the product, taken from left to right, \(\pi(z_0)\, b(z_0, x_0)\, a(z_0, z_1)\, b(z_1, x_1) \cdots a(z_{t-1}, z_t)\, b(z_t, x_t)\).

def pathProb : (t : ℕ) → (Fin (t + 1) → S) → R
  | 0, z => h.init (z 0) * h.emit (z 0) (x 0)
  | t + 1, z => pathProb t (Fin.init z) * h.trans (z (Fin.last t).castSucc) (z (Fin.last (t + 1))) *
      h.emit (z (Fin.last (t + 1))) (x (t + 1))
Uses 1 · Used by 33
Statement usesHidden Markov model
Used byThe ChromHMM update maximizes Q(· | θ) · Positivity of the ChromHMM joint weight · The ChromHMM update is a valid parameter · The Baum-Welch update maximizes the EM objective · One Baum-Welch step · The expected emissions from forward-backward · The expected starts from forward-backward · The EM model of a hidden Markov model · The log path weight is linear in the path's counts · The log-likelihood is monotone along the Baum-Welch iterates · Each Baum-Welch step does not decrease the log-likelihood · Pairwise state marginal of a hidden Markov model · Pairwise forward-backward · Path weight as a product · Pairwise path sums with a fixed endpoint · The expected transitions from forward-backward · The chain CRF of a hidden Markov model has the same path weights · The Viterbi variables are attained · Posterior expected number of correctly decoded states · The expected number of correct states is a sum of posteriors · The forward variables are path sums · Likelihood of the observations · The forward algorithm computes the likelihood · The likelihood from the forward and backward variables · The backtracked path of a hidden Markov model attains the Viterbi variable · Path weights of a hidden Markov model are bounded by the Viterbi variables · The Viterbi path is a most probable path · Smoothed posterior as a sum over state paths · Smoothing weights are nonnegative · Joint weight of the observations and a state · Forward-backward identity · Paths through two fixed states · Viterbi computes the MAP value

DefinitionLikelihood of the observations#✓fully proved

For a hidden Markov model \(h\) with a finite set of states \(S\) and weights in a semiring, observations \(x_0, x_1, \dots\) and \(t \in \mathbb{N}\), the likelihood of \(x_0, \dots, x_t\) is the sum, over all state paths \(z = (z_0, \dots, z_t) \in S^{t+1}\), of the joint weight of \(z\) and \(x_0, \dots, x_t\).

def likelihood (t : ℕ) : R := ∑ z : Fin (t + 1) → S, pathProb h x t z
Uses 2 · Used by 17
Statement usesHidden Markov model · Joint weight of a state path and the observations
Used byEM log-likelihood as a sum of HMM log-likelihoods · The likelihood of the target haplotype · Tabulated recursion computes the haplotype likelihood · The expected emissions from forward-backward · The expected starts from forward-backward · The Baum-Welch log-likelihood is the HMM log-likelihood · The EM marginal of an HMM is its likelihood · The expected transitions from forward-backward · Posterior expected number of correctly decoded states · The expected number of correct states is a sum of posteriors · The forward algorithm computes the likelihood · The likelihood from the forward and backward variables · Smoothed state weights · Forward-backward smoothing is a joint-to-likelihood ratio · Smoothed posterior as a sum over state paths · Smoothing weights are nonnegative · Smoothed weights sum to one

DefinitionForward variables of a hidden Markov model#✓fully proved

Let \(h\) be a hidden Markov model with a finite set of states \(S\) and weights in a semiring \(R\), with initial weights \(\pi(s)\), transition weights \(a(s', s)\) from \(s'\) to \(s\) and emission weights \(e(s, o)\) of the observation \(o\) from the state \(s\), and let \(x\) be an observation sequence. The forward variables are defined by \(\alpha_0(s) = \pi(s) \, e(s, x_0)\) and \(\alpha_{t+1}(s) = \left(\sum_{s'} \alpha_t(s') \, a(s', s)\right) e(s, x_{t+1})\), the sum running over all states \(s'\).

The forward variable \(\alpha_t(s)\) is the weight of the observations \(x_0, \dots, x_t\) with the state at time \(t\) equal to \(s\).

def forward : ℕ → S → R
  | 0, s => h.init s * h.emit s (x 0)
  | t + 1, s => (∑ s', forward t s' * h.trans s' s) * h.emit s (x (t + 1))
Uses 1 · Used by 17
Statement usesHidden Markov model
Used byThe collapsed forward recursion computes the forward variables · Tabulated recursion computes the Li–Stephens forward variables · The likelihood of the target haplotype · Tabulated recursion computes the haplotype likelihood · The expected emissions from forward-backward · The expected starts from forward-backward · Pairwise forward-backward · Pairwise path sums with a fixed endpoint · The expected transitions from forward-backward · The forward variables are path sums · The forward algorithm computes the likelihood · The likelihood from the forward and backward variables · Smoothed state weights · Forward-backward smoothing is a joint-to-likelihood ratio · Forward-backward identity · Paths through two fixed states · Smoothed weights sum to one

TheoremThe forward variables are path sums#✓fully proved

Let \(h\) be a hidden Markov model with a finite set of states \(S\) and weights in a semiring \(R\), and let \(x\) be an observation sequence. For every time \(t\) and every state \(s\), the forward variable \(\alpha_t(s)\) equals \(\sum_z p_t(z)\), the sum running over the state paths \(z = (z_0, \dots, z_t) \in S^{t+1}\) with \(z_t = s\), where \(p_t(z)\) is the joint weight of \(z\) and the observations \(x_0, \dots, x_t\).

theorem forward_eq [DecidableEq S] : ∀ (t : ℕ) (s : S),
    forward h x t s = ∑ z : Fin (t + 1) → S, if z (Fin.last t) = s then pathProb h x t z else 0
Uses 3 · Used by 3
Statement usesHidden Markov model · Forward variables of a hidden Markov model · Joint weight of a state path and the observations
Used byPairwise path sums with a fixed endpoint · The forward algorithm computes the likelihood · Paths through two fixed states

TheoremThe forward algorithm computes the likelihood#✓fully proved

Let \(h\) be a hidden Markov model with a finite set of states \(S\), initial weights \(\pi\), transition weights \(a\) and emission weights \(b\) in a semiring, and let \(x_0, x_1, \dots\) be observations. Let \(\alpha\) be the forward variables, \(\alpha_0(s) = \pi(s)\, b(s, x_0)\) and \(\alpha_{t+1}(s) = \bigl(\sum_{s' \in S} \alpha_t(s')\, a(s', s)\bigr)\, b(s, x_{t+1})\). Then for every \(t \in \mathbb{N}\) the likelihood of \(x_0, \dots, x_t\) equals \(\sum_{s \in S} \alpha_t(s)\).

theorem likelihood_eq_sum_forward (t : ℕ) :
    likelihood h x t = ∑ s, forward h x t s
Uses 5 · Used by 2
Statement usesHidden Markov model · Forward variables of a hidden Markov model · Likelihood of the observations
Proof usesThe forward variables are path sums · Joint weight of a state path and the observations
Used byThe likelihood of the target haplotype · Tabulated recursion computes the haplotype likelihood

DefinitionThe Viterbi variables of a hidden Markov model#✓fully proved

Let \(h\) be a hidden Markov model with a finite nonempty set of states \(S\), initial weights \(\pi(s)\), transition weights \(a(s', s)\) and emission weights \(b(s, o)\) in a linearly ordered commutative semiring \(R\), and let \(x_0, x_1, \dots\) be a sequence of observations. The Viterbi variables \(V_t(s)\), for \(t \in \mathbb{N}\) and \(s \in S\), are defined by \(V_0(s) = \pi(s) \, b(s, x_0)\) and

\[V_{t+1}(s) = \Big(\max_{s' \in S} V_t(s') \, a(s', s)\Big) \, b(s, x_{t+1}).\]

When all weights are nonnegative, \(V_t(s)\) is the largest joint weight of a state path of length \(t + 1\) ending in \(s\) and the observations \(x_0, \dots, x_t\).

def viterbi : ℕ → S → R
  | 0, s => h.init s * h.emit s (x 0)
  | t + 1, s => Finset.univ.sup' Finset.univ_nonempty (fun s' => viterbi t s' * h.trans s' s) *
      h.emit s (x (t + 1))
Uses 1 · Used by 5
Statement usesHidden Markov model
Used byThe Viterbi variables are attained · The backtracked path of a hidden Markov model attains the Viterbi variable · Path weights of a hidden Markov model are bounded by the Viterbi variables · The Viterbi path is a most probable path · Viterbi computes the MAP value

StructureHidden Markov models with nonnegative weights#✓fully proved

A hidden Markov model \(h\) with weights in a commutative semiring with a linear order has nonnegative weights when all of its initial weights, transition weights and emission weights are \(\ge 0\): for all states \(s, s'\) and every observation \(o\), the initial weight of \(s\), the weight of the transition from \(s\) to \(s'\), and the weight of emitting \(o\) from \(s\) are nonnegative.

structure HMM.Nonneg (h : HMM S O R) : Prop where
  /-- Initial weights are nonnegative. -/
  init : ∀ s, 0 ≤ h.init s
  /-- Transition weights are nonnegative. -/
  trans : ∀ s s', 0 ≤ h.trans s s'
  /-- Emission weights are nonnegative. -/
  emit : ∀ s o, 0 ≤ h.emit s o
Uses 1 · Used by 6
Statement usesHidden Markov model
Used byThe chain CRF of a hidden Markov model · The chain CRF of a hidden Markov model has the same path weights · Path weights of a hidden Markov model are bounded by the Viterbi variables · The Viterbi path is a most probable path · Smoothing weights are nonnegative · Viterbi computes the MAP value

TheoremPath weights of a hidden Markov model are bounded by the Viterbi variables#✓fully proved

Let \(h\) be a hidden Markov model with a finite nonempty set of states \(S\) and initial weights \(\pi\), transition weights \(a\) and emission weights \(b\) that are nonnegative elements of a linearly ordered commutative semiring, and let \(x_0, x_1, \dots\) be observations. Let \(\delta\) be the Viterbi variables, \(\delta_0(s) = \pi(s)\, b(s, x_0)\) and \(\delta_{t+1}(s) = \bigl(\max_{s' \in S} \delta_t(s')\, a(s', s)\bigr)\, b(s, x_{t+1})\). For every \(t \in \mathbb{N}\) and every state path \(z = (z_0, \dots, z_t) \in S^{t+1}\), the joint weight of \(z\) and \(x_0, \dots, x_t\) is at most \(\delta_t(z_t)\).

theorem pathProb_le_viterbi (hn : h.Nonneg) :
    ∀ (t : ℕ) (z : Fin (t + 1) → S), pathProb h x t z ≤ viterbi h x t (z (Fin.last t))
Uses 4 · Used by 2
Statement usesHidden Markov model · Hidden Markov models with nonnegative weights · Joint weight of a state path and the observations · The Viterbi variables of a hidden Markov model
Used byThe Viterbi path is a most probable path · Viterbi computes the MAP value

TheoremThe Viterbi variables are attained#✓fully proved

Let \(h\) be a hidden Markov model with a finite nonempty set of states \(S\) and weights in a commutative semiring \(R\) with a linear order, and let \(x\) be an observation sequence. For every time \(t\) and every state \(s\), there is a state path \(z = (z_0, \dots, z_t)\) with \(z_t = s\) whose joint weight with the observations \(x_0, \dots, x_t\) equals the Viterbi variable \(V_t(s)\).

No nonnegativity of the weights and no compatibility of the order with the operations is needed.

theorem exists_pathProb_eq_viterbi :
    ∀ (t : ℕ) (s : S),
      ∃ z : Fin (t + 1) → S, z (Fin.last t) = s ∧ pathProb h x t z = viterbi h x t s
Uses 3 · Used by 1
Statement usesHidden Markov model · Joint weight of a state path and the observations · The Viterbi variables of a hidden Markov model
Used byViterbi computes the MAP value

TheoremViterbi computes the MAP value#✓fully proved

Let \(h\) be a hidden Markov model with a finite nonempty set of states \(S\) and initial weights \(\pi\), transition weights \(a\) and emission weights \(b\) that are nonnegative elements of a linearly ordered commutative semiring, and let \(x_0, x_1, \dots\) be observations. Let \(\delta\) be the Viterbi variables, \(\delta_0(s) = \pi(s)\, b(s, x_0)\) and \(\delta_{t+1}(s) = \bigl(\max_{s' \in S} \delta_t(s')\, a(s', s)\bigr)\, b(s, x_{t+1})\). For every \(t \in \mathbb{N}\), \(\max_{s \in S} \delta_t(s)\) equals the maximum, over all state paths \(z \in S^{t+1}\), of the joint weight of \(z\) and \(x_0, \dots, x_t\).

theorem sup'_viterbi_eq (hn : h.Nonneg) (t : ℕ) :
    (Finset.univ : Finset S).sup' Finset.univ_nonempty (viterbi h x t) =
      (Finset.univ : Finset (Fin (t + 1) → S)).sup' Finset.univ_nonempty (pathProb h x t)
Uses 6
Statement usesHidden Markov model · Hidden Markov models with nonnegative weights · Joint weight of a state path and the observations · The Viterbi variables of a hidden Markov model
Proof usesThe Viterbi variables are attained · Path weights of a hidden Markov model are bounded by the Viterbi variables

DefinitionSum of the entries of a vector#✓fully proved

For a vector \(v = (v_0, \dots, v_{n-1})\) of length \(n\) with entries in an additive commutative monoid, its entry sum is \(\sum_{s < n} v_s\).

The vector is passed as an argument, so a table computed once is summed without recomputing it.

def sumVec [AddCommMonoid R] (v : Vector R n) : R := ∑ s : Fin n, v[s]
Used by 5
Used byTabulated O(K) forward step · The tabulated Li–Stephens likelihood · Tabulated recursion computes the haplotype likelihood · The tabulated forward algorithm for chain CRFs · Tabulated likelihood of a hidden Markov model

DefinitionOne step of the tabulated forward algorithm#✓fully proved

Let \(h\) be a hidden Markov model with states \(\{0, \dots, n-1\}\) and weights in a semiring \(R\), with transition weight \(a(s', s)\) from \(s'\) to \(s\) and emission weight \(e(s, o)\) of the observation \(o\) from the state \(s\), and let \(x\) be an observation sequence. For a table \(v \in R^n\) and a step \(t\), the forward step returns the table whose entry at a state \(s\) is

\[\Bigl(\sum_{s'=0}^{n-1} v_{s'} \, a(s', s)\Bigr) \, e(s, x_{t+1}).\]
def forwardStep (v : Vector R n) (t : ℕ) : Vector R n :=
  Vector.ofFn fun s => (∑ s', v[s'] * h.trans s' s) * h.emit s (x (t + 1))
Uses 1 · Used by 1
Statement usesHidden Markov model
Used byTabulated forward algorithm

DefinitionTabulated forward algorithm#✓fully proved

Let \(h\) be a hidden Markov model with states \(\{0, \dots, n-1\}\) and weights in a semiring \(R\), with initial weight \(\pi(s)\) and emission weight \(e(s, o)\) of the observation \(o\) from the state \(s\), and let \(x\) be an observation sequence. The forward table is the sequence of vectors in \(R^n\) defined by recursion on time: at time \(0\) its entry at \(s\) is \(\pi(s) \, e(s, x_0)\), and the table at time \(t + 1\) is the forward step at step \(t\) applied to the table at time \(t\).

Each step takes \(O(n^2)\) operations, and the entry at \(s\) of the table at time \(t\) is the forward variable \(\alpha_t(s)\).

def forwardTab : ℕ → Vector R n
  | 0 => Vector.ofFn fun s => h.init s * h.emit s (x 0)
  | t + 1 => forwardStep x h (forwardTab t) t
Uses 2 · Used by 2
Statement usesHidden Markov model · One step of the tabulated forward algorithm
Used byTabulated likelihood of a hidden Markov model · Tabulated forward-backward smoothing

DefinitionTabulated likelihood of a hidden Markov model#✓fully proved

For a hidden Markov model \(h\) with states \(0, \dots, n - 1\) and weights in a semiring, observations \(x_0, x_1, \dots\) and \(t \in \mathbb{N}\), the tabulated likelihood at time \(t\) is the sum \(\sum_{s < n} v_s\) of the entries of the forward table \(v = (v_0, \dots, v_{n-1})\) at time \(t\).

The forward table is computed step by step with \(O(n^2)\) semiring operations per step, so the tabulated likelihood costs \(O(t n^2)\) operations; it equals the likelihood of \(x_0, \dots, x_t\).

def likelihoodTab (t : ℕ) : R := sumVec (forwardTab x h t)
Uses 3 · Used by 1
Statement usesHidden Markov model · Tabulated forward algorithm · Sum of the entries of a vector
Used byTabulated forward-backward smoothing

DefinitionFirst maximizer of a function on a finite range#✓fully proved

Let \(n \ge 1\) and let \(R\) be a linearly ordered set. For a function \(f\) from \(\{0, \dots, n-1\}\) to \(R\), the maximizer of \(f\) is the first \(i\), in the order \(0, \dots, n-1\), at which \(f\) attains its maximum, that is, \(f(j) \le f(i)\) for every \(j\).

def argmaxFin (f : Fin n → R) : Fin n := ((List.finRange n).argmax f).getD 0
Used by 9
Used byBackpointer of the tabulated CRF Viterbi algorithm · The backtracked path of a chain CRF attains the Viterbi variable · The Viterbi path of a chain CRF has maximal weight · Index of a largest entry of a table · Backpointer of the tabulated Viterbi algorithm · The backtracked path of a hidden Markov model attains the Viterbi variable · The Viterbi path is a most probable path · Posterior decoding · Posterior path maximizes the posterior at each time

DefinitionOne step of the tabulated Viterbi recursion for a hidden Markov model#✓fully proved

Let \(h\) be a hidden Markov model with states \(\{0, \dots, n - 1\}\), where \(n \ge 1\), transition weights \(a(s', s)\) and emission weights \(b(s, o)\) in a linearly ordered commutative semiring \(R\), and let \(x_0, x_1, \dots\) be a sequence of observations. Given a vector \(v \in R^n\) and \(t \in \mathbb{N}\), the Viterbi step returns the vector in \(R^n\) whose entry at state \(s\) is

\[\Big(\max_{s'} v_{s'} \, a(s', s)\Big) \, b(s, x_{t+1}).\]
def viterbiStep (v : Vector R n) (t : ℕ) : Vector R n :=
  Vector.ofFn fun s => Finset.univ.sup' Finset.univ_nonempty (fun s' => v[s'] * h.trans s' s) *
    h.emit s (x (t + 1))
Uses 1 · Used by 1
Statement usesHidden Markov model
Used byThe tabulated Viterbi variables of a hidden Markov model

DefinitionThe tabulated Viterbi variables of a hidden Markov model#✓fully proved

Let \(h\) be a hidden Markov model with states \(\{0, \dots, n - 1\}\), where \(n \ge 1\), initial weights \(\pi(s)\), transition weights \(a(s', s)\) and emission weights \(b(s, o)\) in a linearly ordered commutative semiring \(R\), and let \(x_0, x_1, \dots\) be a sequence of observations. The Viterbi table assigns to each \(t \in \mathbb{N}\) a vector \(T_t \in R^n\): the vector \(T_0\) has entry \(\pi(s) \, b(s, x_0)\) at each state \(s\), and \(T_{t+1}\) is the Viterbi step at time \(t\) applied to \(T_t\), the vector whose entry at state \(s\) is \(\big(\max_{s'} (T_t)_{s'} \, a(s', s)\big) \, b(s, x_{t+1})\).

The entry of \(T_t\) at state \(s\) is the Viterbi variable of \(s\) at time \(t\).

def viterbiTab : ℕ → Vector R n
  | 0 => Vector.ofFn fun s => h.init s * h.emit s (x 0)
  | t + 1 => viterbiStep x h (viterbiTab t) t
Uses 2 · Used by 4
Statement usesHidden Markov model · One step of the tabulated Viterbi recursion for a hidden Markov model
Used byBacktracked path of the tabulated Viterbi algorithm · The backtracked path of a hidden Markov model attains the Viterbi variable · The Viterbi path is a most probable path · Viterbi's MAP path

DefinitionBackpointer of the tabulated Viterbi algorithm#✓fully proved

Let \(h\) be a hidden Markov model with states \(\{0, \dots, n-1\}\), where \(n \ge 1\), and weights in a commutative semiring \(R\) with a linear order, and let \(a(s', s)\) be its transition weight from \(s'\) to \(s\). For a table \(v \in R^n\) and a state \(s\), the backpointer of \(s\) is the first state \(s'\), in the order \(0, \dots, n-1\), that maximizes \(v_{s'} \, a(s', s)\).

No compatibility of the order with the operations is needed.

def back (v : Vector R n) (s : Fin n) : Fin n := argmaxFin fun s' => v[s'] * h.trans s' s
Uses 2 · Used by 2
Statement usesHidden Markov model · First maximizer of a function on a finite range
Used byBacktracked path of the tabulated Viterbi algorithm · The backtracked path of a hidden Markov model attains the Viterbi variable

DefinitionBacktracked path of the tabulated Viterbi algorithm#✓fully proved

Let \(h\) be a hidden Markov model with states \(\{0, \dots, n-1\}\), where \(n \ge 1\), and weights in a commutative semiring with a linear order, and fix an observation sequence \(x\). For a state \(s\), the backtracked path \(b_t(s) = (b_t(s)_0, \dots, b_t(s)_t)\) of length \(t + 1\) is defined by recursion on \(t\): \(b_0(s)\) is the one-state path \((s)\), and \(b_{t+1}(s)\) is \(b_t(s')\) followed by \(s\), where \(s'\) is the backpointer of \(s\) computed from the Viterbi table at time \(t\).

No compatibility of the order with the operations is needed.

def bestPath : (t : ℕ) → Fin n → Fin (t + 1) → Fin n
  | 0, s => fun _ => s
  | t + 1, s => Fin.snoc (bestPath t (back h (viterbiTab x h t) s)) s
Uses 3 · Used by 3
Statement usesHidden Markov model · Backpointer of the tabulated Viterbi algorithm · The tabulated Viterbi variables of a hidden Markov model
Used byThe backtracked path of a hidden Markov model attains the Viterbi variable · The Viterbi path is a most probable path · Viterbi's MAP path

TheoremThe backtracked path of a hidden Markov model attains the Viterbi variable#✓fully proved

Let \(h\) be a hidden Markov model with states \(0, \dots, n - 1\), where \(n \ge 1\), initial weights \(\pi\), transition weights \(a\) and emission weights \(b\) in a commutative semiring with a linear order, and let \(x_0, x_1, \dots\) be observations. Let \(\delta\) be the Viterbi variables, \(\delta_0(s) = \pi(s)\, b(s, x_0)\) and \(\delta_{t+1}(s) = \bigl(\max_{s'} \delta_t(s')\, a(s', s)\bigr)\, b(s, x_{t+1})\). For every \(t \in \mathbb{N}\) and every state \(s\), the joint weight of \(x_0, \dots, x_t\) and the backtracked path of length \(t + 1\) ending in \(s\), obtained by following the backpointers, equals \(\delta_t(s)\).

theorem pathProb_bestPath : ∀ (t : ℕ) (s : Fin n),
    pathProb h x t (bestPath x h t s) = viterbi h x t s
Uses 7 · Used by 1
Statement usesHidden Markov model · Backtracked path of the tabulated Viterbi algorithm · Joint weight of a state path and the observations · The Viterbi variables of a hidden Markov model
Proof usesFirst maximizer of a function on a finite range · Backpointer of the tabulated Viterbi algorithm · The tabulated Viterbi variables of a hidden Markov model
Used byThe Viterbi path is a most probable path

DefinitionIndex of a largest entry of a table#✓fully proved

Let \(n \ge 1\) and let \(R\) be a linearly ordered set. For a table \(v = (v_0, \dots, v_{n-1}) \in R^n\), the maximizing index of \(v\) is the first index \(s\), in the order \(0, \dots, n-1\), such that \(v_{s'} \le v_s\) for every \(s'\).

def argmaxVec (v : Vector R n) : Fin n := argmaxFin fun s => v[s]
Uses 1 · Used by 4
Statement usesFirst maximizer of a function on a finite range
Used byThe Viterbi path of a chain CRF · The Viterbi path of a chain CRF has maximal weight · The Viterbi path is a most probable path · Viterbi's MAP path

DefinitionViterbi's MAP path#✓fully proved

Let \(h\) be a hidden Markov model with states \(\{0, \dots, n - 1\}\), where \(n \ge 1\), whose weights lie in a linearly ordered commutative semiring \(R\), with transition weights \(a(s', s)\), and let \(x\) be a sequence of observations. For \(t \in \mathbb{N}\), let \(T_0, \dots, T_t \in R^n\) be the tabulated Viterbi variables of \(h\) on \(x\). The Viterbi path of length \(t + 1\) is the state path \((z_0, \dots, z_t)\) in which \(z_t\) is the first state \(s\), in the order \(0, \dots, n - 1\), that maximizes \((T_t)_s\), and, for \(k < t\), \(z_k\) is the first state \(s'\) that maximizes \((T_k)_{s'} \, a(s', z_{k+1})\).

def viterbiPath (t : ℕ) : Fin (t + 1) → Fin n :=
  bestPath x h t (argmaxVec (viterbiTab x h t))
Uses 4 · Used by 1
Statement usesHidden Markov model · Index of a largest entry of a table · Backtracked path of the tabulated Viterbi algorithm · The tabulated Viterbi variables of a hidden Markov model
Used byThe Viterbi path is a most probable path

TheoremThe Viterbi path is a most probable path#✓fully proved

Let \(h\) be a hidden Markov model with states \(0, \dots, n - 1\), where \(n \ge 1\), and nonnegative weights in a linearly ordered commutative semiring, and let \(x_0, x_1, \dots\) be observations. For every \(t \in \mathbb{N}\) and every state path \(z = (z_0, \dots, z_t)\), the joint weight of \(z\) and \(x_0, \dots, x_t\) is at most the joint weight of the Viterbi path of length \(t + 1\) and \(x_0, \dots, x_t\).

theorem pathProb_le_viterbiPath (hn : h.Nonneg) (t : ℕ) (z : Fin (t + 1) → Fin n) :
    pathProb h x t z ≤ pathProb h x t (viterbiPath x h t)
Uses 11
Statement usesHidden Markov model · Hidden Markov models with nonnegative weights · Joint weight of a state path and the observations · Viterbi's MAP path
Proof usesFirst maximizer of a function on a finite range · Index of a largest entry of a table · Backtracked path of the tabulated Viterbi algorithm · The backtracked path of a hidden Markov model attains the Viterbi variable · Path weights of a hidden Markov model are bounded by the Viterbi variables · The Viterbi variables of a hidden Markov model · The tabulated Viterbi variables of a hidden Markov model

DefinitionBackward variables of a hidden Markov model#✓fully proved

Let \(h\) be a hidden Markov model with finite state set \(S\), transition weights \(a\) and emission weights \(b\) in a semiring \(R\), and let \(x_0, x_1, \dots\) be observations. The backward variables \(\beta_k(t, s) \in R\), for \(k, t \in \mathbb{N}\) and \(s \in S\), are defined by \(\beta_0(t, s) = 1\) and

\[\beta_{k+1}(t, s) = \sum_{s' \in S} a(s, s')\, b(s', x_{t+1})\, \beta_k(t + 1, s').\]

Thus \(\beta_k(t, s)\) is the weight of the observations \(x_{t+1}, \dots, x_{t+k}\) given the state \(s\) at time \(t\).

def backward : ℕ → ℕ → S → R
  | 0, _, _ => 1
  | k + 1, t, s => ∑ s', h.trans s s' * h.emit s' (x (t + 1)) * backward k (t + 1) s'
Uses 1 · Used by 10
Statement usesHidden Markov model
Used byThe expected emissions from forward-backward · The expected starts from forward-backward · Pairwise forward-backward · The expected transitions from forward-backward · The likelihood from the forward and backward variables · Smoothed state weights · Forward-backward smoothing is a joint-to-likelihood ratio · Forward-backward identity · Bridge weights sum to the backward variable · Smoothed weights sum to one

DefinitionBridge weights of a hidden Markov model#✓fully proved

Let \(h\) be a hidden Markov model with finite state set \(S\), transition weights \(a\) and emission weights \(b\) in a semiring \(R\), and let \(x_0, x_1, \dots\) be observations. The bridge weights \(B_k(t, s, u) \in R\), for \(k, t \in \mathbb{N}\) and \(s, u \in S\), are defined from the end by \(B_0(t, s, u) = 1\) if \(s = u\) and \(B_0(t, s, u) = 0\) otherwise, and

\[B_{k+1}(t, s, u) = \left(\sum_{u' \in S} B_k(t, s, u')\, a(u', u)\right) b(u, x_{t+k+1}).\]

Thus \(B_k(t, s, u)\) is the total weight of the paths from state \(s\) at time \(t\) to state \(u\) at time \(t + k\), with transitions and emissions at times \(t + 1, \dots, t + k\).

def bridge [DecidableEq S] : ℕ → ℕ → S → S → R
  | 0, _, s, u => if s = u then 1 else 0
  | k + 1, t, s, u => (∑ u', bridge k t s u' * h.trans u' u) * h.emit u (x (t + k + 1))
Uses 1 · Used by 6
Statement usesHidden Markov model
Used byPairwise forward-backward · Pairwise path sums with a fixed endpoint · Front decomposition of the bridge weights · Forward-backward identity · Bridge weights sum to the backward variable · Paths through two fixed states

DefinitionJoint weight of the observations and a state#✓fully proved

For a hidden Markov model with a finite set of states \(S\) and weights in a semiring, observations \(x_0, x_1, \dots\), times \(t, k \in \mathbb{N}\) and a state \(s \in S\), the joint weight of \(x_0, \dots, x_{t+k}\) and the state \(s\) at time \(t\) is the sum of the path weights \(p_{t+k}(z)\) over all state paths \(z = (z_0, \dots, z_{t+k})\) in \(S\) with \(z_t = s\), where \(p_{t+k}(z)\) is the joint weight of the path \(z\) and the observations \(x_0, \dots, x_{t+k}\).

def stateMarg [DecidableEq S] (t k : ℕ) (s : S) : R :=
  ∑ z : Fin (t + k + 1) → S, if z ⟨t, by omega⟩ = s then pathProb h x (t + k) z else 0
Uses 2 · Used by 7
Statement usesHidden Markov model · Joint weight of a state path and the observations
Used byThe expected emissions from forward-backward · The expected starts from forward-backward · The likelihood from the forward and backward variables · Forward-backward smoothing is a joint-to-likelihood ratio · Smoothed posterior as a sum over state paths · Smoothing weights are nonnegative · Forward-backward identity

TheoremFront decomposition of the bridge weights#✓fully proved

Let \(h\) be a hidden Markov model with finite state set \(S\), transition weights \(a\) and emission weights \(b\) in a semiring, let \(x_0, x_1, \dots\) be observations, and write \(B_k(t, s, u)\) for the bridge weight of the paths from state \(s\) at time \(t\) to state \(u\) at time \(t + k\). Then for all \(k, t \in \mathbb{N}\) and \(s, u \in S\),

\[B_{k+1}(t, s, u) = \sum_{s' \in S} a(s, s')\, b(s', x_{t+1})\, B_k(t + 1, s', u).\]
theorem bridge_succ_front [DecidableEq S] : ∀ (k t : ℕ) (s u : S),
    bridge h x (k + 1) t s u =
      ∑ s', h.trans s s' * h.emit s' (x (t + 1)) * bridge h x k (t + 1) s' u
Uses 2 · Used by 1
Statement usesHidden Markov model · Bridge weights of a hidden Markov model
Used byBridge weights sum to the backward variable

TheoremBridge weights sum to the backward variable#✓fully proved

For a hidden Markov model with a finite set of states \(S\) and weights in a semiring, observations \(x_0, x_1, \dots\), all \(k, t \in \mathbb{N}\) and every state \(s \in S\), the sum over all states \(u \in S\) of the bridge weight from state \(s\) at time \(t\) to state \(u\) at time \(t + k\) equals the backward variable \(\beta_{k,t}(s)\), the weight of the observations \(x_{t+1}, \dots, x_{t+k}\) given the state \(s\) at time \(t\).

theorem sum_bridge [DecidableEq S] :
    ∀ (k t : ℕ) (s : S), ∑ u, bridge h x k t s u = backward h x k t s
Uses 4 · Used by 2
Statement usesHidden Markov model · Backward variables of a hidden Markov model · Bridge weights of a hidden Markov model
Proof usesFront decomposition of the bridge weights
Used byPairwise forward-backward · Forward-backward identity

TheoremPaths through two fixed states#✓fully proved

For a hidden Markov model with a finite set of states \(S\) and weights in a semiring, observations \(x_0, x_1, \dots\), all \(k, t \in \mathbb{N}\) and states \(s, u \in S\), the sum of the path weights \(p_{t+k}(z)\) over all state paths \(z = (z_0, \dots, z_{t+k})\) in \(S\) with \(z_t = s\) and \(z_{t+k} = u\) equals \(\alpha_t(s)\, b_{k,t}(s, u)\). Here \(p_{t+k}(z)\) is the joint weight of the path \(z\) and the observations \(x_0, \dots, x_{t+k}\), \(\alpha_t(s)\) is the forward variable and \(b_{k,t}(s, u)\) is the bridge weight from state \(s\) at time \(t\) to state \(u\) at time \(t + k\).

theorem sum_pathProb_ite_ite [DecidableEq S] : ∀ (k t : ℕ) (s u : S),
    ∑ z : Fin (t + k + 1) → S,
      (if z ⟨t, by omega⟩ = s ∧ z (Fin.last (t + k)) = u then pathProb h x (t + k) z else 0) =
      forward h x t s * bridge h x k t s u
Uses 5 · Used by 1
Statement usesHidden Markov model · Bridge weights of a hidden Markov model · Forward variables of a hidden Markov model · Joint weight of a state path and the observations
Proof usesThe forward variables are path sums
Used byForward-backward identity

TheoremForward-backward identity#✓fully proved

For a hidden Markov model with a finite set of states \(S\) and weights in a semiring, observations \(x_0, x_1, \dots\), times \(t, k \in \mathbb{N}\) and a state \(s \in S\), the joint weight of the observations \(x_0, \dots, x_{t+k}\) and the state \(s\) at time \(t\) equals \(\alpha_t(s)\,\beta_{k,t}(s)\), the forward variable \(\alpha_t(s)\) (the weight of \(x_0, \dots, x_t\) with the state at time \(t\) equal to \(s\)) times the backward variable \(\beta_{k,t}(s)\) (the weight of \(x_{t+1}, \dots, x_{t+k}\) given the state \(s\) at time \(t\)).

theorem stateMarg_eq [DecidableEq S] (t k : ℕ) (s : S) :
    stateMarg h x t k s = forward h x t s * backward h x k t s
Uses 8 · Used by 4
Statement usesHidden Markov model · Backward variables of a hidden Markov model · Forward variables of a hidden Markov model · Joint weight of the observations and a state
Proof usesBridge weights of a hidden Markov model · Joint weight of a state path and the observations · Bridge weights sum to the backward variable · Paths through two fixed states
Used byThe expected emissions from forward-backward · The expected starts from forward-backward · The likelihood from the forward and backward variables · Forward-backward smoothing is a joint-to-likelihood ratio

TheoremThe likelihood from the forward and backward variables#✓fully proved

Let \(h\) be a hidden Markov model with finite state set \(S\) and weights in a semiring, and let \(x_0, x_1, \dots\) be observations. Write \(\alpha_t(s)\) for the forward variable (the weight of \(x_0, \dots, x_t\) with the state at time \(t\) equal to \(s\)) and \(\beta_k(t, s)\) for the backward variable. Then for all \(t, k \in \mathbb{N}\), the likelihood of \(x_0, \dots, x_{t+k}\) equals

\[\sum_{s \in S} \alpha_t(s)\, \beta_k(t, s).\]
theorem likelihood_eq_sum_forward_mul_backward (t k : ℕ) :
    likelihood h x (t + k) = ∑ s, forward h x t s * backward h x k t s
Uses 7 · Used by 1
Statement usesHidden Markov model · Backward variables of a hidden Markov model · Forward variables of a hidden Markov model · Likelihood of the observations
Proof usesJoint weight of a state path and the observations · Joint weight of the observations and a state · Forward-backward identity
Used bySmoothed weights sum to one

DefinitionSmoothed state weights#✓fully proved

For a hidden Markov model with a finite set of states \(S\) and weights in a semifield \(K\), observations \(x_0, x_1, \dots\), times \(t, k \in \mathbb{N}\) and a state \(s \in S\), the smoothed weight of \(s\) at time \(t\) is

\[\gamma_{t,k}(s) = \frac{\alpha_t(s)\,\beta_{k,t}(s)}{L_{t+k}},\]

where \(\alpha_t(s)\) is the forward variable, \(\beta_{k,t}(s)\) is the backward variable (the weight of \(x_{t+1}, \dots, x_{t+k}\) given the state \(s\) at time \(t\)) and \(L_{t+k}\) is the likelihood of \(x_0, \dots, x_{t+k}\). Division is that of \(K\), so \(\gamma_{t,k}(s) = 0\) when \(L_{t+k} = 0\).

For nonnegative weights with stochastic rows and a positive likelihood this is the smoothing posterior \(P(z_t = s \mid x_0, \dots, x_{t+k})\) that the hidden state \(z_t\) at time \(t\) is \(s\); for general semifield weights it is only this ratio.

def smoothed (t k : ℕ) (s : S) : K :=
  forward g x t s * backward g x k t s / likelihood g x (t + k)
Uses 4 · Used by 8
Statement usesHidden Markov model · Backward variables of a hidden Markov model · Forward variables of a hidden Markov model · Likelihood of the observations
Used byThe expected number of correct states is a sum of posteriors · Posterior decoding maximizes the expected number of correctly decoded states · Posterior decoding · Forward-backward smoothing is a joint-to-likelihood ratio · Smoothed posterior as a sum over state paths · Posterior path maximizes the posterior at each time · Smoothing weights are nonnegative · Smoothed weights sum to one

TheoremForward-backward smoothing is a joint-to-likelihood ratio#✓fully proved

Let \(g\) be a hidden Markov model with finite state set \(S\) and weights in a semifield, and let \(x_0, x_1, \dots\) be observations. For all \(t, k \in \mathbb{N}\) and \(s \in S\), the smoothing weight \(\alpha_t(s)\, \beta_k(t, s) / L_{t+k}\), where \(\alpha\) and \(\beta\) are the forward and backward variables and \(L_{t+k}\) is the likelihood of \(x_0, \dots, x_{t+k}\), equals the joint weight of \(x_0, \dots, x_{t+k}\) and the state \(s\) at time \(t\), divided by \(L_{t+k}\).

When the weights are probabilities and the likelihood is positive, this ratio is the conditional state marginal.

theorem smoothed_eq [DecidableEq S] (t k : ℕ) (s : S) :
    smoothed x g t k s = stateMarg g x t k s / likelihood g x (t + k)
Uses 7 · Used by 2
Statement usesHidden Markov model · Likelihood of the observations · Smoothed state weights · Joint weight of the observations and a state
Proof usesBackward variables of a hidden Markov model · Forward variables of a hidden Markov model · Forward-backward identity
Used bySmoothed posterior as a sum over state paths · Smoothing weights are nonnegative

TheoremSmoothed weights sum to one#✓fully proved

For a hidden Markov model with a finite set of states \(S\) and weights in a semifield, observations \(x_0, x_1, \dots\) and times \(t, k \in \mathbb{N}\), if the likelihood \(L_{t+k}\) of \(x_0, \dots, x_{t+k}\) is nonzero, then the smoothed weights \(\gamma_{t,k}(s) = \alpha_t(s)\,\beta_{k,t}(s) / L_{t+k}\), with \(\alpha\) the forward and \(\beta\) the backward variables, sum to \(1\) over all states \(s \in S\).

theorem sum_smoothed (t k : ℕ) (hL : likelihood g x (t + k) ≠ 0) :
    ∑ s, smoothed x g t k s = 1
Uses 6
Statement usesHidden Markov model · Likelihood of the observations · Smoothed state weights
Proof usesBackward variables of a hidden Markov model · Forward variables of a hidden Markov model · The likelihood from the forward and backward variables

TheoremSmoothing weights are nonnegative#✓fully proved

Let \(g\) be a hidden Markov model with finite state set \(S\) whose initial, transition and emission weights are nonnegative elements of a linearly ordered semifield \(K\), and let \(x_0, x_1, \dots\) be observations. For all \(t, k \in \mathbb{N}\) and \(s \in S\), the smoothing weight \(\alpha_t(s)\, \beta_k(t, s) / L_{t+k}\) is nonnegative, where \(\alpha\) and \(\beta\) are the forward and backward variables and \(L_{t+k}\) is the likelihood of \(x_0, \dots, x_{t+k}\).

Since the smoothing weights at each time sum to one when the likelihood is nonzero, with a positive likelihood they form a probability distribution over the states.

theorem smoothed_nonneg [LinearOrder K] [IsStrictOrderedRing K]
    (hn : g.Nonneg) (t k : ℕ) (s : S) : 0 ≤ smoothed x g t k s
Uses 7
Statement usesHidden Markov model · Hidden Markov models with nonnegative weights · Smoothed state weights
Proof usesLikelihood of the observations · Joint weight of a state path and the observations · Forward-backward smoothing is a joint-to-likelihood ratio · Joint weight of the observations and a state

DefinitionOne step of the tabulated backward algorithm#✓fully proved

For a hidden Markov model \(g\) with states \(\{0, \dots, n - 1\}\), transition weights \(a\) and emission weights \(b\) in a semiring \(R\), an observation sequence \(x_0, x_1, \dots\), a vector \(v \in R^n\) and a time \(t\), this is the vector in \(R^n\) whose entry at state \(s\) is \(\sum_{s'} a(s, s')\, b(s', x_{t+1})\, v_{s'}\).

def backwardStep (g : HMM (Fin n) O R) (v : Vector R n) (t : ℕ) : Vector R n :=
  Vector.ofFn fun s => ∑ s', g.trans s s' * g.emit s' (x (t + 1)) * v[s']
Uses 1 · Used by 1
Statement usesHidden Markov model
Used byThe tabulated backward algorithm

DefinitionThe tabulated backward algorithm#✓fully proved

For a hidden Markov model \(g\) with states \(\{0, \dots, n - 1\}\), transition weights \(a\) and emission weights \(b\) in a semiring \(R\), and an observation sequence \(x_0, x_1, \dots\), the tables \(\beta^{(k)}_t \in R^n\) for \(k, t \in \mathbb{N}\) are defined by recursion on \(k\): \(\beta^{(0)}_t\) is the all-ones vector, and \(\beta^{(k+1)}_t\) is one backward step at time \(t\) applied to \(\beta^{(k)}_{t+1}\), that is, its entry at state \(s\) is \(\sum_{s'} a(s, s')\, b(s', x_{t+1})\, \beta^{(k)}_{t+1}(s')\).

The entries of \(\beta^{(k)}_t\) are the backward variables; each step takes \(O(n^2)\) operations.

def backwardTab (g : HMM (Fin n) O R) : ℕ → ℕ → Vector R n
  | 0, _ => Vector.replicate n 1
  | k + 1, t => backwardStep x g (backwardTab g k (t + 1)) t
Uses 2 · Used by 1
Statement usesHidden Markov model · One step of the tabulated backward algorithm
Used byTabulated forward-backward smoothing

DefinitionSmoothing step on tables#✓fully proved

For a semifield \(K\), vectors \(a, b \in K^n\) and \(L \in K\), this is the vector in \(K^n\) whose entry at \(s\) is \(a_s b_s / L\).

It combines the forward and backward tables into the smoothing weights.

def smoothStep {K : Type*} [Semifield K] (a b : Vector K n) (L : K) : Vector K n :=
  Vector.ofFn fun s => a[s] * b[s] / L
Used by 1
Used byTabulated forward-backward smoothing

DefinitionTabulated forward-backward smoothing#✓fully proved

Let \(g\) be a hidden Markov model with states \(\{0, \dots, n - 1\}\) and weights in a semifield \(K\), and let \(x_0, x_1, \dots\) be observations. For \(t, k \in \mathbb{N}\), this is the vector in \(K^n\) whose entry at state \(s\) is \(\alpha_t(s)\, \beta_k(t, s) / L_{t+k}\), where \(\alpha_t\) is the tabulated forward vector at time \(t\), \(\beta_k(t, \cdot)\) is the tabulated backward vector for \(k\) steps from time \(t\), and \(L_{t+k}\) is the tabulated likelihood of \(x_0, \dots, x_{t+k}\).

Its entries are the smoothing weights of all states at time \(t\), computed in \(O((t + k) n^2)\) operations.

def smoothedTab {K : Type*} [Semifield K] (g : HMM (Fin n) O K) (t k : ℕ) : Vector K n :=
  smoothStep (forwardTab x g t) (backwardTab x g k t) (likelihoodTab x g (t + k))
Uses 5
Statement usesHidden Markov model · The tabulated backward algorithm · Tabulated forward algorithm · Tabulated likelihood of a hidden Markov model · Smoothing step on tables

DefinitionPosterior decoding#✓fully proved

At each time t ≤ T, a state of largest posterior smoothed x g t (T - t) (the first one, via argmaxFin).

def posteriorPath [NeZero n] (T : ℕ) : Fin (T + 1) → Fin n :=
  fun t => argmaxFin fun s => smoothed x g t (T - t) s
Uses 3 · Used by 2
Statement usesHidden Markov model · First maximizer of a function on a finite range · Smoothed state weights
Used byPosterior decoding maximizes the expected number of correctly decoded states · Posterior path maximizes the posterior at each time

TheoremPosterior path maximizes the posterior at each time#✓fully proved

The posterior path picks a state of largest posterior at each time.

theorem smoothed_le_posteriorPath [NeZero n] (T : ℕ) (t : Fin (T + 1)) (s : Fin n) :
    smoothed x g t (T - t) s ≤ smoothed x g t (T - t) (posteriorPath x g T t)
Uses 4 · Used by 1
Statement usesHidden Markov model · Posterior decoding · Smoothed state weights
Proof usesFirst maximizer of a function on a finite range
Used byPosterior decoding maximizes the expected number of correctly decoded states

TheoremSmoothed posterior as a sum over state paths#✓fully proved

The posterior of state s at time t ≤ T, as a sum over the paths of length T + 1: the total weight of the paths through s at time t over the likelihood.

theorem smoothed_eq_sum_pathProb (T : ℕ) (t : Fin (T + 1)) (s : Fin n) :
    smoothed x g t (T - t) s =
      (∑ w : Fin (T + 1) → Fin n, if w t = s then pathProb g x T w else 0) /
        likelihood g x T
Uses 6 · Used by 1
Statement usesHidden Markov model · Likelihood of the observations · Joint weight of a state path and the observations · Smoothed state weights
Proof usesForward-backward smoothing is a joint-to-likelihood ratio · Joint weight of the observations and a state
Used byThe expected number of correct states is a sum of posteriors

DefinitionPosterior expected number of correctly decoded states#✓fully proved

The posterior expected number of correctly decoded states of a path z: the sum over all state paths w of pathProb w / likelihood times the number of times t ≤ T with w t = z t. When the weights are probabilities and the likelihood is positive, this is the expectation under the posterior law of the path; for likelihood 0 it is 0 (x / 0 = 0), as is every posterior smoothed.

def expectedCorrect (T : ℕ) (z : Fin (T + 1) → Fin n) : K :=
  ∑ w : Fin (T + 1) → Fin n,
    pathProb g x T w / likelihood g x T * ((Finset.univ.filter fun t => w t = z t).card : K)
Uses 3 · Used by 2
Statement usesHidden Markov model · Likelihood of the observations · Joint weight of a state path and the observations
Used byThe expected number of correct states is a sum of posteriors · Posterior decoding maximizes the expected number of correctly decoded states

TheoremThe expected number of correct states is a sum of posteriors#✓fully proved

For every path z, the posterior expected number of times t ≤ T with w t = z t is the sum over t of the posterior of z t at time t.

theorem expectedCorrect_eq_sum_smoothed (T : ℕ) (z : Fin (T + 1) → Fin n) :
    expectedCorrect x g T z = ∑ t : Fin (T + 1), smoothed x g t (T - t) (z t)
Uses 6 · Used by 1
Statement usesHidden Markov model · Posterior expected number of correctly decoded states · Smoothed state weights
Proof usesLikelihood of the observations · Joint weight of a state path and the observations · Smoothed posterior as a sum over state paths
Used byPosterior decoding maximizes the expected number of correctly decoded states

TheoremPosterior decoding maximizes the expected number of correctly decoded states#✓fully proved

Posterior decoding maximizes the expected number of correctly decoded states when addition preserves the order.

theorem expectedCorrect_le_posteriorPath [AddLeftMono K] [NeZero n]
    (T : ℕ) (z : Fin (T + 1) → Fin n) :
    expectedCorrect x g T z ≤ expectedCorrect x g T (posteriorPath x g T)
Uses 6
Statement usesHidden Markov model · Posterior expected number of correctly decoded states · Posterior decoding
Proof usesThe expected number of correct states is a sum of posteriors · Smoothed state weights · Posterior path maximizes the posterior at each time
46 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.