Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.ista

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

AHoF O-family ISTA (Iterative Shrinkage-Thresholding / proximal gradient): the standard first-order method for L1-regularized (LASSO) problems. Each iteration takes a gradient step on the smooth loss, then applies the proximal operator of the L1 penalty -- the soft-thresholding (shrinkage) operator, which drives small coefficients exactly to zero and thereby induces sparsity. A coefficient of magnitude m is shrunk to zero exactly when it does not exceed the threshold lambda (the step size times the regularization weight): shrinks-to-zero? m lambda = decide (m <= lambda) over exact-rational magnitudes. Proved native and axiom-free: the shrinkage test; the certificate that a zeroed coefficient really is within the threshold (m <= lambda as native nnrat/at-most) -- so soft-thresholding is exact; and that a coefficient above the threshold survives (is only shrunk, not zeroed). The gradient step and the shrinkage magnitude are executable; what is proved is the sparsity-inducing thresholding decision. Requires nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound (all in 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.ista` prints this classification.

ista/shrinks-to-zero? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

ista/small-coefficient-zeroed :
  → ce-is/elite? 1/4 1/2 = data/true

ista/zeroed-within-threshold :
  → 1/4 ≤ 1/2

ista/large-coefficient-survives :
  → ce-is/elite? 3/4 1/2 = data/false