Expectation–maximization algorithm
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
λ · Information content is nonnegative · Columns of the Boltzmann matrix are distributions · Target frequencies form a distribution on pairs · The relative entropy of the target frequencies · Background likelihoods form a distribution · Product site likelihoods form a distribution · The expected log-odds score is the total information content · The target score is positive · The evidence lower bound · Posteriors are probability distributions · Gibbs' inequality (evidence lower bound form) · The ELBO is the log evidence minus the KL divergence · Mean-field coordinate ascent never decreases the ELBO · The CAVI update maximizes the ELBO over the first factor · The CAVI update of the second factor does not decrease the ELBO · A sweep of coordinate ascent does not decrease the ELBO · The ELBO is a lower bound · ELBO of a product distribution · Gibbs' inequality · The KL divergence to the posterior is nonnegative · Isotropic Gaussian mixtures: the weight update maximizes the weights term · The weight update maximizes the weights term of the full-covariance mixture · The weighted log-likelihood is bounded by its value at the normalized countsTheoremGibbs' 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)
def IsDist (q : Z → ℝ) : Prop := (∀ z, 0 ≤ q z) ∧ ∑ z, q z = 1
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:68
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
that is, the bound of Gibbs' inequality is attained at the distribution \(q = p / P\).
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
Q(· | θ) · The ChromHMM update is a valid parameter · Positivity of expected motif counts · The E-step in closed form · The EM log-likelihood of the allele copies is the admixture log-likelihood · The marginal of an allele copy · Reference-allele probability is less than one · Positivity of the admixture responsibilities · Positivity of the class masses · The evidence lower bound · The bound is tight at the posterior · Posteriors are probability distributions · Log-likelihood of a latent-variable model · Posterior of a latent-variable model · The mean and variance updates maximize each component term · The mean and covariance updates maximize each component term · The M-step of the Bernoulli mixture maximizes the EM objective · The M-step for isotropic Gaussian mixtures 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 · Mixture density of an isotropic Gaussian mixture · The covariance update is positive definite · 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 update maximizes the EM objective · One Baum-Welch step · The EM marginal of an HMM is its likelihood · The Gaussian-mixture responsibilities are the common-variance responsibilitiesDefinitionLog-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))
def marginal (p : Θ → X → Z → ℝ) (θ : Θ) (x : X) : ℝ := ∑ z, p θ x z
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:105
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
def marginal (p : Θ → X → Z → ℝ) (θ : Θ) (x : X) : ℝ := ∑ z, p θ x z
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:105
Uses 1 · Used by 35
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 pathDefinitionEvidence 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)\).
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)
noncomputable def posterior (p : Θ → X → Z → ℝ) (θ : Θ) (x : X) (z : Z) : ℝ :=
p θ x z / marginal p θ x
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:112
Uses 1 · Used by 19
Q(· | θ) · The M-step maximizes the EM objective · The admixture log-likelihood is monotone along the iterates · The EM theorem for the admixture model · Decomposition of the admixture EM objective · The FRAPPE update maximizes Q(· | θ) · The M-step maximizes Q(· | w) · The ELBO at the posterior is the EM objective plus the entropy · The EM inequality · EM iterates have monotone likelihood · The EM theorem · 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 · The M-step for isotropic Gaussian mixtures maximizes the EM objective · The M-step of the full-covariance Gaussian mixture maximizes the EM objective · The Baum-Welch objective in terms of expected counts · The Baum-Welch update maximizes the EM objectiveDefinitionPosterior 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)
noncomputable def posterior (p : Θ → X → Z → ℝ) (θ : Θ) (x : X) (z : Z) : ℝ :=
p θ x z / marginal p θ x
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:112
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)
def IsDist (q : Z → ℝ) : Prop := (∀ z, 0 ≤ q z) ∧ ∑ z, q z = 1
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:68
noncomputable def posterior (p : Θ → X → Z → ℝ) (θ : Θ) (x : X) (z : Z) : ℝ :=
p θ x z / marginal p θ x
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:112
Uses 3 · Used by 13
Q(· | θ) · The ChromHMM update is a valid parameter · Admixture responsibilities sum to one · Class masses sum to the number of genes · The EM inequality · 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 · 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 update maximizes the EM objective · One Baum-Welch stepTheoremThe 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\),
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 θ
def IsDist (q : Z → ℝ) : Prop := (∀ z, 0 ≤ q z) ∧ ∑ z, q z = 1
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:68
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))
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:117
noncomputable def logLik (p : Θ → X → Z → ℝ) (xs : Fin N → X) (θ : Θ) : ℝ :=
∑ n, log (marginal p θ (xs n))
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:108
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
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 θ
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))
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:117
noncomputable def posterior (p : Θ → X → Z → ℝ) (θ : Θ) (x : X) (z : Z) : ℝ :=
p θ x z / marginal p θ x
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:112
noncomputable def logLik (p : Θ → X → Z → ℝ) (xs : Fin N → X) (θ : Θ) : ℝ :=
∑ n, log (marginal p θ (xs n))
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:108
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
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 θ
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))
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:117
noncomputable def posterior (p : Θ → X → Z → ℝ) (θ : Θ) (x : X) (z : Z) : ℝ :=
p θ x z / marginal p θ x
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:112
noncomputable def emQ (p : Θ → X → Z → ℝ) (xs : Fin N → X) (θ' θ : Θ) : ℝ :=
∑ n, ∑ z, posterior p θ (xs n) z * log (p θ' (xs n) z)
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:122
noncomputable def postEntropy (p : Θ → X → Z → ℝ) (xs : Fin N → X) (θ : Θ) : ℝ :=
-∑ n, ∑ z, posterior p θ (xs n) z * log (posterior p θ (xs n) z)
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:126
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 θ
noncomputable def emQ (p : Θ → X → Z → ℝ) (xs : Fin N → X) (θ' θ : Θ) : ℝ :=
∑ n, ∑ z, posterior p θ (xs n) z * log (p θ' (xs n) z)
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:122
noncomputable def logLik (p : Θ → X → Z → ℝ) (xs : Fin N → X) (θ : Θ) : ℝ :=
∑ n, log (marginal p θ (xs n))
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:108
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 θ'
noncomputable def emQ (p : Θ → X → Z → ℝ) (xs : Fin N → X) (θ' θ : Θ) : ℝ :=
∑ n, ∑ z, posterior p θ (xs n) z * log (p θ' (xs n) z)
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:122
noncomputable def logLik (p : Θ → X → Z → ℝ) (xs : Fin N → X) (θ : Θ) : ℝ :=
∑ n, log (marginal p θ (xs n))
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:108
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] θ₀)
noncomputable def emQ (p : Θ → X → Z → ℝ) (xs : Fin N → X) (θ' θ : Θ) : ℝ :=
∑ n, ∑ z, posterior p θ (xs n) z * log (p θ' (xs n) z)
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:122
noncomputable def logLik (p : Θ → X → Z → ℝ) (xs : Fin N → X) (θ : Θ) : ℝ :=
∑ n, log (marginal p θ (xs n))
CSLibExt/MachineLearning/LatentVariable/ExpectationMaximization.lean:108
Uses 3 · Used by 8
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.