Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.bayes-net

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

AHoF D1 Bayesian Network Representation: the joint distribution factorizes as a product of conditional-probability factors; the joint mass of two factors is their product joint-factor a b = a * b. Proved native and axiom-free (worked masses by cross-product equivalence). Scope (measured by the kernel): this module has 3 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.bayes-net` prints this classification.

bayes-net/joint-factor :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

bayes-net/strong-factor :
  → ℚ≥0

bayes-net/weak-factor :
  → ℚ≥0

bayes-net/joint-factor-unfold :
  (a b : ℚ≥0)
  → baseline/contribution a b = a · b

bayes-net/strong-factor-is-one-eighth :
  → bayes-net/strong-factor = 1/8

bayes-net/weak-factor-is-one-sixteenth :
  → bayes-net/weak-factor = 1/16

bayes-net/combined :
  → proposition/conjunction (bayes-net/strong-factor = 1/8) (bayes-net/weak-factor = 1/16)