Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.maximum-likelihood

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/maximum_likelihood.clj4 definitions, 4 theorems

AHoF D10 worked maximum likelihood estimation over exact rationals. Two models are scored on a two-point data set by their per-datum log-likelihoods: model A scores 3/4 and 3/4 (total 3/2), model B scores 1/4 and 1/4 (total 1/2). Maximum likelihood prefers model A, since its total 3/2 is at least model B's 1/2. The totals are proved by cross-product equivalence and the preference by reflexivity of the decided comparison. Scope (measured by the kernel): this module has 4 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.maximum-likelihood` prints this classification.

ahof-d10/model-a-scores :
  → List ℚ≥0

ahof-d10/model-b-scores :
  → List ℚ≥0

ahof-d10/model-a-total :
  → ℚ≥0

ahof-d10/model-b-total :
  → ℚ≥0

ahof-d10/model-a-total-is-three-halves :
  → ahof-d10/model-a-total = 3/2

ahof-d10/model-b-total-is-one-half :
  → ahof-d10/model-b-total = 1/2

ahof-d10/mle-prefers-model-a :
  → bo/is-safe ahof-d10/model-a-total ahof-d10/model-b-total = data/true

ahof-d10/maximum-likelihood :
  → proposition/conjunction (ahof-d10/model-a-total = 3/2) (conjunction)
  where conjunction := proposition/conjunction (ahof-d10/model-b-total = 1/2) (bo/is-safe ahof-d10/model-a-total ahof-d10/model-b-total = data/true)