Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.ols-regression

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

AHoF Ordinary Least Squares (simple linear regression): fit a line y = slope*x + intercept minimizing the sum of squared residuals. Setting the gradient of the squared-error loss to zero gives the CLOSED FORM: the slope is the covariance of x and y divided by the variance of x, slope covariance variance = covariance / variance and the intercept then centres the line through the means. This is the unique minimizer (the loss is convex), so no iteration is needed. Proved native and axiom-free: the slope as exact rational division of covariance by variance; a worked slope; and that when covariance equals variance the slope is 1 (x and y move together one-for-one). The covariance and variance computations (which need centred sums) are executable; what is proved is the normal-equation slope. 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.ols-regression` prints this classification.

Depends onmath.rational.division

ols/slope :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

ols/slope-example :
  → ols/slope 3 2 = 3/2

ols/unit-covariance-slope-one :
  → ols/slope 2 2 = 1