Exact test for Hardy–Weinberg equilibrium

DefinitionLevene's exact Hardy–Weinberg probability#✓fully proved

Levene's conditional probability of h heterozygotes among N diploid individuals given nA copies of allele A (and nB = 2N - nA of B) under Hardy–Weinberg equilibrium: N! nA! nB! 2^h / (nAA! h! nBB! (2N)!) with nAA = (nA - h) / 2, nBB = (nB - h) / 2, when h ≤ nA, h ≤ nB and nA - h is even, and 0 otherwise. The parameter domain is nA ≤ 2N; for nA > 2N the value is 0.

noncomputable def leveneProb (N nA h : ℕ) : ℝ :=
  if h ≤ nA ∧ h + nA ≤ 2 * N ∧ Even (nA - h) then
    (N.factorial * nA.factorial * (2 * N - nA).factorial * 2 ^ h : ℝ) /
      (((nA - h) / 2).factorial * h.factorial * ((2 * N - nA - h) / 2).factorial *
        (2 * N).factorial)
  else 0

Used by 2

Used byLevene's formula is the conditional law under random union of gametes · Normalization of Levene's distribution

DefinitionNumber of heterozygous individuals#✓fully proved

The number of heterozygous individuals when the A gametes occupy the slots s: individuals j carrying exactly one of the slots (j, 0), (j, 1).

def hetCount {N : ℕ} (s : Finset (Fin N × Fin 2)) : ℕ :=
  (univ.filter fun j : Fin N => ¬((j, 0) ∈ s ↔ (j, 1) ∈ s)).card

Used by 2

Used byLevene's formula is the conditional law under random union of gametes · Normalization of Levene's distribution

TheoremLevene's formula is the conditional law under random union of gametes#✓fully proved

Among the C(2N, nA) equally likely placements of the nA copies of A in the 2N gamete slots, the fraction with exactly h heterozygous individuals is leveneProb N nA h.

No hypothesis nA ≤ 2N is needed: for nA > 2N there is no placement and C(2N, nA) = 0, so the left side is 0 / 0 = 0, matching leveneProb N nA h = 0; the statement is meaningful for nA ≤ 2N. The uniform law on placements is taken as the model; deriving it from independent gametes conditioned on nA is not part of this file.

theorem card_hetCount_div_choose (N nA h : ℕ) :
    ((univ.filter fun s : Finset (Fin N × Fin 2) => s.card = nA ∧ hetCount s = h).card : ℝ) /
      (2 * N).choose nA = leveneProb N nA h

Sources

• Levene (1949); Wigginton, Cutler and Abecasis (2005).

Uses 2 · Used by 1

Statement usesNumber of heterozygous individuals · Levene's exact Hardy–Weinberg probability

Used byNormalization of Levene's distribution

TheoremNormalization of Levene's distribution#✓fully proved

For nA ≤ 2N the probabilities leveneProb N nA h over the admissible heterozygote counts h sum to one.

theorem sum_leveneProb {N nA : ℕ} (hnA : nA ≤ 2 * N) :
    ∑ h ∈ range (nA + 1), leveneProb N nA h = 1

Sources

• Levene (1949); Wigginton, Cutler and Abecasis (2005).

Uses 3

Statement usesLevene's exact Hardy–Weinberg probability

Proof usesLevene's formula is the conditional law under random union of gametes · Number of heterozygous individuals

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.