Mixture models

TheoremThe weighted log-likelihood is bounded by its value at the normalized counts#✓fully proved

Let \(Z\) be a finite set, let \(c \colon Z \to \mathbb{R}\) be nonnegative counts with positive total \(C = \sum_{z \in Z} c_z > 0\), and let \(w \colon Z \to \mathbb{R}\) be positive weights with \(\sum_{z \in Z} w_z = 1\). Then \(\sum_{z \in Z} c_z \log w_z \le \sum_{z \in Z} c_z \log(c_z / C)\) (Gibbs' inequality).

When every count is positive the normalized counts \(c_z / C\) are themselves admissible weights, so they maximize.

theorem sum_mul_log_le_sum_mul_log_div {Z : Type*} [Fintype Z] {c w : Z → ℝ}
    (hc : ∀ z, 0 ≤ c z) (hC : 0 < ∑ z, c z) (hw : ∀ z, 0 < w z) (hsum : ∑ z, w z = 1) :
    ∑ z, c z * log (w z) ≤ ∑ z, c z * log (c z / ∑ z', c z')

Uses 2 · Used by 7

Proof usesProbability distributions on a finite latent space · Gibbs' inequality (evidence lower bound form)

Used byThe ChromHMM update maximizes Q(· | θ) · The update is an upper bound for the truncated objective · The M-step maximizes the EM objective · The FRAPPE update maximizes Q(· | θ) · The M-step maximizes Q(· | w) · The M-step of the Bernoulli mixture maximizes the EM objective · The Baum-Welch update maximizes the EM objective

DefinitionProduct Bernoulli probability mass function#✓fully proved

For a vector \(p \in \mathbb{R}^d\) of success probabilities and a binary vector \(x \in \{0, 1\}^d\), the probability of \(x\) under the product of \(d\) independent Bernoulli distributions with parameters \(p_1, \dots, p_d\) is

\[\prod_{j=1}^{d} p_j^{x_j} (1 - p_j)^{1 - x_j},\]

that is, the product over \(j\) of \(p_j\) when \(x_j = 1\) and of \(1 - p_j\) when \(x_j = 0\).

noncomputable def bernPMF (p : Fin d → ℝ) (x : Fin d → Bool) : ℝ :=
  ∏ j, if x j then p j else 1 - p j

Used by 11

Used byProduct of Bernoulli distributions sums to one · Expected product-Bernoulli log-likelihood splits over marks · The factored update maximizes the expected log-likelihood · HMM of ChromHMM parameters · Valid ChromHMM parameters give a valid HMM · Decomposition of the EM objective for the Bernoulli mixture · The M-step of the Bernoulli mixture maximizes the EM objective · One EM step for the Bernoulli mixture · Joint distribution of the Bernoulli mixture · The log-likelihood is monotone along the EM iterates of a Bernoulli mixture · Each EM step for the Bernoulli mixture does not decrease the log-likelihood

StructureParameters of a Bernoulli mixture#✓fully proved

The parameters of a mixture of \(K\) products of \(d\) Bernoulli distributions are real mixing weights \(\pi_k\) for \(k < K\) and real success probabilities \(p_{kj}\) for every component \(k < K\) and coordinate \(j < d\). No constraint is imposed on these numbers here; the admissible ones are the valid parameters.

structure Params (d K : ℕ) where
  /-- The mixing weights. -/
  weight : Fin K → ℝ
  /-- The success probability of each coordinate in each component. -/
  prob : Fin K → Fin d → ℝ

Used by 9

Used byDecomposition of the EM objective for the Bernoulli mixture · The M-step of the Bernoulli mixture maximizes the EM objective · One EM step for the Bernoulli mixture · Joint distribution of the Bernoulli mixture · The log-likelihood is monotone along the EM iterates of a Bernoulli mixture · Each EM step for the Bernoulli mixture does not decrease the log-likelihood · The M-step of the Bernoulli mixture · Valid parameters of a Bernoulli mixture · The parameter space of a Bernoulli mixture

StructureValid parameters of a Bernoulli mixture#✓fully proved

Parameters of a mixture of \(K\) products of \(d\) Bernoulli distributions, with mixing weights \(\pi_k\) and success probabilities \(p_{kj}\), are valid when \(\pi_k > 0\) for every \(k < K\), \(\sum_{k < K} \pi_k = 1\), and \(0 < p_{kj} < 1\) for every \(k < K\) and \(j < d\).

structure Params.Valid (θ : Params d K) : Prop where
  weight_pos : ∀ k, 0 < θ.weight k
  weight_sum : ∑ k, θ.weight k = 1
  prob_pos : ∀ k j, 0 < θ.prob k j
  prob_lt_one : ∀ k j, θ.prob k j < 1

Uses 1 · Used by 7

Statement usesParameters of a Bernoulli mixture

Used byDecomposition of the EM objective for the Bernoulli mixture · The M-step of the Bernoulli mixture maximizes the EM objective · One EM step for the Bernoulli mixture · Joint distribution of the Bernoulli mixture · The log-likelihood is monotone along the EM iterates of a Bernoulli mixture · Each EM step for the Bernoulli mixture does not decrease the log-likelihood · The parameter space of a Bernoulli mixture

AbbreviationThe parameter space of a Bernoulli mixture#✓fully proved

The parameter space of EM for a mixture of \(K\) products of \(d\) Bernoulli distributions is the set of valid parameters: mixing weights \(\pi_k\) and success probabilities \(p_{kj}\) (\(k < K\), \(j < d\)) with every \(\pi_k > 0\), \(\sum_{k < K} \pi_k = 1\) and every \(p_{kj}\) strictly between \(0\) and \(1\).

abbrev ValidParams (d K : ℕ) := {θ : Params d K // θ.Valid}

Uses 2 · Used by 11

Statement usesParameters of a Bernoulli mixture · Valid parameters of a Bernoulli mixture

Used byDecomposition of the EM objective for the Bernoulli mixture · The M-step of the Bernoulli mixture maximizes the EM objective · One EM step for the Bernoulli mixture · Joint distribution of the Bernoulli mixture · The log-likelihood is monotone along the EM iterates of a Bernoulli mixture · Each EM step for the Bernoulli mixture does not decrease the log-likelihood · The M-step of the Bernoulli mixture · Effective number of points of a Bernoulli-mixture component · Responsibility-weighted count of ones · Responsibilities of a Bernoulli mixture · Responsibility-weighted count of zeros

DefinitionJoint distribution of the Bernoulli mixture#✓fully proved

For valid parameters \(\theta\) of a mixture of \(K\) products of \(d\) Bernoulli distributions, with mixing weights \(\pi_k\) and success probabilities \(p_{kj}\), the joint probability of a binary vector \(x \in \{0, 1\}^d\) and a component \(k\) is

\[p_\theta(x, k) = \pi_k \prod_{j=1}^{d} p_{kj}^{x_j} (1 - p_{kj})^{1 - x_j},\]

that is, \(\pi_k\) times the product Bernoulli probability of \(x\) with parameters \(p_{k1}, \dots, p_{kd}\).

noncomputable def joint (θ : ValidParams d K) (x : Fin d → Bool) (k : Fin K) : ℝ :=
  θ.1.weight k * bernPMF (θ.1.prob k) x

Uses 4 · Used by 6

Statement usesParameters of a Bernoulli mixture · Valid parameters of a Bernoulli mixture · The parameter space of a Bernoulli mixture · Product Bernoulli probability mass function

Used byDecomposition of the EM objective for the Bernoulli mixture · The M-step of the Bernoulli mixture maximizes the EM objective · One EM step for the Bernoulli mixture · The log-likelihood is monotone along the EM iterates of a Bernoulli mixture · Each EM step for the Bernoulli mixture does not decrease the log-likelihood · Responsibilities of a Bernoulli mixture

DefinitionResponsibilities of a Bernoulli mixture#✓fully proved

Let \(\theta\) be valid parameters of a mixture of \(K\) products of \(d\) Bernoulli distributions, and write \(p_\theta(x, k)\) for the joint probability of a binary vector \(x \in \{0,1\}^d\) and a component \(k < K\) under \(\theta\). The responsibility of \(k\) for \(x\) is the posterior probability \(r_k(x) = p_\theta(x, k) / \sum_{k' < K} p_\theta(x, k')\). Computing it is the E-step of EM.

noncomputable def resp (θ : ValidParams d K) (x : Fin d → Bool) (k : Fin K) : ℝ :=
  posterior joint θ x k

Uses 3 · Used by 6

Statement usesThe parameter space of a Bernoulli mixture · Joint distribution of the Bernoulli mixture · Posterior of a latent-variable model

Used byDecomposition of the EM objective for the Bernoulli mixture · The M-step of the Bernoulli mixture maximizes the EM objective · One EM step for the Bernoulli mixture · Effective number of points of a Bernoulli-mixture component · Responsibility-weighted count of ones · Responsibility-weighted count of zeros

DefinitionEffective number of points of a Bernoulli-mixture component#✓fully proved

For data \(x_1, \dots, x_N \in \{0, 1\}^d\) and valid parameters \(\theta\) of a mixture of \(K\) products of \(d\) Bernoulli distributions, the effective number of points of component \(k\) is \(N_k = \sum_{n=1}^{N} r_{nk}\), where \(r_{nk}\) is the posterior probability (responsibility) of component \(k\) given \(x_n\) under \(\theta\).

noncomputable def mass (θ : ValidParams d K) (k : Fin K) : ℝ := ∑ n, resp θ (xs n) k

Uses 2 · Used by 4

Statement usesThe parameter space of a Bernoulli mixture · Responsibilities of a Bernoulli mixture

Used byDecomposition of the EM objective for the Bernoulli mixture · The M-step of the Bernoulli mixture maximizes the EM objective · One EM step for the Bernoulli mixture · The M-step of the Bernoulli mixture

DefinitionResponsibility-weighted count of ones#✓fully proved

For data \(x_1, \dots, x_N \in \{0, 1\}^d\), valid parameters \(\theta\) of a mixture of \(K\) products of \(d\) Bernoulli distributions, a component \(k\) and a coordinate \(j\), this is the sum \(\sum_{n \,:\, x_{nj} = 1} r_{nk}\), over the points whose \(j\)-th coordinate is \(1\), of the posterior probability \(r_{nk}\) of component \(k\) given \(x_n\) under \(\theta\).

noncomputable def ones (θ : ValidParams d K) (k : Fin K) (j : Fin d) : ℝ :=
  ∑ n, if xs n j then resp θ (xs n) k else 0

Uses 2 · Used by 4

Statement usesThe parameter space of a Bernoulli mixture · Responsibilities of a Bernoulli mixture

Used byDecomposition of the EM objective for the Bernoulli mixture · The M-step of the Bernoulli mixture maximizes the EM objective · One EM step for the Bernoulli mixture · The M-step of the Bernoulli mixture

DefinitionResponsibility-weighted count of zeros#✓fully proved

Let \(\theta\) be valid parameters of a mixture of \(K\) products of \(d\) Bernoulli distributions, let \(x_0, \dots, x_{N-1} \in \{0,1\}^d\) be data, and let \(k < K\) be a component and \(j < d\) a coordinate. Write \(x_{nj}\) for the \(j\)-th coordinate of \(x_n\) and \(r_k(x_n)\) for the responsibility of component \(k\) for \(x_n\) under \(\theta\). The weighted count is \(\sum_{n < N,\ x_{nj} = 0} r_k(x_n)\), the sum of the responsibilities over the points whose \(j\)-th coordinate is \(0\).

noncomputable def zeros (θ : ValidParams d K) (k : Fin K) (j : Fin d) : ℝ :=
  ∑ n, if xs n j then 0 else resp θ (xs n) k

Uses 2 · Used by 3

Statement usesThe parameter space of a Bernoulli mixture · Responsibilities of a Bernoulli mixture

Used byDecomposition of the EM objective for the Bernoulli mixture · The M-step of the Bernoulli mixture maximizes the EM objective · One EM step for the Bernoulli mixture

DefinitionThe M-step of the Bernoulli mixture#✓fully proved

Let \(x_1, \dots, x_N \in \{0, 1\}^d\) be data and \(\theta\) valid parameters of a mixture of \(K\) products of \(d\) Bernoulli distributions. With \(r_{nk}\) the posterior probability of component \(k\) given \(x_n\) under \(\theta\), \(N_k = \sum_n r_{nk}\) and \(A_{kj} = \sum_n r_{nk} x_{nj}\), the M-step returns the parameters with mixing weights \(\pi'_k = N_k / N\) and success probabilities \(p'_{kj} = A_{kj} / N_k\), where a quotient by \(0\) is read as \(0\). These parameters need not be valid.

noncomputable def mStep (θ : ValidParams d K) : Params d K where
  weight k := mass xs θ k / N
  prob k j := ones xs θ k j / mass xs θ k

Uses 4 · Used by 1

Statement usesParameters of a Bernoulli mixture · The parameter space of a Bernoulli mixture · Effective number of points of a Bernoulli-mixture component · Responsibility-weighted count of ones

Used byOne EM step for the Bernoulli mixture

StructureRich data for a Bernoulli mixture#✓fully proved

Data \(x_0, \dots, x_{N-1} \in \{0,1\}^d\) are rich when \(N > 0\) and, for every coordinate \(j < d\), some \(x_n\) has \(j\)-th coordinate \(1\) and some \(x_m\) has \(j\)-th coordinate \(0\). These are the data on which the M-step yields valid parameters.

structure Rich (xs : Fin N → Fin d → Bool) : Prop where
  pos : 0 < N
  both : ∀ j, (∃ n, xs n j = true) ∧ ∃ n, xs n j = false

Used by 4

Used byThe M-step of the Bernoulli mixture maximizes the EM objective · One EM step for the Bernoulli mixture · The log-likelihood is monotone along the EM iterates of a Bernoulli mixture · Each EM step for the Bernoulli mixture does not decrease the log-likelihood

DefinitionOne EM step for the Bernoulli mixture#✓fully proved

Let \(x_1, \dots, x_N \in \{0, 1\}^d\) be data with \(N \ge 1\) in which every coordinate takes both values. For valid parameters \(\theta\) of a mixture of \(K\) products of \(d\) Bernoulli distributions, the EM step maps \(\theta\) to the parameters with mixing weights \(\pi'_k = N_k / N\) and success probabilities \(p'_{kj} = A_{kj} / N_k\), where \(r_{nk}\) is the posterior probability of component \(k\) given \(x_n\) under \(\theta\), \(N_k = \sum_n r_{nk}\), and \(A_{kj}\) is the sum of \(r_{nk}\) over the points with \(x_{nj} = 1\). On such data these parameters are again valid.

noncomputable def emStep (hx : Rich xs) (θ : ValidParams d K) : ValidParams d K :=
  ⟨mStep xs θ, mStep_valid hx θ⟩

Uses 14 · Used by 3

Statement usesParameters of a Bernoulli mixture · Valid parameters of a Bernoulli mixture · Rich data for a Bernoulli mixture · The parameter space of a Bernoulli mixture · Product Bernoulli probability mass function · Joint distribution of the Bernoulli mixture · The M-step of the Bernoulli mixture · Effective number of points of a Bernoulli-mixture component · Responsibility-weighted count of ones · Responsibilities of a Bernoulli mixture · Responsibility-weighted count of zeros · Posteriors are probability distributions · Marginal of a latent-variable model · Posterior of a latent-variable model

Used byThe M-step of the Bernoulli mixture maximizes the EM objective · The log-likelihood is monotone along the EM iterates of a Bernoulli mixture · Each EM step for the Bernoulli mixture does not decrease the log-likelihood

TheoremDecomposition of the EM objective for the Bernoulli mixture#✓fully proved

Let \(x_1, \dots, x_N \in \{0, 1\}^d\) be data and let \(\theta\) and \(\theta'\) be valid parameters of a mixture of \(K\) products of \(d\) Bernoulli distributions (positive mixing weights summing to one and success probabilities in \((0, 1)\)), where \(\theta'\) has mixing weights \(\pi'_k\) and success probabilities \(p'_{kj}\). Write \(p_\theta(x, k)\) for the joint probability of \(x\) and component \(k\) under \(\theta\) (the mixing weight of \(k\) times the product Bernoulli probability of \(x\)), \(r_{nk} = p_\theta(k \mid x_n) = p_\theta(x_n, k) / \sum_l p_\theta(x_n, l)\) for the posterior probability of component \(k\) given \(x_n\), \(N_k = \sum_n r_{nk}\), and \(A_{kj}\) and \(B_{kj}\) for the sums of \(r_{nk}\) over the points \(x_n\) whose \(j\)-th coordinate \(x_{nj}\) is \(1\) and is \(0\) respectively. Then the EM objective \(Q(\theta' \mid \theta) = \sum_n \sum_k r_{nk} \log p_{\theta'}(x_n, k)\) equals

\[\sum_{k=1}^{K} \Big( N_k \log \pi'_k + \sum_{j=1}^{d} \big( A_{kj} \log p'_{kj} + B_{kj} \log (1 - p'_{kj}) \big) \Big).\]

The first term depends only on the mixing weights and each remaining term on a single \(p'_{kj}\).

theorem emQ_eq (θ' θ : ValidParams d K) :
    emQ joint xs θ' θ = ∑ k, (mass xs θ k * log (θ'.1.weight k) +
      ∑ j, (ones xs θ k j * log (θ'.1.prob k j) + zeros xs θ k j * log (1 - θ'.1.prob k j)))

Uses 11 · Used by 1

Statement usesParameters of a Bernoulli mixture · Valid parameters of a Bernoulli mixture · The parameter space of a Bernoulli mixture · Joint distribution of the Bernoulli mixture · Effective number of points of a Bernoulli-mixture component · Responsibility-weighted count of ones · Responsibility-weighted count of zeros · The EM objective

Proof usesProduct Bernoulli probability mass function · Responsibilities of a Bernoulli mixture · Posterior of a latent-variable model

Used byThe M-step of the Bernoulli mixture maximizes the EM objective

TheoremThe M-step of the Bernoulli mixture maximizes the EM objective#✓fully proved

Let \(x_1, \dots, x_N \in \{0, 1\}^d\) be rich data: \(N > 0\), and for every coordinate \(j < d\) some \(x_n\) has \(j\)-th coordinate \(1\) and some \(x_m\) has \(j\)-th coordinate \(0\). Let \(\theta\) be valid parameters of a mixture of \(K\) products of \(d\) Bernoulli distributions, and let \(\theta^+\) be the result of the EM step applied to \(\theta\). Then every valid parameter \(\theta'\) satisfies \(Q(\theta' \mid \theta) \le Q(\theta^+ \mid \theta)\), where \(Q\) is the EM objective of the mixture's joint distribution.

theorem emQ_le_emStep (hx : Rich xs) (θ' θ : ValidParams d K) :
    emQ joint xs θ' θ ≤ emQ joint xs (emStep xs hx θ) θ

Uses 17 · Used by 2

Statement usesRich data for a Bernoulli mixture · The parameter space of a Bernoulli mixture · One EM step for the Bernoulli mixture · Joint distribution of the Bernoulli mixture · The EM objective

Proof usesParameters of a Bernoulli mixture · Valid parameters of a Bernoulli mixture · Product Bernoulli probability mass function · Decomposition of the EM objective for the Bernoulli mixture · Effective number of points of a Bernoulli-mixture component · Responsibility-weighted count of ones · Responsibilities of a Bernoulli mixture · The weighted log-likelihood is bounded by its value at the normalized counts · Responsibility-weighted count of zeros · Posteriors are probability distributions · Marginal of a latent-variable model · Posterior of a latent-variable model

Used byThe log-likelihood is monotone along the EM iterates of a Bernoulli mixture · Each EM step for the Bernoulli mixture does not decrease the log-likelihood

TheoremEach EM step for the Bernoulli mixture does not decrease the log-likelihood#✓fully proved

Let \(x_1, \dots, x_N \in \{0, 1\}^d\) be rich data: \(N > 0\), and for every coordinate \(j < d\) some \(x_n\) has \(j\)-th coordinate \(1\) and some \(x_m\) has \(j\)-th coordinate \(0\). Let \(\theta\) be valid parameters of a mixture of \(K\) products of \(d\) Bernoulli distributions. Then \(\ell(\theta) \le \ell(\theta^+)\), where \(\ell\) is the log-likelihood of the data under the mixture's joint distribution and \(\theta^+\) is the result of the EM step applied to \(\theta\).

theorem logLik_le_emStep (hx : Rich xs) (θ : ValidParams d K) :
    logLik joint xs θ ≤ logLik joint xs (emStep xs hx θ)

Uses 10

Statement usesRich data for a Bernoulli mixture · The parameter space of a Bernoulli mixture · One EM step for the Bernoulli mixture · Joint distribution of the Bernoulli mixture · Log-likelihood of a latent-variable model

Proof usesParameters of a Bernoulli mixture · Valid parameters of a Bernoulli mixture · Product Bernoulli probability mass function · The M-step of the Bernoulli mixture maximizes the EM objective · The EM theorem

TheoremThe log-likelihood is monotone along the EM iterates of a Bernoulli mixture#✓fully proved

Let \(x_1, \dots, x_N \in \{0, 1\}^d\) be rich data: \(N > 0\), and for every coordinate \(j < d\) some \(x_n\) has \(j\)-th coordinate \(1\) and some \(x_m\) has \(j\)-th coordinate \(0\). Let \(\theta_0\) be valid parameters of a mixture of \(K\) products of \(d\) Bernoulli distributions, and let \(\theta_t\) be the result of \(t\) EM steps from \(\theta_0\). Then \(\ell(\theta_t)\) is nondecreasing in \(t \in \mathbb{N}\), where \(\ell\) is the log-likelihood of the data under the mixture's joint distribution.

theorem logLik_iterate_emStep_monotone (hx : Rich xs) (θ₀ : ValidParams d K) :
    Monotone fun t => logLik joint xs ((emStep xs hx)^[t] θ₀)

Uses 10

Statement usesRich data for a Bernoulli mixture · The parameter space of a Bernoulli mixture · One EM step for the Bernoulli mixture · Joint distribution of the Bernoulli mixture · Log-likelihood of a latent-variable model

Proof usesParameters of a Bernoulli mixture · Valid parameters of a Bernoulli mixture · Product Bernoulli probability mass function · The M-step of the Bernoulli mixture maximizes the EM objective · EM iterates have monotone likelihood

DefinitionIsotropic Gaussian density#✓fully proved

For a mean \(\mu \in \mathbb{R}^d\) and a variance \(v \ge 0\), the isotropic Gaussian density at \(x \in \mathbb{R}^d\) is \(\mathcal{N}(x \mid \mu, v I) = \prod_{i=1}^{d} \varphi_{\mu_i, v}(x_i)\), where \(\varphi_{m, v}\) is the one-dimensional Gaussian density with mean \(m\) and variance \(v\).

For \(v = 0\) the one-dimensional density is identically \(0\), following Mathlib's convention.

noncomputable def isoGaussPDF (μ : EuclideanSpace ℝ (Fin d)) (v : ℝ≥0)
    (x : EuclideanSpace ℝ (Fin d)) : ℝ :=
  ∏ i, gaussianPDFReal (μ i) v (x i)

Used by 14

Used byThe mean and variance updates maximize each component term · The EM objective of an isotropic Gaussian mixture splits by component · The M-step for isotropic Gaussian mixtures maximizes the EM objective · The EM step for isotropic Gaussian mixtures · Joint density of an isotropic Gaussian mixture · Log-density of the isotropic Gaussian · The log-likelihood is monotone along the EM iterates of an isotropic Gaussian mixture · Each EM step for the Gaussian mixture does not decrease the log-likelihood · Mixture density of an isotropic Gaussian mixture · Isotropic Gaussian mixtures: the weight update maximizes the weights term · Ratio of isotropic Gaussian densities with a common variance · The Gaussian-mixture responsibilities are the common-variance responsibilities · Responsibilities with a common variance · Common-variance responsibilities relative to a fixed component

TheoremLog-density of the isotropic Gaussian#✓fully proved

For \(\mu, x \in \mathbb{R}^d\) and a variance \(v > 0\), the isotropic Gaussian density \(\mathcal{N}(x \mid \mu, v I)\) with mean \(\mu\) and covariance \(v I\) satisfies \(\log \mathcal{N}(x \mid \mu, v I) = -\tfrac{d}{2} \log(2 \pi v) - \|x - \mu\|^2 / (2 v)\).

theorem log_isoGaussPDF (μ : EuclideanSpace ℝ (Fin d)) {v : ℝ≥0} (hv : v ≠ 0)
    (x : EuclideanSpace ℝ (Fin d)) :
    log (isoGaussPDF μ v x) = -(d / 2) * log (2 * π * v) - ‖x - μ‖ ^ 2 / (2 * v)

Uses 1 · Used by 2

Statement usesIsotropic Gaussian density

Used byThe EM objective of an isotropic Gaussian mixture splits by component · Ratio of isotropic Gaussian densities with a common variance

StructureParameters of an isotropic Gaussian mixture#✓fully proved

Parameters of a \(K\)-component isotropic Gaussian mixture in \(d\) dimensions consist, for each component \(k < K\), of a mixing weight \(\pi_k \in \mathbb{R}\), a mean \(\mu_k \in \mathbb{R}^d\) and a variance \(\sigma_k^2 \ge 0\); component \(k\) has covariance \(\sigma_k^2 I\).

No constraint is placed on the weights here; validity is a separate condition.

structure Params (d K : ℕ) where
  /-- The mixing weights `π k`. -/
  weight : Fin K → ℝ
  /-- The component means `μ k`. -/
  mean : Fin K → EuclideanSpace ℝ (Fin d)
  /-- The component variances `σ k²` (isotropic: covariance `σ k² I`). -/
  var : Fin K → ℝ≥0

Used by 15

Used byThe mean and variance updates maximize each component term · The EM objective of an isotropic Gaussian mixture splits by component · The M-step for isotropic Gaussian mixtures maximizes the EM objective · The EM step for isotropic Gaussian mixtures · Joint density of an isotropic Gaussian mixture · The log-likelihood is monotone along the EM iterates of an isotropic Gaussian mixture · Each EM step for the Gaussian mixture does not decrease the log-likelihood · M-step of EM for an isotropic Gaussian mixture · Mixture density of an isotropic Gaussian mixture · Valid mixture parameters have at least one component · Isotropic Gaussian mixtures: the weight update maximizes the weights term · Validity of isotropic Gaussian mixture parameters · The parameter space of isotropic Gaussian mixture EM · The Gaussian-mixture M-step mean is the common-variance M-step mean · The Gaussian-mixture responsibilities are the common-variance responsibilities

StructureValidity of isotropic Gaussian mixture parameters#✓fully proved

Parameters of a \(K\)-component isotropic Gaussian mixture in \(d\) dimensions, with mixing weights \(\pi_k\), means \(\mu_k\) and variances \(\sigma_k^2 \ge 0\), are valid when every \(\pi_k > 0\), \(\sum_k \pi_k = 1\), and every \(\sigma_k^2 > 0\).

structure Params.Valid (θ : Params d K) : Prop where
  weight_pos : ∀ k, 0 < θ.weight k
  weight_sum : ∑ k, θ.weight k = 1
  var_ne_zero : ∀ k, θ.var k ≠ 0

Uses 1 · Used by 13

Statement usesParameters of an isotropic Gaussian mixture

Used byThe mean and variance updates maximize each component term · The EM objective of an isotropic Gaussian mixture splits by component · The M-step for isotropic Gaussian mixtures maximizes the EM objective · The EM step for isotropic Gaussian mixtures · Joint density of an isotropic Gaussian mixture · The log-likelihood is monotone along the EM iterates of an isotropic Gaussian mixture · Each EM step for the Gaussian mixture does not decrease the log-likelihood · Mixture density of an isotropic Gaussian mixture · Valid mixture parameters have at least one component · Isotropic Gaussian mixtures: the weight update maximizes the weights term · The parameter space of isotropic Gaussian mixture EM · The Gaussian-mixture M-step mean is the common-variance M-step mean · The Gaussian-mixture responsibilities are the common-variance responsibilities

AbbreviationThe parameter space of isotropic Gaussian mixture EM#✓fully proved

For a \(K\)-component isotropic Gaussian mixture in \(d\) dimensions, the parameter space of EM is the set of parameters (mixing weights \(\pi_k\), means \(\mu_k \in \mathbb{R}^d\) and variances \(\sigma_k^2 \ge 0\)) that are valid: every \(\pi_k > 0\), \(\sum_k \pi_k = 1\), and every \(\sigma_k^2 > 0\).

abbrev ValidParams (d K : ℕ) := {θ : Params d K // θ.Valid}

Uses 2 · Used by 19

Statement usesParameters of an isotropic Gaussian mixture · Validity of isotropic Gaussian mixture parameters

Used byComponent term of the EM objective for isotropic Gaussian mixtures · The mean and variance updates maximize each component term · The EM objective of an isotropic Gaussian mixture splits by component · The M-step for isotropic Gaussian mixtures maximizes the EM objective · The EM step for isotropic Gaussian mixtures · Joint density of an isotropic Gaussian mixture · The log-likelihood is monotone along the EM iterates of an isotropic Gaussian mixture · Each EM step for the Gaussian mixture does not decrease the log-likelihood · M-step of EM for an isotropic Gaussian mixture · Mixture density of an isotropic Gaussian mixture · Effective number of points in an isotropic Gaussian mixture · M-step mean update for an isotropic Gaussian mixture · M-step variance update for an isotropic Gaussian mixture · Valid mixture parameters have at least one component · Responsibilities in an isotropic Gaussian mixture · Responsibility-weighted scatter in an isotropic Gaussian mixture · Isotropic Gaussian mixtures: the weight update maximizes the weights term · The Gaussian-mixture M-step mean is the common-variance M-step mean · The Gaussian-mixture responsibilities are the common-variance responsibilities

DefinitionJoint density of an isotropic Gaussian mixture#✓fully proved

For valid parameters \(\theta\) of a \(K\)-component isotropic Gaussian mixture in \(\mathbb{R}^d\), with weights \(\pi_k\), means \(\mu_k\) and variances \(\sigma_k^2\), the joint density of a point \(x \in \mathbb{R}^d\) and a component \(k\) is \(p_\theta(x, k) = \pi_k \, \mathcal{N}(x \mid \mu_k, \sigma_k^2 I)\), where \(\mathcal{N}(\cdot \mid \mu, v I)\) is the isotropic Gaussian density.

noncomputable def joint (θ : ValidParams d K) (x : EuclideanSpace ℝ (Fin d)) (k : Fin K) : ℝ :=
  θ.1.weight k * isoGaussPDF (θ.1.mean k) (θ.1.var k) x

Uses 4 · Used by 10

Statement usesParameters of an isotropic Gaussian mixture · Validity of isotropic Gaussian mixture parameters · The parameter space of isotropic Gaussian mixture EM · Isotropic Gaussian density

Used byThe mean and variance updates maximize each component term · The EM objective of an isotropic Gaussian mixture splits by component · The M-step for isotropic Gaussian mixtures maximizes the EM objective · The EM step for isotropic Gaussian mixtures · The log-likelihood is monotone along the EM iterates of an isotropic Gaussian mixture · Each EM step for the Gaussian mixture does not decrease the log-likelihood · Mixture density of an isotropic Gaussian mixture · Responsibilities in an isotropic Gaussian mixture · Isotropic Gaussian mixtures: the weight update maximizes the weights term · The Gaussian-mixture responsibilities are the common-variance responsibilities

TheoremMixture density of an isotropic Gaussian mixture#✓fully proved

For valid parameters \(\theta\) with mixing weights \(\pi_k\), means \(\mu_k\) and variances \(\sigma_k^2\), and every \(x \in \mathbb{R}^d\), the marginal \(p_\theta(x) = \sum_k p_\theta(x, k)\) of the joint density equals \(\sum_k \pi_k \, \mathcal{N}(x \mid \mu_k, \sigma_k^2 I)\), where \(\mathcal{N}(x \mid \mu, v I)\) is the isotropic Gaussian density.

theorem marginal_joint (θ : ValidParams d K) (x : EuclideanSpace ℝ (Fin d)) :
    marginal joint θ x = ∑ k, θ.1.weight k * isoGaussPDF (θ.1.mean k) (θ.1.var k) x

Uses 6

Statement usesMarginal of a latent-variable model · Parameters of an isotropic Gaussian mixture · Validity of isotropic Gaussian mixture parameters · The parameter space of isotropic Gaussian mixture EM · Isotropic Gaussian density · Joint density of an isotropic Gaussian mixture

DefinitionResponsibilities in an isotropic Gaussian mixture#✓fully proved

For valid parameters \(\theta\) with mixing weights \(\pi_k\), means \(\mu_k\) and variances \(\sigma_k^2\), a point \(x \in \mathbb{R}^d\) and a component \(k\), the responsibility of \(k\) for \(x\) is the posterior \(p_\theta(k \mid x) = \pi_k \mathcal{N}(x \mid \mu_k, \sigma_k^2 I) / \sum_j \pi_j \mathcal{N}(x \mid \mu_j, \sigma_j^2 I)\), where \(\mathcal{N}(x \mid \mu, v I)\) is the isotropic Gaussian density. Computing it at each data point is the E-step.

noncomputable def resp (θ : ValidParams d K) (x : EuclideanSpace ℝ (Fin d)) (k : Fin K) : ℝ :=
  posterior joint θ x k

Uses 3 · Used by 11

Statement usesPosterior of a latent-variable model · The parameter space of isotropic Gaussian mixture EM · Joint density of an isotropic Gaussian mixture

Used byComponent term of the EM objective for isotropic Gaussian mixtures · The mean and variance updates maximize each component term · The EM objective of an isotropic Gaussian mixture splits by component · The M-step for isotropic Gaussian mixtures maximizes the EM objective · The EM step for isotropic Gaussian mixtures · Effective number of points in an isotropic Gaussian mixture · M-step mean update for an isotropic Gaussian mixture · Responsibility-weighted scatter in an isotropic Gaussian mixture · Isotropic Gaussian mixtures: the weight update maximizes the weights term · The Gaussian-mixture M-step mean is the common-variance M-step mean · The Gaussian-mixture responsibilities are the common-variance responsibilities

TheoremValid mixture parameters have at least one component#✓fully proved

If \(\theta\) is a valid parameter of a \(K\)-component isotropic Gaussian mixture in \(d\) dimensions, then \(K \ge 1\).

theorem nonempty_of_valid (θ : ValidParams d K) : Nonempty (Fin K)

Uses 3 · Used by 4

Statement usesThe parameter space of isotropic Gaussian mixture EM

Proof usesParameters of an isotropic Gaussian mixture · Validity of isotropic Gaussian mixture parameters

Used byThe EM step for isotropic Gaussian mixtures · The log-likelihood is monotone along the EM iterates of an isotropic Gaussian mixture · Each EM step for the Gaussian mixture does not decrease the log-likelihood · Isotropic Gaussian mixtures: the weight update maximizes the weights term

DefinitionEffective number of points in an isotropic Gaussian mixture#✓fully proved

Given data points \(x_0, \dots, x_{N-1}\) in \(\mathbb{R}^d\), valid parameters \(\theta\) of a \(K\)-component isotropic Gaussian mixture and a component \(k\), the effective number of points of \(k\) is \(N_k = \sum_n r_{nk}\), where \(r_{nk}\) is the responsibility of component \(k\) for \(x_n\) under \(\theta\), the posterior probability of \(k\) given \(x_n\).

noncomputable def mass (θ : ValidParams d K) (k : Fin K) : ℝ := ∑ n, resp θ (xs n) k

Uses 2 · Used by 9

Statement usesThe parameter space of isotropic Gaussian mixture EM · Responsibilities in an isotropic Gaussian mixture

Used byThe mean and variance updates maximize each component term · The EM objective of an isotropic Gaussian mixture splits by component · The M-step for isotropic Gaussian mixtures maximizes the EM objective · The EM step for isotropic Gaussian mixtures · M-step of EM for an isotropic Gaussian mixture · M-step mean update for an isotropic Gaussian mixture · M-step variance update for an isotropic Gaussian mixture · Isotropic Gaussian mixtures: the weight update maximizes the weights term · The Gaussian-mixture M-step mean is the common-variance M-step mean

DefinitionM-step mean update for an isotropic Gaussian mixture#✓fully proved

Given data points \(x_0, \dots, x_{N-1}\) in \(\mathbb{R}^d\), valid parameters \(\theta\) of a \(K\)-component isotropic Gaussian mixture and a component \(k\), the updated mean of \(k\) is the responsibility-weighted mean \(\mu_k' = N_k^{-1} \sum_n r_{nk} x_n\), where \(r_{nk}\) is the responsibility of component \(k\) for \(x_n\) under \(\theta\) and \(N_k = \sum_n r_{nk}\).

The inverse of \(0\) is read as \(0\).

noncomputable def newMean (θ : ValidParams d K) (k : Fin K) : EuclideanSpace ℝ (Fin d) :=
  (mass xs θ k)⁻¹ • ∑ n, resp θ (xs n) k • xs n

Uses 3 · Used by 6

Statement usesThe parameter space of isotropic Gaussian mixture EM · Effective number of points in an isotropic Gaussian mixture · Responsibilities in an isotropic Gaussian mixture

Used byThe mean and variance updates maximize each component term · The M-step for isotropic Gaussian mixtures maximizes the EM objective · The EM step for isotropic Gaussian mixtures · M-step of EM for an isotropic Gaussian mixture · Responsibility-weighted scatter in an isotropic Gaussian mixture · The Gaussian-mixture M-step mean is the common-variance M-step mean

DefinitionResponsibility-weighted scatter in an isotropic Gaussian mixture#✓fully proved

Given data points \(x_0, \dots, x_{N-1}\) in \(\mathbb{R}^d\), valid parameters \(\theta\) of a \(K\)-component isotropic Gaussian mixture and a component \(k\), the scatter of \(k\) is \(S_k = \sum_n r_{nk} \lVert x_n - \mu_k' \rVert^2\), where \(r_{nk}\) is the responsibility of component \(k\) for \(x_n\) under \(\theta\), \(N_k = \sum_n r_{nk}\) and \(\mu_k' = N_k^{-1} \sum_n r_{nk} x_n\) is the responsibility-weighted mean.

noncomputable def scatter (θ : ValidParams d K) (k : Fin K) : ℝ :=
  ∑ n, resp θ (xs n) k * ‖xs n - newMean xs θ k‖ ^ 2

Uses 3 · Used by 4

Statement usesThe parameter space of isotropic Gaussian mixture EM · M-step mean update for an isotropic Gaussian mixture · Responsibilities in an isotropic Gaussian mixture

Used byThe mean and variance updates maximize each component term · The M-step for isotropic Gaussian mixtures maximizes the EM objective · The EM step for isotropic Gaussian mixtures · M-step variance update for an isotropic Gaussian mixture

DefinitionM-step variance update for an isotropic Gaussian mixture#✓fully proved

Given data points \(x_0, \dots, x_{N-1}\) in \(\mathbb{R}^d\), valid parameters \(\theta\) of a \(K\)-component isotropic Gaussian mixture and a component \(k\), the updated variance of \(k\) is \(\sigma_k'^2 = S_k / (d N_k)\), where \(r_{nk}\) is the responsibility of component \(k\) for \(x_n\) under \(\theta\), \(N_k = \sum_n r_{nk}\), \(\mu_k' = N_k^{-1} \sum_n r_{nk} x_n\) and \(S_k = \sum_n r_{nk} \lVert x_n - \mu_k' \rVert^2\).

Division by zero is read as \(0\).

noncomputable def newVar (θ : ValidParams d K) (k : Fin K) : ℝ := scatter xs θ k / (d * mass xs θ k)

Uses 3 · Used by 4

Statement usesThe parameter space of isotropic Gaussian mixture EM · Effective number of points in an isotropic Gaussian mixture · Responsibility-weighted scatter in an isotropic Gaussian mixture

Used byThe mean and variance updates maximize each component term · The M-step for isotropic Gaussian mixtures maximizes the EM objective · The EM step for isotropic Gaussian mixtures · M-step of EM for an isotropic Gaussian mixture

DefinitionM-step of EM for an isotropic Gaussian mixture#✓fully proved

Let \(x_0, \dots, x_{N-1}\) be data points in \(\mathbb{R}^d\), let \(\theta\) be valid parameters of a \(K\)-component isotropic Gaussian mixture, and let \(r_{nk}\) be the responsibility of component \(k\) for \(x_n\) under \(\theta\). With \(N_k = \sum_n r_{nk}\), the M-step returns the parameters with mixing weights \(\pi_k' = N_k / N\), means \(\mu_k' = N_k^{-1} \sum_n r_{nk} x_n\) and variances \(\sigma_k'^2 = S_k / (d N_k)\), where \(S_k = \sum_n r_{nk} \lVert x_n - \mu_k' \rVert^2\).

Division by zero is read as \(0\).

noncomputable def mStep (θ : ValidParams d K) : Params d K where
  weight k := mass xs θ k / N
  mean := newMean xs θ
  var k := (newVar xs θ k).toNNReal

Uses 5 · Used by 1

Statement usesParameters of an isotropic Gaussian mixture · The parameter space of isotropic Gaussian mixture EM · Effective number of points in an isotropic Gaussian mixture · M-step mean update for an isotropic Gaussian mixture · M-step variance update for an isotropic Gaussian mixture

Used byThe EM step for isotropic Gaussian mixtures

TheoremThe weighted centroid decomposition#✓fully proved

Let \(F\) be a real inner product space, \(s\) a finite index set, \(w_i \in \mathbb{R}\) weights with \(W = \sum_{i \in s} w_i \ne 0\), and \(x_i \in F\) points for \(i \in s\), and let \(m = W^{-1} \sum_{i \in s} w_i x_i\). Then for every \(c \in F\),

\[\sum_{i \in s} w_i \|x_i - c\|^2 = \sum_{i \in s} w_i \|x_i - m\|^2 + W \|m - c\|^2.\]

This is the weighted version of the centroid decomposition behind \(k\)-means. When \(W > 0\) it shows that \(m\) minimizes \(c \mapsto \sum_{i \in s} w_i \|x_i - c\|^2\).

theorem sum_mul_norm_sub_sq {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
    {ι : Type*} (s : Finset ι) (w : ι → ℝ) (x : ι → F) (hW : ∑ i ∈ s, w i ≠ 0) (c : F) :
    ∑ i ∈ s, w i * ‖x i - c‖ ^ 2 =
      ∑ i ∈ s, w i * ‖x i - (∑ i ∈ s, w i)⁻¹ • ∑ i ∈ s, w i • x i‖ ^ 2 +
        (∑ i ∈ s, w i) * ‖(∑ i ∈ s, w i)⁻¹ • ∑ i ∈ s, w i • x i - c‖ ^ 2

Used by 2

Used byThe mean and variance updates maximize each component term · With positive total weight, the weighted mean minimizes the weighted sum of squared distances

TheoremWith positive total weight, the weighted mean minimizes the weighted sum of squared distances#✓fully proved

With positive total weight, the weighted mean minimizes the weighted sum of squared distances. Let \(F\) be a real inner product space, \(s\) a finite index set, \(w_i \in \mathbb{R}\) weights with \(W = \sum_{i \in s} w_i > 0\), and \(x_i \in F\) points for \(i \in s\), and let \(m = W^{-1} \sum_{i \in s} w_i x_i\) be the weighted mean. Then for every \(c \in F\),

\[\sum_{i \in s} w_i \|x_i - m\|^2 \le \sum_{i \in s} w_i \|x_i - c\|^2.\]

The individual weights need not be nonnegative; only their total is assumed positive.

theorem sum_mul_norm_sub_sq_mean_le {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
    {ι : Type*} (s : Finset ι) {w : ι → ℝ} (hW : 0 < ∑ i ∈ s, w i)
    (x : ι → F) (c : F) :
    ∑ i ∈ s, w i * ‖x i - (∑ i ∈ s, w i)⁻¹ • ∑ i ∈ s, w i • x i‖ ^ 2 ≤
      ∑ i ∈ s, w i * ‖x i - c‖ ^ 2

Uses 1

Proof usesThe weighted centroid decomposition

DefinitionData that are not all equal#✓fully proved

A finite family of points \(x_0, \dots, x_{N-1}\) in \(\mathbb{R}^d\) is not all equal when there are indices \(n\) and \(n'\) with \(x_n \ne x_{n'}\).

def NotAllEqual (xs : Fin N → EuclideanSpace ℝ (Fin d)) : Prop := ∃ n n', xs n ≠ xs n'

Used by 5

Used byThe mean and variance updates maximize each component term · The M-step for isotropic Gaussian mixtures maximizes the EM objective · The EM step for isotropic Gaussian mixtures · The log-likelihood is monotone along the EM iterates of an isotropic Gaussian mixture · Each EM step for the Gaussian mixture does not decrease the log-likelihood

DefinitionThe EM step for isotropic Gaussian mixtures#✓fully proved

Let \(x_1, \dots, x_N\) be points of \(\mathbb{R}^d\) that are not all equal and let \(\theta\) be valid parameters of a \(K\)-component isotropic Gaussian mixture. With \(r_{nk}\) the responsibility of component \(k\) for \(x_n\) under \(\theta\) (the E-step), the EM step sends \(\theta\) to the valid parameters with weights \(\pi_k' = N_k / N\), means \(\mu_k' = N_k^{-1} \sum_n r_{nk} x_n\) and variances \(v_k' = S_k / (d N_k)\), where \(N_k = \sum_n r_{nk}\) and \(S_k = \sum_n r_{nk} \|x_n - \mu_k'\|^2\) (the M-step).

noncomputable def emStep (hx : NotAllEqual xs) (θ : ValidParams d K) : ValidParams d K :=
  ⟨mStep xs θ, mStep_valid hx θ⟩

Uses 16 · Used by 3

Statement usesPosteriors are probability distributions · Marginal of a latent-variable model · Posterior of a latent-variable model · Data that are not all equal · Parameters of an isotropic Gaussian mixture · Validity of isotropic Gaussian mixture parameters · The parameter space of isotropic Gaussian mixture EM · Isotropic Gaussian density · Joint density of an isotropic Gaussian mixture · M-step of EM for an isotropic Gaussian mixture · Effective number of points in an isotropic Gaussian mixture · M-step mean update for an isotropic Gaussian mixture · M-step variance update for an isotropic Gaussian mixture · Valid mixture parameters have at least one component · Responsibilities in an isotropic Gaussian mixture · Responsibility-weighted scatter in an isotropic Gaussian mixture

Used byThe M-step for isotropic Gaussian mixtures maximizes the EM objective · The log-likelihood is monotone along the EM iterates of an isotropic Gaussian mixture · Each EM step for the Gaussian mixture does not decrease the log-likelihood

DefinitionComponent term of the EM objective for isotropic Gaussian mixtures#✓fully proved

Given points \(x_1, \dots, x_N\) of \(\mathbb{R}^d\), valid parameters \(\theta\) of a \(K\)-component isotropic Gaussian mixture, a component \(k\), a mean \(\mu \in \mathbb{R}^d\) and a real number \(v\), the component term is

\[ C_k(\mu, v) = \sum_n r_{nk} \bigl(-\tfrac{d}{2} \log(2\pi v) - \|x_n - \mu\|^2 / (2v)\bigr), \]

where \(r_{nk}\) is the responsibility of component \(k\) for \(x_n\) under \(\theta\).

For \(v > 0\) this is \(\sum_n r_{nk} \log \mathcal{N}(x_n \mid \mu, v I)\), where \(\mathcal{N}(\cdot \mid \mu, v I)\) is the isotropic Gaussian density with mean \(\mu\) and covariance \(v I\).

noncomputable def compTerm (θ : ValidParams d K) (k : Fin K) (μ : EuclideanSpace ℝ (Fin d))
    (v : ℝ) : ℝ :=
  ∑ n, resp θ (xs n) k * (-(d / 2) * log (2 * π * v) - ‖xs n - μ‖ ^ 2 / (2 * v))

Uses 2 · Used by 3

Statement usesThe parameter space of isotropic Gaussian mixture EM · Responsibilities in an isotropic Gaussian mixture

Used byThe mean and variance updates maximize each component term · The EM objective of an isotropic Gaussian mixture splits by component · The M-step for isotropic Gaussian mixtures maximizes the EM objective

TheoremThe EM objective of an isotropic Gaussian mixture splits by component#✓fully proved

Let \(x_1, \dots, x_N\) be points of \(\mathbb{R}^d\), and let \(\theta'\) and \(\theta\) be valid parameters of a \(K\)-component isotropic Gaussian mixture, where \(\theta'\) has weights \(\pi_k'\), means \(\mu_k'\) and variances \(v_k'\). Then the EM objective of the mixture's joint density satisfies

\[ Q(\theta' \mid \theta) = \sum_k \bigl(N_k \log \pi_k' + C_k(\mu_k', v_k')\bigr), \]

where \(r_{nk}\) is the responsibility of component \(k\) for \(x_n\) under \(\theta\), \(N_k = \sum_n r_{nk}\) and \(C_k(\mu, v) = \sum_n r_{nk} \bigl(-\tfrac{d}{2} \log(2\pi v) - \|x_n - \mu\|^2 / (2v)\bigr)\).

theorem emQ_eq (θ' θ : ValidParams d K) :
    emQ joint xs θ' θ = ∑ k, (mass xs θ k * log (θ'.1.weight k) +
      compTerm xs θ k (θ'.1.mean k) (θ'.1.var k))

Uses 11 · Used by 1

Statement usesThe EM objective · Parameters of an isotropic Gaussian mixture · Validity of isotropic Gaussian mixture parameters · The parameter space of isotropic Gaussian mixture EM · Component term of the EM objective for isotropic Gaussian mixtures · Joint density of an isotropic Gaussian mixture · Effective number of points in an isotropic Gaussian mixture

Proof usesPosterior of a latent-variable model · Isotropic Gaussian density · Log-density of the isotropic Gaussian · Responsibilities in an isotropic Gaussian mixture

Used byThe M-step for isotropic Gaussian mixtures maximizes the EM objective

TheoremIsotropic Gaussian mixtures: the weight update maximizes the weights term#✓fully proved

Let \(x_1, \dots, x_N\) be \(N > 0\) points of \(\mathbb{R}^d\), let \(\theta\) be valid parameters of a \(K\)-component isotropic Gaussian mixture in \(d\) dimensions, and let \(N_k = \sum_n r_{nk}\) be the mass of component \(k\), where \(r_{nk}\) is the responsibility of component \(k\) for \(x_n\) under \(\theta\). Then for all real \(w_1, \dots, w_K > 0\) with \(\sum_k w_k = 1\),

\[\sum_k N_k \log w_k \le \sum_k N_k \log \frac{N_k}{N}.\]

That is, the M-step weights \(N_k / N\) maximize the weights term (Gibbs' inequality).

theorem sum_mass_mul_log_le (hN0 : 0 < N) (θ : ValidParams d K) {w : Fin K → ℝ}
    (hw : ∀ k, 0 < w k) (hsum : ∑ k, w k = 1) :
    ∑ k, mass xs θ k * log (w k) ≤ ∑ k, mass xs θ k * log (mass xs θ k / N)

Uses 13 · Used by 1

Statement usesThe parameter space of isotropic Gaussian mixture EM · Effective number of points in an isotropic Gaussian mixture

Proof usesProbability distributions on a finite latent space · Posteriors are probability distributions · Marginal of a latent-variable model · Posterior of a latent-variable model · Gibbs' inequality (evidence lower bound form) · Parameters of an isotropic Gaussian mixture · Validity of isotropic Gaussian mixture parameters · Isotropic Gaussian density · Joint density of an isotropic Gaussian mixture · Valid mixture parameters have at least one component · Responsibilities in an isotropic Gaussian mixture

Used byThe M-step for isotropic Gaussian mixtures maximizes the EM objective

TheoremThe mean and variance updates maximize each component term#✓fully proved

Let \(x_1, \dots, x_N\) be points of \(\mathbb{R}^d\) that are not all equal, let \(\theta\) be valid parameters of a \(K\)-component isotropic Gaussian mixture, let \(k\) be a component, and let \(r_{nk}\) be the responsibility of component \(k\) for \(x_n\) under \(\theta\). For every \(\mu \in \mathbb{R}^d\) and every real \(v > 0\), the component term

\[ C_k(\mu, v) = \sum_n r_{nk} \bigl(-\tfrac{d}{2} \log(2\pi v) - \|x_n - \mu\|^2 / (2v)\bigr) \]

satisfies \(C_k(\mu, v) \le C_k(\mu_k', v_k')\), where \(N_k = \sum_n r_{nk}\), \(\mu_k' = N_k^{-1} \sum_n r_{nk} x_n\) is the responsibility-weighted mean, \(S_k = \sum_n r_{nk} \|x_n - \mu_k'\|^2\) and \(v_k' = S_k / (d N_k)\).

theorem compTerm_le (hx : NotAllEqual xs) (θ : ValidParams d K) (k : Fin K)
    (μ : EuclideanSpace ℝ (Fin d)) {v : ℝ} (hv : 0 < v) :
    compTerm xs θ k μ v ≤ compTerm xs θ k (newMean xs θ k) (newVar xs θ k)

Uses 14 · Used by 1

Statement usesData that are not all equal · The parameter space of isotropic Gaussian mixture EM · Component term of the EM objective for isotropic Gaussian mixtures · M-step mean update for an isotropic Gaussian mixture · M-step variance update for an isotropic Gaussian mixture

Proof usesMarginal of a latent-variable model · Parameters of an isotropic Gaussian mixture · Validity of isotropic Gaussian mixture parameters · Isotropic Gaussian density · Joint density of an isotropic Gaussian mixture · Effective number of points in an isotropic Gaussian mixture · Responsibilities in an isotropic Gaussian mixture · Responsibility-weighted scatter in an isotropic Gaussian mixture · The weighted centroid decomposition

Used byThe M-step for isotropic Gaussian mixtures maximizes the EM objective

TheoremThe M-step for isotropic Gaussian mixtures maximizes the EM objective#✓fully proved

Let \(x_1, \dots, x_N\) be points of \(\mathbb{R}^d\) that are not all equal, let \(\theta\) be valid parameters of a \(K\)-component isotropic Gaussian mixture, and let \(\theta^+\) be the result of the EM step applied to \(\theta\). Then every valid parameter \(\theta'\) satisfies \(Q(\theta' \mid \theta) \le Q(\theta^+ \mid \theta)\), where \(Q\) is the EM objective of the mixture's joint density.

theorem emQ_le_emStep (hx : NotAllEqual xs) (θ' θ : ValidParams d K) :
    emQ joint xs θ' θ ≤ emQ joint xs (emStep xs hx θ) θ

Uses 18 · Used by 2

Statement usesThe EM objective · Data that are not all equal · The parameter space of isotropic Gaussian mixture EM · The EM step for isotropic Gaussian mixtures · Joint density of an isotropic Gaussian mixture

Proof usesMarginal of a latent-variable model · Parameters of an isotropic Gaussian mixture · Validity of isotropic Gaussian mixture parameters · Component term of the EM objective for isotropic Gaussian mixtures · The mean and variance updates maximize each component term · The EM objective of an isotropic Gaussian mixture splits by component · Isotropic Gaussian density · Effective number of points in an isotropic Gaussian mixture · M-step mean update for an isotropic Gaussian mixture · M-step variance update for an isotropic Gaussian mixture · Responsibilities in an isotropic Gaussian mixture · Responsibility-weighted scatter in an isotropic Gaussian mixture · Isotropic Gaussian mixtures: the weight update maximizes the weights term

Used byThe log-likelihood is monotone along the EM iterates of an isotropic Gaussian mixture · Each EM step for the Gaussian mixture does not decrease the log-likelihood

TheoremEach EM step for the Gaussian mixture does not decrease the log-likelihood#✓fully proved

Let \(x_1, \dots, x_N\) be points of \(\mathbb{R}^d\) that are not all equal and let \(\theta\) be valid parameters of a \(K\)-component isotropic Gaussian mixture. Then \(\ell(\theta) \le \ell(\theta^+)\), where \(\ell\) is the log-likelihood of the data under the mixture and \(\theta^+\) is the result of the EM step applied to \(\theta\).

theorem logLik_le_emStep (hx : NotAllEqual xs) (θ : ValidParams d K) :
    logLik joint xs θ ≤ logLik joint xs (emStep xs hx θ)

Uses 11

Statement usesLog-likelihood of a latent-variable model · Data that are not all equal · The parameter space of isotropic Gaussian mixture EM · The EM step for isotropic Gaussian mixtures · Joint density of an isotropic Gaussian mixture

Proof usesThe EM theorem · Parameters of an isotropic Gaussian mixture · Validity of isotropic Gaussian mixture parameters · The M-step for isotropic Gaussian mixtures maximizes the EM objective · Isotropic Gaussian density · Valid mixture parameters have at least one component

TheoremThe log-likelihood is monotone along the EM iterates of an isotropic Gaussian mixture#✓fully proved

Let \(x_1, \dots, x_N\) be points of \(\mathbb{R}^d\) that are not all equal, let \(\theta_0\) be valid parameters of a \(K\)-component isotropic Gaussian mixture, and let \(\theta_t\) be the result of \(t\) EM steps from \(\theta_0\). Then \(\ell(\theta_t)\) is nondecreasing in \(t \in \mathbb{N}\), where \(\ell\) is the log-likelihood of the data under the mixture.

theorem logLik_iterate_emStep_monotone (hx : NotAllEqual xs) (θ₀ : ValidParams d K) :
    Monotone fun t => logLik joint xs ((emStep xs hx)^[t] θ₀)

Uses 11

Statement usesLog-likelihood of a latent-variable model · Data that are not all equal · The parameter space of isotropic Gaussian mixture EM · The EM step for isotropic Gaussian mixtures · Joint density of an isotropic Gaussian mixture

Proof usesEM iterates have monotone likelihood · Parameters of an isotropic Gaussian mixture · Validity of isotropic Gaussian mixture parameters · The M-step for isotropic Gaussian mixtures maximizes the EM objective · Isotropic Gaussian density · Valid mixture parameters have at least one component

StructureParameters of a full-covariance Gaussian mixture#✓fully proved

A parameter of the \(K\)-component Gaussian mixture in \(d\) dimensions with full covariances consists of, for each component \(k < K\), a real mixing weight \(\pi_k\), a mean \(\mu_k \in \mathbb{R}^d\) and a real \(d \times d\) covariance matrix \(\Sigma_k\), with no constraints imposed.

structure Params (d K : ℕ) where
  /-- The mixing weights `π k`. -/
  weight : Fin K → ℝ
  /-- The component means `μ k`. -/
  mean : Fin K → EuclideanSpace ℝ (Fin d)
  /-- The component covariances `Σ k`. -/
  cov : Fin K → Matrix (Fin d) (Fin d) ℝ

Used by 12

Used byThe mean and covariance updates maximize each component term · The EM objective of a full-covariance Gaussian mixture splits by component · The M-step of the full-covariance Gaussian mixture maximizes the EM objective · EM step for the full-covariance Gaussian mixture · Joint density of the full-covariance Gaussian mixture · The log-likelihood is monotone along the EM iterates of a full-covariance Gaussian mixture · Each EM step for the full-covariance Gaussian mixture does not decrease the log-likelihood · M-step of the full-covariance Gaussian mixture · The covariance update is positive definite · The weight update maximizes the weights term of the full-covariance mixture · Validity of full-covariance Gaussian mixture parameters · Valid parameters of a full-covariance Gaussian mixture

StructureValidity of full-covariance Gaussian mixture parameters#✓fully proved

Parameters \((\pi_k, \mu_k, \Sigma_k)_{k\lt K}\) of a \(K\)-component Gaussian mixture in \(d\) dimensions are valid when every weight \(\pi_k\) is positive, the weights sum to one, and every covariance matrix \(\Sigma_k\) is positive definite.

structure Params.Valid (θ : Params d K) : Prop where
  weight_pos : ∀ k, 0 < θ.weight k
  weight_sum : ∑ k, θ.weight k = 1
  cov_posDef : ∀ k, (θ.cov k).PosDef

Uses 1 · Used by 10

Statement usesParameters of a full-covariance Gaussian mixture

Used byThe mean and covariance updates maximize each component term · The EM objective of a full-covariance Gaussian mixture splits by component · The M-step of the full-covariance Gaussian mixture maximizes the EM objective · EM step for the full-covariance Gaussian mixture · Joint density of the full-covariance Gaussian mixture · The log-likelihood is monotone along the EM iterates of a full-covariance Gaussian mixture · Each EM step for the full-covariance Gaussian mixture does not decrease the log-likelihood · The covariance update is positive definite · The weight update maximizes the weights term of the full-covariance mixture · Valid parameters of a full-covariance Gaussian mixture

AbbreviationValid parameters of a full-covariance Gaussian mixture#✓fully proved

The parameter space of EM for the \(K\)-component Gaussian mixture in \(d\) dimensions with full covariances is the set of parameters \((\pi_k, \mu_k, \Sigma_k)_{k\lt K}\) that are valid: every weight \(\pi_k\) is positive, the weights sum to one, and every covariance matrix \(\Sigma_k\) is positive definite.

abbrev ValidParams (d K : ℕ) := {θ : Params d K // θ.Valid}

Uses 2 · Used by 15

Statement usesParameters of a full-covariance Gaussian mixture · Validity of full-covariance Gaussian mixture parameters

Used byComponent term of the EM objective for full-covariance Gaussian mixtures · The mean and covariance updates maximize each component term · The EM objective of a full-covariance Gaussian mixture splits by component · The M-step of the full-covariance Gaussian mixture maximizes the EM objective · EM step for the full-covariance Gaussian mixture · Joint density of the full-covariance Gaussian mixture · The log-likelihood is monotone along the EM iterates of a full-covariance Gaussian mixture · Each EM step for the full-covariance Gaussian mixture does not decrease the log-likelihood · M-step of the full-covariance Gaussian mixture · Effective number of points of a full-covariance mixture component · Covariance update of the full-covariance Gaussian mixture · The covariance update is positive definite · Mean update of the full-covariance Gaussian mixture · Responsibilities of the full-covariance Gaussian mixture · The weight update maximizes the weights term of the full-covariance mixture

DefinitionJoint density of the full-covariance Gaussian mixture#✓fully proved

For valid parameters \(\theta\) with weights \(\pi_k\), means \(\mu_k\) and covariances \(\Sigma_k\), the joint density of a point \(x \in \mathbb{R}^d\) and a component \(k\) is \(p_\theta(x, k) = \pi_k \, \mathcal{N}(x \mid \mu_k, \Sigma_k)\), where \(\mathcal{N}(x \mid \mu, \Sigma)\) is the multivariate Gaussian density.

noncomputable def joint (θ : ValidParams d K) (x : EuclideanSpace ℝ (Fin d)) (k : Fin K) : ℝ :=
  θ.1.weight k * multivariateGaussianPDFReal (θ.1.mean k) (θ.1.cov k) x

Uses 4 · Used by 9

Statement usesParameters of a full-covariance Gaussian mixture · Validity of full-covariance Gaussian mixture parameters · Valid parameters of a full-covariance Gaussian mixture · Multivariate Gaussian density function

Used byThe mean and covariance updates maximize each component term · The EM objective of a full-covariance Gaussian mixture splits by component · The M-step of the full-covariance Gaussian mixture maximizes the EM objective · EM step for the full-covariance Gaussian mixture · The log-likelihood is monotone along the EM iterates of a full-covariance Gaussian mixture · Each EM step for the full-covariance Gaussian mixture does not decrease the log-likelihood · The covariance update is positive definite · Responsibilities of the full-covariance Gaussian mixture · The weight update maximizes the weights term of the full-covariance mixture

DefinitionResponsibilities of the full-covariance Gaussian mixture#✓fully proved

For valid parameters \(\theta = (\pi_j, \mu_j, \Sigma_j)_{j\lt K}\), a point \(x \in \mathbb{R}^d\) and a component \(k\), write \(p_k(x) = \pi_k \, \mathcal{N}(x \mid \mu_k, \Sigma_k)\), where \(\mathcal{N}(\cdot \mid \mu, \Sigma)\) is the multivariate Gaussian density. The responsibility of \(k\) for \(x\) is the posterior probability of component \(k\) given \(x\) (the E-step),

\[r_k(x) = \frac{p_k(x)}{\sum_j p_j(x)}.\]

For data \((x_n)_{n\lt N}\) one writes \(r_{nk} = r_k(x_n)\).

noncomputable def resp (θ : ValidParams d K) (x : EuclideanSpace ℝ (Fin d)) (k : Fin K) : ℝ :=
  posterior joint θ x k

Uses 3 · Used by 9

Statement usesPosterior of a latent-variable model · Valid parameters of a full-covariance Gaussian mixture · Joint density of the full-covariance Gaussian mixture

Used byComponent term of the EM objective for full-covariance Gaussian mixtures · The mean and covariance updates maximize each component term · The EM objective of a full-covariance Gaussian mixture splits by component · EM step for the full-covariance Gaussian mixture · Effective number of points of a full-covariance mixture component · Covariance update of the full-covariance Gaussian mixture · The covariance update is positive definite · Mean update of the full-covariance Gaussian mixture · The weight update maximizes the weights term of the full-covariance mixture

DefinitionEffective number of points of a full-covariance mixture component#✓fully proved

For data \(x_1, \dots, x_N \in \mathbb{R}^d\) and valid parameters \(\theta\) with responsibilities \(r_{nk}\), the effective number of points of component \(k\) is \(N_k = \sum_n r_{nk}\).

noncomputable def mass (θ : ValidParams d K) (k : Fin K) : ℝ := ∑ n, resp θ (xs n) k

Uses 2 · Used by 5

Statement usesValid parameters of a full-covariance Gaussian mixture · Responsibilities of the full-covariance Gaussian mixture

Used byThe EM objective of a full-covariance Gaussian mixture splits by component · The M-step of the full-covariance Gaussian mixture maximizes the EM objective · EM step for the full-covariance Gaussian mixture · M-step of the full-covariance Gaussian mixture · The weight update maximizes the weights term of the full-covariance mixture

DefinitionMean update of the full-covariance Gaussian mixture#✓fully proved

Given data \((x_n)_{n\lt N}\) in \(\mathbb{R}^d\), valid parameters \(\theta\) and a component \(k\), let \(r_{nk}\) be the responsibility of component \(k\) for \(x_n\) and let \(N_k = \sum_n r_{nk}\). The mean update is the responsibility-weighted mean

\[\mu_k' = \frac{1}{N_k} \sum_n r_{nk} x_n \in \mathbb{R}^d.\]

When there are no data (\(N = 0\)), \(N_k = 0\) and the convention \(N_k^{-1} = 0\) makes \(\mu_k' = 0\).

noncomputable def newMean (θ : ValidParams d K) (k : Fin K) : EuclideanSpace ℝ (Fin d) :=
  weightedMean (fun n => resp θ (xs n) k) xs

Uses 3 · Used by 4

Statement usesValid parameters of a full-covariance Gaussian mixture · Responsibilities of the full-covariance Gaussian mixture · Weighted mean

Used byThe mean and covariance updates maximize each component term · M-step of the full-covariance Gaussian mixture · Covariance update of the full-covariance Gaussian mixture · The covariance update is positive definite

DefinitionCovariance update of the full-covariance Gaussian mixture#✓fully proved

Given data \((x_n)_{n\lt N}\) in \(\mathbb{R}^d\), valid parameters \(\theta\) and a component \(k\), let \(r_{nk}\) be the responsibility of component \(k\) for \(x_n\), let \(N_k = \sum_n r_{nk}\), and let \(\mu_k'\) be the responsibility-weighted mean \(N_k^{-1} \sum_n r_{nk} x_n\). The covariance update is the real \(d \times d\) matrix

\[\Sigma_k' = \frac{1}{N_k} \sum_n r_{nk} (x_n - \mu_k')(x_n - \mu_k')^{\top}.\]

When there are no data (\(N = 0\)), \(N_k = 0\) and the convention \(N_k^{-1} = 0\) makes \(\Sigma_k' = 0\).

noncomputable def newCov (θ : ValidParams d K) (k : Fin K) : Matrix (Fin d) (Fin d) ℝ :=
  weightedScatter (fun n => resp θ (xs n) k) xs (newMean xs θ k)

Uses 4 · Used by 3

Statement usesValid parameters of a full-covariance Gaussian mixture · Mean update of the full-covariance Gaussian mixture · Responsibilities of the full-covariance Gaussian mixture · Weighted scatter matrix

Used byThe mean and covariance updates maximize each component term · M-step of the full-covariance Gaussian mixture · The covariance update is positive definite

DefinitionM-step of the full-covariance Gaussian mixture#✓fully proved

For data \(x_1, \dots, x_N \in \mathbb{R}^d\) and valid parameters \(\theta\) with responsibilities \(r_{nk}\), let \(N_k = \sum_n r_{nk}\). The M-step parameters have weights \(\pi'_k = N_k / N\), means \(\mu'_k = N_k^{-1} \sum_n r_{nk} x_n\) and covariances \(\Sigma'_k = N_k^{-1} \sum_n r_{nk} (x_n - \mu'_k)(x_n - \mu'_k)^{\top}\).

noncomputable def mStep (θ : ValidParams d K) : Params d K where
  weight k := mass xs θ k / N
  mean := newMean xs θ
  cov := newCov xs θ

Uses 5 · Used by 1

Statement usesParameters of a full-covariance Gaussian mixture · Valid parameters of a full-covariance Gaussian mixture · Effective number of points of a full-covariance mixture component · Covariance update of the full-covariance Gaussian mixture · Mean update of the full-covariance Gaussian mixture

Used byEM step for the full-covariance Gaussian mixture

StructureData that span the space affinely#✓fully proved

A family \((x_n)_{n\lt N}\) of points of \(\mathbb{R}^d\) is in general position when it has at least one point (\(N > 0\)) and is not contained in an affine hyperplane: for every nonzero \(v \in \mathbb{R}^d\) there are indices \(n, n'\) with \(\langle v, x_n \rangle \neq \langle v, x_{n'} \rangle\).

On such data every responsibility-weighted sample covariance is positive definite.

structure SpansAffinely (xs : Fin N → EuclideanSpace ℝ (Fin d)) : Prop where
  pos : 0 < N
  spans : ∀ v : EuclideanSpace ℝ (Fin d), v ≠ 0 → ∃ n n', ⟪v, xs n⟫ ≠ ⟪v, xs n'⟫

Used by 6

Used byThe mean and covariance updates maximize each component term · The M-step of the full-covariance Gaussian mixture maximizes the EM objective · EM step for the full-covariance Gaussian mixture · The log-likelihood is monotone along the EM iterates of a full-covariance Gaussian mixture · Each EM step for the full-covariance Gaussian mixture does not decrease the log-likelihood · The covariance update is positive definite

TheoremThe covariance update is positive definite#✓fully proved

Let \((x_n)_{n\lt N}\) be data in \(\mathbb{R}^d\) in general position: \(N > 0\), and for every nonzero \(v \in \mathbb{R}^d\) the values \(\langle v, x_n \rangle\) are not all equal. Then for all valid parameters \(\theta\) of the \(K\)-component full-covariance Gaussian mixture and every component \(k\), the covariance update \(\Sigma_k'\) (the responsibility-weighted sample covariance of the data about the responsibility-weighted mean) is positive definite.

theorem newCov_posDef {xs : Fin N → EuclideanSpace ℝ (Fin d)} (hx : SpansAffinely xs)
    (θ : ValidParams d K) (k : Fin K) : (newCov xs θ k).PosDef

Uses 11 · Used by 1

Statement usesData that span the space affinely · Valid parameters of a full-covariance Gaussian mixture · Covariance update of the full-covariance Gaussian mixture

Proof usesMarginal of a latent-variable model · Parameters of a full-covariance Gaussian mixture · Validity of full-covariance Gaussian mixture parameters · Joint density of the full-covariance Gaussian mixture · Mean update of the full-covariance Gaussian mixture · Responsibilities of the full-covariance Gaussian mixture · Multivariate Gaussian density function · Weighted scatter matrices of points in general position are positive definite

Used byEM step for the full-covariance Gaussian mixture

DefinitionEM step for the full-covariance Gaussian mixture#✓fully proved

For data \(x_1, \dots, x_N \in \mathbb{R}^d\) in general position (at least one point, and not all in an affine hyperplane) and valid parameters \(\theta\), the EM step returns the M-step parameters of \(\theta\): with responsibilities \(r_{nk}\) under \(\theta\) and \(N_k = \sum_n r_{nk}\), the new weights are \(N_k / N\), the new means are the responsibility-weighted means and the new covariances are the responsibility-weighted sample covariances. General position makes these parameters valid.

noncomputable def emStep (hx : SpansAffinely xs) (θ : ValidParams d K) : ValidParams d K :=
  ⟨mStep xs θ, mStep_valid hx θ⟩

Uses 13 · Used by 3

Statement usesPosteriors are probability distributions · Marginal of a latent-variable model · Posterior of a latent-variable model · Parameters of a full-covariance Gaussian mixture · Validity of full-covariance Gaussian mixture parameters · Data that span the space affinely · Valid parameters of a full-covariance Gaussian mixture · Joint density of the full-covariance Gaussian mixture · M-step of the full-covariance Gaussian mixture · Effective number of points of a full-covariance mixture component · The covariance update is positive definite · Responsibilities of the full-covariance Gaussian mixture · Multivariate Gaussian density function

Used byThe M-step of the full-covariance Gaussian mixture maximizes the EM objective · The log-likelihood is monotone along the EM iterates of a full-covariance Gaussian mixture · Each EM step for the full-covariance Gaussian mixture does not decrease the log-likelihood

DefinitionComponent term of the EM objective for full-covariance Gaussian mixtures#✓fully proved

Given points \(x_1, \dots, x_N\) of \(\mathbb{R}^d\), valid parameters \(\theta\) of a \(K\)-component full-covariance Gaussian mixture, a component \(k\), a mean \(\mu \in \mathbb{R}^d\) and a real \(d \times d\) matrix \(S\), the component term is

\[ C_k(\mu, S) = \sum_n r_{nk} \log \mathcal{N}(x_n \mid \mu, S), \]

where \(r_{nk}\) is the responsibility of component \(k\) for \(x_n\) under \(\theta\) and \(\mathcal{N}(\cdot \mid \mu, S)\) is the multivariate Gaussian density with mean \(\mu\) and covariance matrix \(S\).

The matrix \(S\) is not required to be positive definite; the density is defined for every real matrix.

noncomputable def compTerm (θ : ValidParams d K) (k : Fin K) (μ : EuclideanSpace ℝ (Fin d))
    (S : Matrix (Fin d) (Fin d) ℝ) : ℝ :=
  ∑ n, resp θ (xs n) k * log (multivariateGaussianPDFReal μ S (xs n))

Uses 3 · Used by 3

Statement usesValid parameters of a full-covariance Gaussian mixture · Responsibilities of the full-covariance Gaussian mixture · Multivariate Gaussian density function

Used byThe mean and covariance updates maximize each component term · The EM objective of a full-covariance Gaussian mixture splits by component · The M-step of the full-covariance Gaussian mixture maximizes the EM objective

TheoremThe EM objective of a full-covariance Gaussian mixture splits by component#✓fully proved

Let \(x_1, \dots, x_N\) be points of \(\mathbb{R}^d\), and let \(\theta'\) and \(\theta\) be valid parameters of a \(K\)-component full-covariance Gaussian mixture, where \(\theta'\) has weights \(\pi_k'\), means \(\mu_k'\) and covariance matrices \(\Sigma_k'\). Then the EM objective of the mixture's joint density satisfies

\[ Q(\theta' \mid \theta) = \sum_k \bigl(N_k \log \pi_k' + C_k(\mu_k', \Sigma_k')\bigr), \]

where \(r_{nk}\) is the responsibility of component \(k\) for \(x_n\) under \(\theta\), \(N_k = \sum_n r_{nk}\) and \(C_k(\mu, S) = \sum_n r_{nk} \log \mathcal{N}(x_n \mid \mu, S)\), with \(\mathcal{N}(\cdot \mid \mu, S)\) the multivariate Gaussian density with mean \(\mu\) and covariance matrix \(S\).

theorem emQ_eq (θ' θ : ValidParams d K) :
    emQ joint xs θ' θ = ∑ k, (mass xs θ k * log (θ'.1.weight k) +
      compTerm xs θ k (θ'.1.mean k) (θ'.1.cov k))

Uses 10 · Used by 1

Statement usesThe EM objective · Parameters of a full-covariance Gaussian mixture · Validity of full-covariance Gaussian mixture parameters · Valid parameters of a full-covariance Gaussian mixture · Component term of the EM objective for full-covariance Gaussian mixtures · Joint density of the full-covariance Gaussian mixture · Effective number of points of a full-covariance mixture component

Proof usesPosterior of a latent-variable model · Responsibilities of the full-covariance Gaussian mixture · Multivariate Gaussian density function

Used byThe M-step of the full-covariance Gaussian mixture maximizes the EM objective

TheoremThe mean and covariance updates maximize each component term#✓fully proved

Let \(x_1, \dots, x_N \in \mathbb{R}^d\) be data in general position (at least one point, and not all in an affine hyperplane), let \(\theta\) be valid mixture parameters with responsibilities \(r_{nk}\), and fix a component \(k\). Write \(\mathcal{N}(x \mid \mu, S)\) for the multivariate Gaussian density and let \(\mu'_k\) and \(\Sigma'_k\) be the responsibility-weighted mean and the responsibility-weighted sample covariance of the data for component \(k\). Then for every \(\mu \in \mathbb{R}^d\) and every positive definite \(d \times d\) matrix \(S\),

\[\sum_n r_{nk} \log \mathcal{N}(x_n \mid \mu, S) \le \sum_n r_{nk} \log \mathcal{N}(x_n \mid \mu'_k, \Sigma'_k).\]

theorem compTerm_le {xs : Fin N → EuclideanSpace ℝ (Fin d)} (hx : SpansAffinely xs)
    (θ : ValidParams d K) (k : Fin K) (μ : EuclideanSpace ℝ (Fin d))
    {S : Matrix (Fin d) (Fin d) ℝ} (hS : S.PosDef) :
    compTerm xs θ k μ S ≤ compTerm xs θ k (newMean xs θ k) (newCov xs θ k)

Uses 12 · Used by 1

Statement usesData that span the space affinely · Valid parameters of a full-covariance Gaussian mixture · Component term of the EM objective for full-covariance Gaussian mixtures · Covariance update of the full-covariance Gaussian mixture · Mean update of the full-covariance Gaussian mixture

Proof usesMarginal of a latent-variable model · Parameters of a full-covariance Gaussian mixture · Validity of full-covariance Gaussian mixture parameters · Joint density of the full-covariance Gaussian mixture · Responsibilities of the full-covariance Gaussian mixture · Multivariate Gaussian density function · The weighted Gaussian MLE for points in general position

Used byThe M-step of the full-covariance Gaussian mixture maximizes the EM objective

TheoremThe weight update maximizes the weights term of the full-covariance mixture#✓fully proved

Let \((x_n)_{n\lt N}\) be data in \(\mathbb{R}^d\) with \(N > 0\), let \(\theta\) be valid parameters, and let \(N_k = \sum_n r_{nk}\), where \(r_{nk}\) is the responsibility of component \(k\) for \(x_n\). Then for all real weights \(w_k > 0\) with \(\sum_k w_k = 1\),

\[\sum_k N_k \log w_k \le \sum_k N_k \log \frac{N_k}{N}.\]

The proof is Gibbs' inequality.

theorem sum_mass_mul_log_le (hN0 : 0 < N) (θ : ValidParams d K) {w : Fin K → ℝ}
    (hw : ∀ k, 0 < w k) (hsum : ∑ k, w k = 1) :
    ∑ k, mass xs θ k * log (w k) ≤ ∑ k, mass xs θ k * log (mass xs θ k / N)

Uses 12 · Used by 1

Statement usesValid parameters of a full-covariance Gaussian mixture · Effective number of points of a full-covariance mixture component

Proof usesProbability distributions on a finite latent space · Posteriors are probability distributions · Marginal of a latent-variable model · Posterior of a latent-variable model · Gibbs' inequality (evidence lower bound form) · Parameters of a full-covariance Gaussian mixture · Validity of full-covariance Gaussian mixture parameters · Joint density of the full-covariance Gaussian mixture · Responsibilities of the full-covariance Gaussian mixture · Multivariate Gaussian density function

Used byThe M-step of the full-covariance Gaussian mixture maximizes the EM objective

TheoremThe M-step of the full-covariance Gaussian mixture maximizes the EM objective#✓fully proved

Let \(x_1, \dots, x_N \in \mathbb{R}^d\) be data in general position: \(N > 0\), and for every nonzero \(v \in \mathbb{R}^d\) the values \(\langle v, x_n \rangle\) are not all equal. Let \(\theta\) be valid parameters of a \(K\)-component full-covariance Gaussian mixture, and let \(\theta^+\) be the result of the EM step applied to \(\theta\). Then every valid parameter \(\theta'\) satisfies \(Q(\theta' \mid \theta) \le Q(\theta^+ \mid \theta)\), where \(Q\) is the EM objective of the mixture's joint density.

theorem emQ_le_emStep (hx : SpansAffinely xs) (θ' θ : ValidParams d K) :
    emQ joint xs θ' θ ≤ emQ joint xs (emStep xs hx θ) θ

Uses 12 · Used by 2

Statement usesThe EM objective · Data that span the space affinely · Valid parameters of a full-covariance Gaussian mixture · EM step for the full-covariance Gaussian mixture · Joint density of the full-covariance Gaussian mixture

Proof usesParameters of a full-covariance Gaussian mixture · Validity of full-covariance Gaussian mixture parameters · Component term of the EM objective for full-covariance Gaussian mixtures · The mean and covariance updates maximize each component term · The EM objective of a full-covariance Gaussian mixture splits by component · Effective number of points of a full-covariance mixture component · The weight update maximizes the weights term of the full-covariance mixture

Used byThe log-likelihood is monotone along the EM iterates of a full-covariance Gaussian mixture · Each EM step for the full-covariance Gaussian mixture does not decrease the log-likelihood

TheoremEach EM step for the full-covariance Gaussian mixture does not decrease the log-likelihood#✓fully proved

Each EM step for the full-covariance Gaussian mixture does not decrease the log-likelihood. Let \(x_1, \dots, x_N \in \mathbb{R}^d\) be data in general position (at least one point, and not all in an affine hyperplane) and let \(\theta\) be valid parameters. If \(\theta^{+}\) is the result of one EM step from \(\theta\), then \(\ell(\theta) \le \ell(\theta^{+})\), where \(\ell\) is the log-likelihood of the data under the mixture.

theorem logLik_le_emStep (hx : SpansAffinely xs) (θ : ValidParams d K) :
    logLik joint xs θ ≤ logLik joint xs (emStep xs hx θ)

Uses 10

Statement usesLog-likelihood of a latent-variable model · Data that span the space affinely · Valid parameters of a full-covariance Gaussian mixture · EM step for the full-covariance Gaussian mixture · Joint density of the full-covariance Gaussian mixture

Proof usesThe EM theorem · Parameters of a full-covariance Gaussian mixture · Validity of full-covariance Gaussian mixture parameters · The M-step of the full-covariance Gaussian mixture maximizes the EM objective · Multivariate Gaussian density function

TheoremThe log-likelihood is monotone along the EM iterates of a full-covariance Gaussian mixture#✓fully proved

The log-likelihood is monotone along the EM iterates of a full-covariance Gaussian mixture. Let \(x_1, \dots, x_N \in \mathbb{R}^d\) be data in general position: \(N > 0\), and for every nonzero \(v \in \mathbb{R}^d\) the values \(\langle v, x_n \rangle\) are not all equal. Let \(\theta_0\) be valid parameters of a \(K\)-component full-covariance Gaussian mixture, and let \(\theta_t\) be the result of \(t\) EM steps from \(\theta_0\). Then \(\ell(\theta_t)\) is nondecreasing in \(t \in \mathbb{N}\), where \(\ell\) is the log-likelihood of the data under the mixture's joint density.

theorem logLik_iterate_emStep_monotone (hx : SpansAffinely xs) (θ₀ : ValidParams d K) :
    Monotone fun t => logLik joint xs ((emStep xs hx)^[t] θ₀)

Uses 10

Statement usesLog-likelihood of a latent-variable model · Data that span the space affinely · Valid parameters of a full-covariance Gaussian mixture · EM step for the full-covariance Gaussian mixture · Joint density of the full-covariance Gaussian mixture

Proof usesEM iterates have monotone likelihood · Parameters of a full-covariance Gaussian mixture · Validity of full-covariance Gaussian mixture parameters · The M-step of the full-covariance Gaussian mixture maximizes the EM objective · Multivariate Gaussian density function

61 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.