Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.nesterov

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/nesterov.clj5 definitions, 4 theorems

AHoF O20 worked Nesterov accelerated momentum over signed rationals. Momentum coefficient 1, rate 1, and a position-dependent gradient (the positive part of the point), starting from position 1 and velocity 1. The look-ahead point is `1 + 1 * 1 = 2`, so the gradient there is 2 (not the 1 it would be at the current point), giving velocity `1 * 1 - 1 * 2 = -1` and position `1 + (-1) = 0`. Plain Polyak momentum, evaluating the gradient at the current point, would instead give velocity 0 and position 1 -- so the look-ahead genuinely changes the trajectory. The signed values are proved by cross-product equivalence. Scope (measured by the kernel): this module has 4 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.nesterov` prints this classification.

ahof-o20/beta :
  → ℚ≥0

ahof-o20/rate :
  → ℚ≥0

ahof-o20/gradient :
  (x₁ : ℚ)
  → ℚ≥0

ahof-o20/initial :
  → data/Product ℚ ℚ

ahof-o20/trajectory :
  (x₁ : ℕ)
  → data/Product ℚ ℚ

ahof-o20/first-velocity-is-negative-one :
  → product/second ℚ ℚ (iterate) = signed/make 0 1
  where iterate := optimization/nesterov-iterate ahof-o20/beta ahof-o20/beta ahof-o20/gradient 1 ahof-o20/initial

ahof-o20/first-position-is-zero :
  → product/first ℚ ℚ (iterate) = signed/from-nnrat 0
  where iterate := optimization/nesterov-iterate ahof-o20/beta ahof-o20/beta ahof-o20/gradient 1 ahof-o20/initial

ahof-o20/nesterov-recurrence :
  → proposition/conjunction (iterate = ahof-o20/initial) (iterate₁ = step)
  where iterate := optimization/nesterov-iterate ahof-o20/beta ahof-o20/beta ahof-o20/gradient 0 ahof-o20/initial
  where iterate₁ := optimization/nesterov-iterate ahof-o20/beta ahof-o20/beta ahof-o20/gradient 1 ahof-o20/initial
  where step := optimization/nesterov-step ahof-o20/beta ahof-o20/beta ahof-o20/gradient ahof-o20/initial

ahof-o20/nesterov :
  → proposition/conjunction (second = signed/make 0 1) (conjunction)
  where conjunction := proposition/conjunction (product/first ℚ ℚ (optimization/nesterov-iterate ahof-o20/beta ahof-o20/beta ahof-o20/gradient 1 ahof-o20/initial) = signed/from-nnrat 0) (proposition/conjunction (optimization/nesterov-iterate ahof-o20/beta ahof-o20/beta ahof-o20/gradient 0 ahof-o20/initial = ahof-o20/initial) (optimization/nesterov-iterate ahof-o20/beta ahof-o20/beta ahof-o20/gradient 1 ahof-o20/initial = optimization/nesterov-step ahof-o20/beta ahof-o20/beta ahof-o20/gradient ahof-o20/initial))
  where second := product/second ℚ ℚ (optimization/nesterov-iterate ahof-o20/beta ahof-o20/beta ahof-o20/gradient 1 ahof-o20/initial)