Skip to content

Expectation–maximization algorithm

16 fully proved

Gibbs' inequality

DefinitionProbability distributions on a finite latent space#✓fully proved

A function \(q : Z \to \mathbb{R}\) on a finite set \(Z\) is a probability distribution when \(q(z) \ge 0\) for every \(z \in Z\) and \(\sum_{z \in Z} q(z) = 1\).

def IsDist (q : Z → ℝ) : Prop := (∀ z, 0 ≤ q z) ∧ ∑ z, q z = 1
Used by 24

TheoremGibbs' inequality (evidence lower bound form)#✓fully proved

Let \(Z\) be a finite set, let \(p : Z \to \mathbb{R}\) satisfy \(p(z) > 0\) for all \(z\), and let \(q\) be a probability distribution on \(Z\). Then \(\sum_{z \in Z} q(z) (\log p(z) - \log q(z)) \le \log \sum_{z \in Z} p(z)\).

This is the log-sum inequality with \(\sum_{z} q(z) = 1\); terms with \(q(z) = 0\) contribute \(0\).

theorem sum_mul_log_sub_le {p q : Z → ℝ} (hp : ∀ z, 0 < p z) (hq : IsDist q) :
    ∑ z, q z * (log (p z) - log (q z)) ≤ log (∑ z, p z)
Uses 2 · Used by 9

TheoremEquality case of Gibbs' inequality#✓fully proved

Let \(Z\) be a finite nonempty set, let \(p : Z \to \mathbb{R}\) satisfy \(p(z) > 0\) for all \(z\), and write \(P = \sum_{z \in Z} p(z)\). Then

\[\sum_{z \in Z} \frac{p(z)}{P} \left(\log p(z) - \log \frac{p(z)}{P}\right) = \log P,\]

that is, the bound of Gibbs' inequality is attained at the distribution \(q = p / P\).

theorem sum_div_mul_log_sub {p : Z → ℝ} (hp : ∀ z, 0 < p z) [Nonempty Z] :
    ∑ z, p z / (∑ z', p z') * (log (p z) - log (p z / ∑ z', p z')) = log (∑ z, p z)
Used by 3

The model

DefinitionMarginal of a latent-variable model#✓fully proved

For a joint model \(p\) assigning a real number \(p_\theta(x, z)\) to each parameter \(\theta\), observation \(x\) and latent value \(z\) in a finite latent space \(Z\), the marginal is \(p_\theta(x) = \sum_{z \in Z} p_\theta(x, z)\).

def marginal (p : Θ → X → Z → ℝ) (θ : Θ) (x : X) : ℝ := ∑ z, p θ x z
Used by 29

DefinitionLog-likelihood of a latent-variable model#✓fully proved

For a joint model \(p\) with finite latent space \(Z\) and data \(x_0, \dots, x_{N-1}\), the log-likelihood at the parameter \(\theta\) is \(\ell(\theta) = \sum_{n < N} \log p_\theta(x_n)\), where \(p_\theta(x) = \sum_{z \in Z} p_\theta(x, z)\) is the marginal.

noncomputable def logLik (p : Θ → X → Z → ℝ) (xs : Fin N → X) (θ : Θ) : ℝ :=
  ∑ n, log (marginal p θ (xs n))
Uses 1 · Used by 23

DefinitionPosterior of a latent-variable model#✓fully proved

For a joint model \(p\) with finite latent space \(Z\), the posterior of the latent value \(z\) given the observation \(x\) at the parameter \(\theta\) is \(p_\theta(z \mid x) = p_\theta(x, z) / p_\theta(x)\), where \(p_\theta(x) = \sum_{z' \in Z} p_\theta(x, z')\) is the marginal (the quotient is read as \(0\) when the marginal is \(0\)). Computing it is the E-step of expectation-maximization.

noncomputable def posterior (p : Θ → X → Z → ℝ) (θ : Θ) (x : X) (z : Z) : ℝ :=
  p θ x z / marginal p θ x
