Probability Distributions

@cite{goodman-stuhlmuller-2013} @cite{herbstritt-franke-2019}

General-purpose discrete probability distributions used across RSA models.

Hypergeometric Distribution

The hypergeometric distribution describes sampling without replacement from a finite population. It is the observation model in urn-based RSA scenarios:

P(k | N, K, n) = C(K, k) · C(N−K, n−k) / C(N, n)

where N = population size, K = success states, n = draws, k = observed successes.

Used by:

• @cite{goodman-stuhlmuller-2013}: speaker observation of 3 objects (N=3)
• @cite{herbstritt-franke-2019}: urn-based probability expressions (N=10)

The general formula replaces paper-specific match tables (e.g., obsPriorTable in GoodmanStuhlmuller2013.lean), enabling reuse across RSA models with different population sizes.

def Core.Distributions.hypergeometric (N K n k : ℕ) : ℚ

Hypergeometric PMF: probability of drawing exactly k successes in n draws without replacement from a population of N items containing K successes.

P(k | N, K, n) = C(K, k) · C(N−K, n−k) / C(N, n)

Returns 0 for impossible combinations (k > K, k > n, n−k > N−K, n > N) because Nat.choose a b = 0 when b > a. Division by zero (when n > N) yields 0 in ℚ, which is the correct probability.

Equations

• Core.Distributions.hypergeometric N K n k = ↑(K.choose k * (N - K).choose (n - k)) / ↑(N.choose n)

theorem Core.Distributions.hypergeometric_nonneg (N K n k : ℕ) : 0 ≤ hypergeometric N K n k

Hypergeometric probabilities are non-negative.