Reference · Algorithm guarantees

rainbow.algorithms.proofs.cross-validation

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

K-fold cross-validation mean over exact rationals. Given the per-fold scores of an evaluated model, the cross-validation estimate is their mean: the sum of the fold scores divided by the fold count. This composes the exact-rational list sum (map then reduce) with exact rational division (AHoF V4) -- averaging the folds is the aggregation that turns per-fold evaluations into a single estimate. 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.cross-validation` prints this classification.

validation/cross-validation-total :
  (x₁ : List ℚ≥0)
  → ℚ≥0

validation/cross-validation-mean :
  (x₁ : List ℚ≥0) (x₂ : ℚ≥0)
  → ℚ≥0

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

validation/cross-validation-mean-unfold :
  (scores : List ℚ≥0) (count : ℚ≥0)
  → validation/cross-validation-mean scores count = nnrat/divide (estimation/log-likelihood-total scores) count