Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.r-squared

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/r_squared.clj1 definitions, 2 theorems

AHoF R-squared (coefficient of determination): summarize how well a regression fits by the FRACTION of the total variance in the target that the model explains, r-squared explained-variance total-variance = explained-variance / total-variance = SS_regression / SS_total = 1 - SS_residual / SS_total. It ranges in [0, 1] for a least-squares fit: 1 means the model explains all variance (perfect fit), 0 means it does no better than predicting the mean. Proved native and axiom-free: R-squared as exact rational division of explained by total variance; a worked value; and that a model explaining all the variance (explained = total) has R-squared = 1. The sum-of-squares computations are executable; what is proved is the explained-variance fraction. Requires nnrat/divide (division is the rational-division capability, composed here), nnrat/equivalent, and the D63 checkpoint. Scope (measured by the kernel): this module has 2 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.r-squared` prints this classification.

Depends onmath.rational.division

r-squared/r-squared :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

r-squared/r-squared-example :
  → ols/slope 3 4 = 3/4

r-squared/perfect-fit-r-squared-one :
  → ols/slope 5 5 = 1