Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.central-difference

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

AHoF O2 Central Difference: the central finite difference estimates a derivative as (f(x+h) - f(x-h)) / (2h). What is defined here is only its NUMERATOR, the signed difference of the two evaluations: central-difference f-plus f-minus = f-plus - f-minus; the division by 2h is not performed. For f(x)=x^2 at x=1, h=1 the proved numerator is f(2)-f(0) = 4-0 = 4 (slope-example-is-4); the divided estimate would be 4/(2*1) = 2, which is not computed or proved here. Also proved: the symmetric pair 2-2 = 0 (symmetric-flat-is-0), and that central-difference unfolds to signed/subtract for all signed inputs (by reflexivity). Values proved by signed cross-product equivalence. Proved native and axiom-free. Requires signed/subtract, signed/from-nnrat, signed/equivalent (all in the D63 checkpoint). Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 1 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.central-difference` prints this classification.

central-diff/central-difference :
  (x₁ x₂ : ℚ)
  → ℚ

central-diff/slope-example :
  → ℚ

central-diff/symmetric-flat :
  → ℚ

central-diff/central-difference-unfold :
  (a b : ℚ)
  → bfgs/gradient-change a b = a - b

central-diff/slope-example-is-4 :
  → central-diff/slope-example = signed/from-nnrat 4

central-diff/symmetric-flat-is-0 :
  → bfgs/no-change = signed/from-nnrat 0