Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.adaptive-is

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

AHoF V28 Adaptive Importance Sampling: iteratively refine the proposal and reweight samples by the ratio of the target density to the current proposal density: reweight target proposal = target / proposal. The ratio reading holds only for a POSITIVE proposal density. nnrat/divide is totalised: a zero proposal is accepted and yields a junk value (its reciprocal maps the equivalent zeros 0/1 and 0/2 to 1 and 2), and that zero case lies outside the reweighting claim. Proved native and axiom-free: reweight unfolds to nnrat/divide for all inputs (by reflexivity, an unfolding and not a ratio claim), and the worked weights 1/2 / 1/4 = 2 and 1/4 / 1/4 = 1 via cross-product equivalence. Adaptive refinement of the proposal is not modelled here. 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.adaptive-is` prints this classification.

adaptive-is/reweight :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

adaptive-is/unequal-weight :
  → ℚ≥0

adaptive-is/equal-weight :
  → ℚ≥0

adaptive-is/reweight-unfold :
  (target proposal : ℚ≥0)
  → accuracy/accuracy target proposal = nnrat/divide target proposal

adaptive-is/unequal-is-two :
  → adaptive-is/unequal-weight = 2

adaptive-is/equal-is-one :
  → adaptive-is/equal-weight = 1