Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.importance-sampling

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

AHoF D7 worked likelihood-weighted (importance) sampling over exact rationals. Two samples carry unnormalized likelihood weights 3 and 1 and values 1 and 0. The weighted sum is 3 * 1 + 1 * 0 = 3 and the total weight is 3 + 1 = 4, so the importance estimate is 3 / 4 -- the normalization by the total weight matters because the weights do not sum to one. The 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.importance-sampling` prints this classification.

ahof-d7/sample-weighted-sum :
  → ℚ≥0

ahof-d7/sample-total-weight :
  → ℚ≥0

ahof-d7/sample-estimate :
  → ℚ≥0

ahof-d7/weighted-sum-is-three :
  → ahof-d7/sample-weighted-sum = 3

ahof-d7/total-weight-is-four :
  → ahof-d7/sample-total-weight = 4

ahof-d7/estimate-is-three-quarters :
  → ahof-d7/sample-estimate = 3/4

ahof-d7/importance-sampling :
  → proposition/conjunction (ahof-d7/sample-weighted-sum = 3) (conjunction)
  where conjunction := proposition/conjunction (ahof-d7/sample-total-weight = 4) (ahof-d7/sample-estimate = 3/4)