Reference · Algorithm guarantees

rainbow.algorithms.proofs.maximum-likelihood

Algorithm guaranteessrc/rainbow/algorithms/proofs/maximum_likelihood.clj2 definitions, 2 theorems

Maximum likelihood estimation over exact rationals. The log-likelihood of a model on a data set is the sum of the per-datum log-likelihoods (map then reduce); maximum likelihood estimation selects the model whose total log-likelihood is largest. This composes the exact-rational list sum with the decidable rational comparison (AHoF D10): scoring each model by its total log-likelihood and preferring the higher-scoring one. Scope (measured by the kernel): this module has 2 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.maximum-likelihood` prints this classification.

estimation/log-likelihood-total :
  (x₁ : List ℚ≥0)
  → ℚ≥0

estimation/mle-prefers :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

estimation/log-likelihood-total-unfold :
  (scores : List ℚ≥0)
  → estimation/log-likelihood-total scores = list/nnrat-map-sum ℚ≥0 (fun score => score) scores

estimation/mle-prefers-unfold :
  (total-a total-b : ℚ≥0)
  → estimation/mle-prefers total-a total-b = audit/decide-nnrat-at-most total-b total-a