Hypergeometric distribution

DefinitionHypergeometric mass function#✓fully proved

The hypergeometric mass function: the probability C(K, k) C(N - K, n - k) / C(N, n) of drawing exactly k marked items in n draws without replacement from N items of which K are marked; it is 0 for k > n. The parameter domain is K ≤ N, n ≤ N; outside it the value is not a probability (N - K truncates, and C(N, n) = 0 makes it 0 for n > N).

noncomputable def hypergeometricReal (N K n k : ℕ) : ℝ :=
  if k ≤ n then (K.choose k * (N - K).choose (n - k) : ℝ) / N.choose n else 0

Used by 8

Used byHypergeometric distribution · Point masses of the hypergeometric distribution · Nonnegativity of the hypergeometric mass function · Hypergeometric mass vanishes above the number of draws · Hypergeometric mass vanishes above the number of marked items · Normalization · Mean · Fisher's exact conditional law

TheoremNonnegativity of the hypergeometric mass function#✓fully proved

The hypergeometric mass function is nonnegative.

theorem hypergeometricReal_nonneg (N K n k : ℕ) : 0 ≤ hypergeometricReal N K n k

Uses 1 · Used by 1

Statement usesHypergeometric mass function

Used byHypergeometric distribution

TheoremHypergeometric mass vanishes above the number of draws#✓fully proved

The hypergeometric mass function vanishes above the number of draws.

theorem hypergeometricReal_of_lt {N K n k : ℕ} (h : n < k) : hypergeometricReal N K n k = 0

Uses 1 · Used by 2

Statement usesHypergeometric mass function

Used byHypergeometric distribution · Fisher's exact conditional law

TheoremHypergeometric mass vanishes above the number of marked items#✓fully proved

The hypergeometric mass function vanishes above the number of marked items.

theorem hypergeometricReal_of_lt' {N K n k : ℕ} (h : K < k) :
    hypergeometricReal N K n k = 0

Uses 1

Statement usesHypergeometric mass function

TheoremNormalization#✓fully proved

For K ≤ N and n ≤ N the hypergeometric probabilities sum to one; this is Vandermonde's identity ∑ₖ C(K, k) C(N - K, n - k) = C(N, n).

theorem sum_hypergeometricReal {N K n : ℕ} (hK : K ≤ N) (hn : n ≤ N) :
    ∑ k ∈ range (n + 1), hypergeometricReal N K n k = 1

Uses 1 · Used by 1

Statement usesHypergeometric mass function

Used byHypergeometric distribution

TheoremMean#✓fully proved

For 0 < N, K ≤ N and n ≤ N the hypergeometric law has mean n K / N.

theorem sum_mul_hypergeometricReal {N K n : ℕ} (hN : 0 < N) (hK : K ≤ N) (hn : n ≤ N) :
    ∑ k ∈ range (n + 1), (k : ℝ) * hypergeometricReal N K n k = n * K / N

Uses 1

Statement usesHypergeometric mass function

DefinitionHypergeometric distribution#✓fully proved

The hypergeometric law on ℕ with population size N, K ≤ N marked items, and n ≤ N draws without replacement.

noncomputable def hypergeometric (N K n : ℕ) (hK : K ≤ N) (hn : n ≤ N) : PMF ℕ :=
  PMF.ofFinset (fun k => ENNReal.ofReal (hypergeometricReal N K n k)) (range (n + 1))
    (by
      rw [← ENNReal.ofReal_sum_of_nonneg fun k _ => hypergeometricReal_nonneg N K n k,
        sum_hypergeometricReal hK hn, ENNReal.ofReal_one])
    (fun k hk => by
      rw [hypergeometricReal_of_lt (by simpa [Nat.lt_succ_iff] using hk), ENNReal.ofReal_zero])

Uses 4 · Used by 1

Statement usesHypergeometric mass function · Nonnegativity of the hypergeometric mass function · Hypergeometric mass vanishes above the number of draws · Normalization

Used byPoint masses of the hypergeometric distribution

TheoremPoint masses of the hypergeometric distribution#✓fully proved

The mass of k under hypergeometric N K n is hypergeometricReal N K n k.

theorem hypergeometric_apply {N K n : ℕ} (hK : K ≤ N) (hn : n ≤ N) (k : ℕ) :
    hypergeometric N K n hK hn k = ENNReal.ofReal (hypergeometricReal N K n k)

Uses 2

Statement usesHypergeometric distribution · Hypergeometric mass function

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.