Uses 1 · Used by 35
Used byThe ChromHMM update maximizes Q(· | θ) · The ChromHMM update is a valid parameter · The M-step maximizes the EM objective · Expected letter counts in motif columns · Positivity of expected motif counts · The E-step in closed form · Decomposition of the admixture EM objective · Ancestry responsibility of an allele copy (E-step) · Admixture responsibilities sum to one · The M-step maximizes Q(· | w) · Expected number of genes in a constraint class · Positivity of the class masses · Class masses sum to the number of genes · The bound is tight at the posterior · The ELBO at the posterior is the EM objective plus the entropy · The EM objective · The EM inequality · Posteriors are probability distributions · Posterior entropy · Decomposition of the EM objective for the Bernoulli mixture · The EM objective of an isotropic Gaussian mixture splits by component · The EM objective of a full-covariance Gaussian mixture splits by component · The M-step of the Bernoulli mixture maximizes the EM objective · One EM step for the Bernoulli mixture · The EM step for isotropic Gaussian mixtures · EM step for the full-covariance Gaussian mixture · Responsibilities of a Bernoulli mixture · Responsibilities in an isotropic Gaussian mixture · Responsibilities of the full-covariance Gaussian mixture · Isotropic Gaussian mixtures: the weight update maximizes the weights term · The weight update maximizes the weights term of the full-covariance mixture · The Baum-Welch objective in terms of expected counts · The Baum-Welch update maximizes the EM objective · One Baum-Welch step · Posterior weight of a state path

DefinitionEvidence lower bound of latent distributions#✓fully proved

Let \(Z\) be a finite set, let \(p_\theta(x, z)\) be real numbers indexed by parameters \(\theta\), observations \(x\) and latent values \(z \in Z\), and let \(x_1, \dots, x_N\) be data. For a parameter \(\theta\) and functions \(q_1, \dots, q_N : Z \to \mathbb{R}\) (one latent distribution per data point), the evidence lower bound is \(\sum_{n=1}^N \sum_{z \in Z} q_n(z) \bigl(\log p_\theta(x_n, z) - \log q_n(z)\bigr)\).

noncomputable def elbo (p : Θ → X → Z → ℝ) (xs : Fin N → X) (θ : Θ) (q : Fin N → Z → ℝ) : ℝ :=
  ∑ n, ∑ z, q n z * (log (p θ (xs n) z) - log (q n z))
Used by 5

DefinitionThe EM objective#✓fully proved

Let \(Z\) be a finite set, let \(p_\theta(x, z)\) be real numbers indexed by parameters \(\theta\), observations \(x\) and latent values \(z \in Z\), let \(x_1, \dots, x_N\) be data, and write \(p_\theta(z \mid x) = p_\theta(x, z) / \sum_{z' \in Z} p_\theta(x, z')\) for the posterior. For parameters \(\theta'\) and \(\theta\), the EM objective is \(Q(\theta' \mid \theta) = \sum_{n=1}^N \sum_{z \in Z} p_\theta(z \mid x_n) \log p_{\theta'}(x_n, z)\) (maximized over \(\theta'\) in the M-step).

