The hypergeometric distribution

Draw n of N objects without replacement, K of them marked. The number of marked objects among those drawn is hypergeometric: exactly k of them turn up in K.choose k * (N - K).choose (n - k) of the N.choose n draws. This file defines the distribution on Fin (N + 1) as a kernel from the number of marked objects to the number drawn.

Main definitions

• ProbabilityTheory.hypergeometricCount: the number of draws with k marked objects.
• ProbabilityTheory.hypergeometric: the kernel from the number of marked objects to the number of marked objects drawn.

Main results

• ProbabilityTheory.hypergeometric_real_singleton: the mass function, by Vandermonde's identity.
• ProbabilityTheory.hypergeometric_self: drawing every object is the identity kernel.
• ProbabilityTheory.posterior_hypergeometric_self: after drawing every object the posterior is the point mass at the number observed.

[UPSTREAM] candidate for Mathlib/Probability/Distributions/.

def ProbabilityTheory.hypergeometricCount (N K n k : ℕ) : ℕ

The number of ways to draw n of N objects, K of them marked, so that exactly k marked objects are drawn.

Equations

• ProbabilityTheory.hypergeometricCount N K n k = if k ≤ n then K.choose k * (N - K).choose (n - k) else 0

theorem ProbabilityTheory.hypergeometricCount_ne_zero_iff {N K n k : ℕ} : hypergeometricCount N K n k ≠ 0 ↔ k ≤ n ∧ k ≤ K ∧ n - k ≤ N - K

@[simp]

theorem ProbabilityTheory.hypergeometricCount_zero_zero (N K : ℕ) : hypergeometricCount N K 0 0 = 1

Drawing nothing is possible whatever the number of marked objects.

theorem ProbabilityTheory.hypergeometricCount_self {N K : ℕ} (hK : K ≤ N) (k : ℕ) : hypergeometricCount N K N k = if k = K then 1 else 0

Drawing every object yields exactly the marked ones.

theorem ProbabilityTheory.hypergeometricCount_top {N n : ℕ} (k : ℕ) : hypergeometricCount N N n k = if k = n then N.choose n else 0

When every object is marked, every object drawn is.

theorem ProbabilityTheory.sum_hypergeometricCount {N K n : ℕ} (hK : K ≤ N) (hn : n ≤ N) : ∑ k : Fin (N + 1), hypergeometricCount N K n ↑k = N.choose n

The draws are counted by the number of marked objects in them, by Vandermonde's identity.

noncomputable def ProbabilityTheory.hypergeometric (N n : ℕ) : Kernel (Fin (N + 1)) (Fin (N + 1))

The hypergeometric kernel sends the number of marked objects among N to the law of the number of marked objects among n drawn without replacement.

Equations

• ProbabilityTheory.hypergeometric N n = ProbabilityTheory.Kernel.ofWeights fun (K k : Fin (N + 1)) => ↑(ProbabilityTheory.hypergeometricCount N (↑K) n ↑k)

instance ProbabilityTheory.instIsFiniteKernelFinHAddNatOfNatHypergeometric (N n : ℕ) : IsFiniteKernel (hypergeometric N n)

theorem ProbabilityTheory.hypergeometric_self {N : ℕ} : hypergeometric N N = Kernel.id

Drawing every object reveals the number of marked ones.

theorem ProbabilityTheory.hypergeometric_last {N n : ℕ} (hn : n ≤ N) : (hypergeometric N n) (Fin.last N) = MeasureTheory.Measure.dirac ⟨n, ⋯⟩

When every object is marked, every object drawn is.

theorem ProbabilityTheory.hypergeometric_apply_singleton_ne_zero_iff {N n : ℕ} (K k : Fin (N + 1)) : ((hypergeometric N n) K) {k} ≠ 0 ↔ hypergeometricCount N (↑K) n ↑k ≠ 0

A number of marked draws is possible exactly when some draw has it.

theorem ProbabilityTheory.hypergeometric_real_singleton {N n : ℕ} (K k : Fin (N + 1)) (hn : n ≤ N) : ((hypergeometric N n) K).real {k} = ↑(hypergeometricCount N (↑K) n ↑k) / ↑(N.choose n)

The hypergeometric mass function.

theorem ProbabilityTheory.posterior_hypergeometric_self {N : ℕ} (K : Fin (N + 1)) (μ : MeasureTheory.Measure (Fin (N + 1))) [MeasureTheory.IsFiniteMeasure μ] (hμ : μ {K} ≠ 0) : (posterior (hypergeometric N N) μ) K = MeasureTheory.Measure.dirac K

After drawing every object, the posterior over the number of marked ones is the point mass at the number observed.