Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.hypothesis-test

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

AHoF Statistical Hypothesis Testing (z-test / critical-value decision): decide whether observed data are inconsistent with a null hypothesis at a chosen significance level. Having computed a test statistic (e.g. a z-score) and the critical value for the significance level alpha, the null is REJECTED exactly when the statistic reaches the critical value: reject-null? statistic critical = decide (critical <= statistic) over exact-rational values. Proved native and axiom-free: the rejection decision; that a statistic in the critical region rejects the null; the certificate that a rejection really means the statistic met the critical value (native nnrat/at-most) -- so the Type-I error rate is controlled at alpha; and that a statistic below the critical value fails to reject (insufficient evidence). The statistic and critical-value computation are executable; what is proved is the reject/fail-to-reject decision. Requires nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound (all in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.hypothesis-test` prints this classification.

hypothesis-test/reject-null? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

hypothesis-test/rejects-in-critical-region :
  → bo/is-safe 3 2 = data/true

hypothesis-test/rejection-meets-critical :
  → 2 ≤ 3

hypothesis-test/fails-to-reject :
  → bo/is-safe 1 2 = data/false