noncomputable def emQ (p : Θ → X → Z → ℝ) (xs : Fin N → X) (θ' θ : Θ) : ℝ :=
  ∑ n, ∑ z, posterior p θ (xs n) z * log (p θ' (xs n) z)
Uses 1 · Used by 19

DefinitionPosterior entropy#✓fully proved

For a joint model \(p\) with finite latent space \(Z\), data \(x_0, \dots, x_{N-1}\) and a parameter \(\theta\), the posterior entropy is \(-\sum_{n < N} \sum_{z \in Z} p_\theta(z \mid x_n) \log p_\theta(z \mid x_n)\), where \(p_\theta(z \mid x)\) is the posterior of \(z\) given \(x\).

noncomputable def postEntropy (p : Θ → X → Z → ℝ) (xs : Fin N → X) (θ : Θ) : ℝ :=
  -∑ n, ∑ z, posterior p θ (xs n) z * log (posterior p θ (xs n) z)
Uses 1 · Used by 2

TheoremPosteriors are probability distributions#✓fully proved

Let \(Z\) be a nonempty finite set and let \(p_\theta(x, z)\) be real numbers indexed by parameters \(\theta\), observations \(x\) and latent values \(z \in Z\), with \(p_\theta(x, z) > 0\) for all \(\theta\), \(x\), \(z\). For every parameter \(\theta\) and observation \(x\), the posterior \(z \mapsto p_\theta(x, z) / \sum_{z' \in Z} p_\theta(x, z')\) is a probability distribution on \(Z\): its values are nonnegative and sum to \(1\).

theorem isDist_posterior [Nonempty Z] (hp : ∀ θ x z, 0 < p θ x z) (θ : Θ) (x : X) :
    IsDist (posterior p θ x)
Uses 3 · Used by 13

TheoremThe evidence lower bound#✓fully proved

Let \(Z\) be a finite set, let \(p_\theta(x, z)\) be real numbers indexed by parameters \(\theta\), observations \(x\) and latent values \(z \in Z\), with \(p_\theta(x, z) > 0\) for all \(\theta\), \(x\), \(z\), and let \(x_1, \dots, x_N\) be data. For every parameter \(\theta\) and all probability distributions \(q_1, \dots, q_N\) on \(Z\),

\[ \sum_{n=1}^N \sum_{z \in Z} q_n(z) \bigl(\log p_\theta(x_n, z) - \log q_n(z)\bigr) \le \sum_{n=1}^N \log \sum_{z \in Z} p_\theta(x_n, z), \]

that is, the evidence lower bound of \(q_1, \dots, q_N\) at \(\theta\) is at most the log-likelihood of the data at \(\theta\). Terms with \(q_n(z) = 0\) count as \(0\).

theorem elbo_le_logLik (hp : ∀ θ x z, 0 < p θ x z) (xs : Fin N → X) (θ : Θ)
    {q : Fin N → Z → ℝ} (hq : ∀ n, IsDist (q n)) : elbo p xs θ q ≤ logLik p xs θ
Uses 5 · Used by 1

TheoremThe bound is tight at the posterior#✓fully proved

Let \(Z\) be a nonempty finite set, let \(p_\theta(x, z)\) be real numbers indexed by parameters \(\theta\), observations \(x\) and latent values \(z \in Z\), with \(p_\theta(x, z) > 0\) for all \(\theta\), \(x\), \(z\), and let \(x_1, \dots, x_N\) be data. For every parameter \(\theta\), the posteriors \(q_n(z) = p_\theta(z \mid x_n) = p_\theta(x_n, z) / \sum_{z' \in Z} p_\theta(x_n, z')\) satisfy

\[ \sum_{n=1}^N \sum_{z \in Z} q_n(z) \bigl(\log p_\theta(x_n, z) - \log q_n(z)\bigr) = \sum_{n=1}^N \log \sum_{z \in Z} p_\theta(x_n, z), \]

that is, the evidence lower bound at \(\theta\) of the posteriors equals the log-likelihood of the data at \(\theta\).

theorem elbo_posterior [Nonempty Z] (hp : ∀ θ x z, 0 < p θ x z) (xs : Fin N → X) (θ : Θ) :
    elbo p xs θ (fun n => posterior p θ (xs n)) = logLik p xs θ
Uses 5 · Used by 1

TheoremThe ELBO at the posterior is the EM objective plus the entropy#✓fully proved

Let \(Z\) be a finite set, let \(p_\theta(x, z)\) be real numbers indexed by parameters \(\theta\), observations \(x\) and latent values \(z \in Z\), let \(x_1, \dots, x_N\) be data, and write \(p_\theta(z \mid x) = p_\theta(x, z) / \sum_{z' \in Z} p_\theta(x, z')\) for the posterior, \(Q(\theta' \mid \theta) = \sum_{n=1}^N \sum_{z \in Z} p_\theta(z \mid x_n) \log p_{\theta'}(x_n, z)\) for the EM objective and \(H(\theta) = -\sum_{n=1}^N \sum_{z \in Z} p_\theta(z \mid x_n) \log p_\theta(z \mid x_n)\) for the entropy of the posteriors. For all parameters \(\theta'\) and \(\theta\), the evidence lower bound at \(\theta'\) of the posteriors \(q_n = p_\theta(\cdot \mid x_n)\) satisfies

\[ \sum_{n=1}^N \sum_{z \in Z} q_n(z) \bigl(\log p_{\theta'}(x_n, z) - \log q_n(z)\bigr) = Q(\theta' \mid \theta) + H(\theta), \]

that is, it splits as the EM objective \(Q(\theta' \mid \theta)\) plus the posterior entropy.

theorem elbo_posterior_eq (xs : Fin N → X) (θ' θ : Θ) :
    elbo p xs θ' (fun n => posterior p θ (xs n)) = emQ p xs θ' θ + postEntropy p xs θ
Uses 4 · Used by 1

TheoremThe EM inequality#✓fully proved

Let \(Z\) be a nonempty finite set, let \(p_\theta(x, z)\) be real numbers indexed by parameters \(\theta\), observations \(x\) and latent values \(z \in Z\), with \(p_\theta(x, z) > 0\) for all \(\theta\), \(x\), \(z\), and let \(x_1, \dots, x_N\) be data. Write \(p_\theta(z \mid x) = p_\theta(x, z) / \sum_{z' \in Z} p_\theta(x, z')\) for the posterior, \(Q(\theta' \mid \theta) = \sum_{n=1}^N \sum_{z \in Z} p_\theta(z \mid x_n) \log p_{\theta'}(x_n, z)\) for the EM objective and \(\ell(\theta) = \sum_{n=1}^N \log \sum_{z \in Z} p_\theta(x_n, z)\) for the log-likelihood. For all parameters \(\theta'\) and \(\theta\), \(Q(\theta' \mid \theta) - Q(\theta \mid \theta) \le \ell(\theta') - \ell(\theta)\): the log-likelihood gains at least as much as \(Q(\cdot \mid \theta)\).

theorem emQ_sub_le_logLik_sub [Nonempty Z] (hp : ∀ θ x z, 0 < p θ x z) (xs : Fin N → X)
    (θ' θ : Θ) : emQ p xs θ' θ - emQ p xs θ θ ≤ logLik p xs θ' - logLik p xs θ
Uses 9 · Used by 1

TheoremThe EM theorem#✓fully proved

Let \(Z\) be a nonempty finite set, let \(p_\theta(x, z)\) be real numbers indexed by parameters \(\theta\), observations \(x\) and latent values \(z \in Z\), with \(p_\theta(x, z) > 0\) for all \(\theta\), \(x\), \(z\), and let \(x_1, \dots, x_N\) be data. Write \(p_\theta(z \mid x) = p_\theta(x, z) / \sum_{z' \in Z} p_\theta(x, z')\) for the posterior, \(Q(\theta' \mid \theta) = \sum_{n=1}^N \sum_{z \in Z} p_\theta(z \mid x_n) \log p_{\theta'}(x_n, z)\) for the EM objective and \(\ell(\theta) = \sum_{n=1}^N \log \sum_{z \in Z} p_\theta(x_n, z)\) for the log-likelihood. For parameters \(\theta\) and \(\theta'\), if \(Q(\theta \mid \theta) \le Q(\theta' \mid \theta)\), then \(\ell(\theta) \le \ell(\theta')\): a step that does not decrease \(Q(\cdot \mid \theta)\) does not decrease the log-likelihood.

theorem logLik_le_of_emQ_le [Nonempty Z] (hp : ∀ θ x z, 0 < p θ x z) (xs : Fin N → X)
    {θ' θ : Θ} (h : emQ p xs θ θ ≤ emQ p xs θ' θ) : logLik p xs θ ≤ logLik p xs θ'
Uses 3 · Used by 8

TheoremEM iterates have monotone likelihood#✓fully proved

Let \(Z\) be a nonempty finite set, let \(p_\theta(x, z)\) be real numbers indexed by parameters \(\theta\), observations \(x\) and latent values \(z \in Z\), with \(p_\theta(x, z) > 0\) for all \(\theta\), \(x\), \(z\), and let \(x_1, \dots, x_N\) be data. Write \(p_\theta(z \mid x) = p_\theta(x, z) / \sum_{z' \in Z} p_\theta(x, z')\) for the posterior, \(Q(\theta' \mid \theta) = \sum_{n=1}^N \sum_{z \in Z} p_\theta(z \mid x_n) \log p_{\theta'}(x_n, z)\) for the EM objective and \(\ell(\theta) = \sum_{n=1}^N \log \sum_{z \in Z} p_\theta(x_n, z)\) for the log-likelihood. Let \(M\) be a map on parameters, with \(k\)-th iterate \(M^k\) (\(M^0\) the identity), such that \(Q(M\theta \mid \theta) \ge Q(\theta \mid \theta)\) for every \(\theta\) (in particular if \(M\theta\) maximizes \(Q(\cdot \mid \theta)\), or \(M\) is a generalized-EM step). Then for every \(\theta_0\) the sequence \(k \mapsto \ell(M^k \theta_0)\) is nondecreasing.

theorem logLik_iterate_monotone [Nonempty Z] (hp : ∀ θ x z, 0 < p θ x z) (xs : Fin N → X)
    {M : Θ → Θ} (hM : ∀ θ, emQ p xs θ θ ≤ emQ p xs (M θ) θ) (θ₀ : Θ) :
    Monotone fun k => logLik p xs (M^[k] θ₀)
Uses 3 · Used by 8

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.