Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.mc-mean

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

AHoF O69 Uncertainty Propagation (Monte Carlo): propagate input uncertainty by sampling and averaging the outputs. The two-sample Monte Carlo mean estimator weights each sample equally: estimate s1 s2 = 1/2 * s1 + 1/2 * s2. Averaging samples 1/2 and 3/4 gives the mean 5/8; averaging 1/4 and 3/4 gives 1/2. Values are proved by cross-product equivalence. Proved native and axiom-free. 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.mc-mean` prints this classification.

mc-mean/estimate :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

mc-mean/sample-mean :
  → ℚ≥0

mc-mean/balanced-mean :
  → ℚ≥0

mc-mean/estimate-unfold :
  (s1 s2 : ℚ≥0)
  → mc-mean/estimate s1 s2 = 1/2 · s1 + 1/2 · s2

mc-mean/sample-mean-is-five-eighths :
  → mc-mean/sample-mean = 5/8

mc-mean/balanced-mean-is-half :
  → mc-mean/balanced-mean = 1/2

mc-mean/mc-mean :
  → proposition/conjunction (mc-mean/sample-mean = 5/8) (mc-mean/balanced-mean = 1/2)