Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.gradient-ascent

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

AHoF D49 worked bounded fixed-rate gradient-ascent instance. A constant unit gradient with rate 1/2 from the origin produces the exact rational trajectory 1/2, 1, 3/2 over three steps. The schedule-prefix recurrence reuses the generic gradient-ascent engine; the worked values are exact-rational equivalences proved by cross-product reflexivity. 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.gradient-ascent` prints this classification.

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

ahof-d49/rate :
  → ℚ≥0

ahof-d49/initial :
  → ℚ≥0

ahof-d49/trajectory :
  (x₁ : ℕ)
  → ℚ≥0

ahof-d49/gradient-ascent-recurrence :
  → proposition/conjunction (iterate = ahof-d49/initial) (∀ (steps : ℕ), optimization/nnrat-ascent-iterate ahof-d49/gradient ahof-d49/rate (data/succ steps) ahof-d49/initial = (fun x₂ => fun previous => step previous) steps (optimization/nnrat-ascent-iterate ahof-d49/gradient ahof-d49/rate steps ahof-d49/initial))
  where iterate := optimization/nnrat-ascent-iterate ahof-d49/gradient ahof-d49/rate 0 ahof-d49/initial
  where step := optimization/nnrat-ascent-step ahof-d49/gradient ahof-d49/rate

ahof-d49/worked-trajectory :
  → proposition/conjunction (iterate = nnrat/half) (conjunction)
  where conjunction := proposition/conjunction (optimization/nnrat-ascent-iterate ahof-d49/gradient ahof-d49/rate 2 ahof-d49/initial = 1) (optimization/nnrat-ascent-iterate ahof-d49/gradient ahof-d49/rate 3 ahof-d49/initial = 3/2)
  where iterate := optimization/nnrat-ascent-iterate ahof-d49/gradient ahof-d49/rate 1 ahof-d49/initial

ahof-d49/gradient-ascent :
  → proposition/conjunction (proposition/conjunction (iterate = ahof-d49/initial) (∀ (steps : ℕ), optimization/nnrat-ascent-iterate ahof-d49/gradient ahof-d49/rate (data/succ steps) ahof-d49/initial = (fun x₄ => fun previous => step previous) steps (optimization/nnrat-ascent-iterate ahof-d49/gradient ahof-d49/rate steps ahof-d49/initial))) (conjunction)
  where conjunction := proposition/conjunction (optimization/nnrat-ascent-iterate ahof-d49/gradient ahof-d49/rate 1 ahof-d49/initial = nnrat/half) (proposition/conjunction (optimization/nnrat-ascent-iterate ahof-d49/gradient ahof-d49/rate 2 ahof-d49/initial = 1) (optimization/nnrat-ascent-iterate ahof-d49/gradient ahof-d49/rate 3 ahof-d49/initial = 3/2))
  where iterate := optimization/nnrat-ascent-iterate ahof-d49/gradient ahof-d49/rate 0 ahof-d49/initial
  where step := optimization/nnrat-ascent-step ahof-d49/gradient ahof-d49/rate