Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.min-max-scaling

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

AHoF Min-Max Scaling (normalization): rescale a feature linearly to the unit interval [0, 1] by mapping the minimum to 0 and the maximum to 1, scaled offset range = (x - min) / (max - min), where offset = x - min and range = max - min. Unlike z-score standardization it bounds every value into [0, 1] (useful for image pixels, neural-net inputs, and bounded activations), at the cost of sensitivity to outliers. Proved native and axiom-free: the scaled value as exact rational division of the offset by the range; a worked scaling; and that the maximum (offset = range) maps to 1. The min, max, and offset computations are executable; what is proved is the normalizing 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.min-max-scaling` prints this classification.

Depends onmath.rational.division

min-max-scaling/scaled :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

min-max-scaling/scaled-example :
  → accuracy/accuracy 3 4 = 3/4

min-max-scaling/maximum-maps-to-one :
  → accuracy/accuracy 4 4 = 1