Reference · Algorithm guarantees
rainbow.algorithms.proofs.composite-metric
Composite evaluation metrics over exact rationals. A composite metric is a weighted combination of atomic metrics: given weights and atomic metric values, the composite is `w1 * m1 + w2 * m2`. This composes exact-rational multiplication and addition to aggregate several atomic metrics into one score (AHoF V5). When the weights sum to one the composite is a weighted average of the metrics. Scope (measured by the kernel): this module has 1 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.composite-metric` prints this classification.
validation/composite-metric
validation/composite-metric : (x₁ x₂ x₃ x₄ : ℚ≥0) → ℚ≥0
ℚ≥0 = nnrat/NonnegativeRational
validation/composite-metric-unfold
validation/composite-metric-unfold : (weight-a metric-a weight-b metric-b : ℚ≥0) → estimation/weighted-sum weight-a metric-a weight-b metric-b = weight-a · metric-a + weight-b · metric-b
+ = nnrat/add= = equality/Eq· = nnrat/multiplyℚ≥0 = nnrat/NonnegativeRational