Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.mse

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/mse.clj2 definitions, 3 theorems

AHoF Mean Squared Error: the standard loss for regression and the objective of least-squares fitting -- the average of the squared prediction errors, squared-error e = e * e mse e0 e1 = (e0*e0 + e1*e1) / 2 (a two-sample average). Squaring penalizes large errors quadratically and makes the loss smooth and convex in the predictions (for a linear model), which is why its gradient drives least-squares and neural-network training. Proved native and axiom-free: the squared-error term; a worked squared error; the two-sample mean squared error composing squares, a sum, and exact rational division; and a worked MSE. The residual (y - y_hat) computation is executable; what is proved is the squared error and its average. Requires nnrat/multiply, nnrat/add, nnrat/divide (division is the rational-division capability, composed here), and the D63 checkpoint. Scope (measured by the kernel): this module has 3 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.mse` prints this classification.

Depends onmath.rational.division

mse/squared-error :
  (x₁ : ℚ≥0)
  → ℚ≥0

mse/mse :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

mse/squared-error-example :
  → mse/squared-error 3 = 9

mse/mse-example :
  → mse/mse 2 1 = 5/2

mse/perfect-fit-zero-loss :
  → mse/squared-error 0 = 0