Reference · Algorithm guarantees

rainbow.algorithms.proofs.importance-sampling

Algorithm guaranteessrc/rainbow/algorithms/proofs/importance_sampling.clj3 definitions, 2 theorems

Likelihood-weighted (importance) sampling estimates over exact rationals. Each sample carries a likelihood weight and a value; the importance estimate is the weight-weighted sum of the values divided by the total weight -- normalizing by the total weight so that unnormalized likelihood weights still yield a proper estimate (AHoF D7). This composes exact-rational multiplication and addition (the weighted sum and total weight) with exact rational division (the normalization). Scope (measured by the kernel): this module has 2 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.importance-sampling` prints this classification.

estimation/weighted-sum :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

estimation/total-weight :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

estimation/importance-estimate :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

estimation/weighted-sum-unfold :
  (weight-a value-a weight-b value-b : ℚ≥0)
  → estimation/weighted-sum weight-a value-a weight-b value-b = weight-a · value-a + weight-b · value-b

estimation/importance-estimate-unfold :
  (weight-a value-a weight-b value-b : ℚ≥0)
  → estimation/importance-estimate weight-a value-a weight-b value-b = nnrat/divide (sum) (weight)
  where sum := estimation/weighted-sum weight-a value-a weight-b value-b
  where weight := estimation/total-weight weight-a weight-b