Theorem 24.3: the EM procedure never decreases the log-likelihood, L(θ⁽ᵗ⁺¹⁾) ≥ L(θ⁽ᵗ⁾)

Proved

UnderstandingML.em_monotone

by naimengye · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

expectation-maximizationlatent-variablesmonotonicity

Theorem 24.3. The EM procedure never decreases the log-likelihood; namely, for all $t$ , $L(\theta^{(t+1)}) \ge L(\theta^{(t)})$ .

Formally: for a positive parametric joint $P_\theta[X = x, Y = y]$ (so every logarithm is genuine), a sample, and any run of EM in which each M-step returns some maximizer of $F(Q^{(t+1)}, \cdot)$ .

Preamble

import Definitions.Def_UnderstandingML_Generative

open MeasureTheory ProbabilityTheory
open scoped InnerProductSpace

Formal statement

namespace UnderstandingML

/-- **Theorem 24.3** (p. 352). The EM procedure never decreases the log-likelihood; namely, for
all `t`, `L(θ⁽ᵗ⁺¹⁾) ≥ L(θ⁽ᵗ⁾)`. The joint `P_θ[X = x, Y = y]` is positive, so that all
logarithms are genuine. -/
theorem em_monotone {Θ X : Type*} {k m : ℕ} (p : Θ → X → Fin k → ℝ)
    (hp : ∀ θ x y, 0 < p θ x y) (x : Fin m → X) (θ : ℕ → Θ) (hθ : IsEMSequence p x θ) (t : ℕ) :
    latentLogLik p x (θ t) ≤ latentLogLik p x (θ (t + 1)) := by sorry

end UnderstandingML

Source

Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014, doi:10.1017/CBO9781107298019, §24.4.1 p. 352, Theorem 24.3 with its proof

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Confirmed by the moderator at approval.
Endorsed by naimengye · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph