Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.z-score

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

AHoF Z-Score Standardization: rescale a feature to zero mean and unit standard deviation, z = (x - mean) / std-dev -- the standard preprocessing step that puts features on a comparable scale (essential for distance-based methods, gradient descent conditioning, and regularization) and expresses each value as a number of standard deviations from the mean. Writing the (absolute) deviation d = |x - mean|: z-score deviation std-dev = deviation / std-dev over exact rationals. Proved native and axiom-free: the z-score as exact rational division of the deviation by the standard deviation; a worked z-score; and that a value exactly one standard deviation from the mean has |z| = 1. The mean, the standard deviation, and the sign of the deviation are executable; what is proved is the standardizing division. 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.z-score` prints this classification.

Depends onmath.rational.division

z-score/z-score :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

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

z-score/one-sigma-z-one :
  → ols/slope 2 2 = 1