Reference · Foundations

rainbow.math.monte-carlo-estimation

Foundationssrc/rainbow/math/monte_carlo_estimation.clj3 definitions, 3 theorems

Direct Monte Carlo estimation of a failure probability. Given a finite list of sample outcomes (a boolean flag per sample, true = failure), the empirical failure frequency is the count of failures over the sample size, an exact rational. The count reduces a boolean indicator over the list; the estimate is a nonnegative rational.

estimation/nnrat-indicator :
  (x₁ : data/Bool)
  → ℕ

estimation/failure-count :
  (x₁ : List data/Bool)
  → ℕ

estimation/monte-carlo-frequency :
  (x₁ : List data/Bool) (x₂ : ℕ)
  → ℚ≥0

estimation/indicator-failure :
  → estimation/nnrat-indicator data/true = 1

estimation/indicator-success :
  → estimation/nnrat-indicator data/false = 0

estimation/count-empty :
  → estimation/failure-count [] = 0