Fisher's exact test

TheoremSum of independent binomials#✓fully proved

If X ~ Bin(n₁, p) and Y ~ Bin(n₂, p) are independent, then X + Y ~ Bin(n₁ + n₂, p): P(X + Y = t) = C(n₁ + n₂, t) p^t (1 - p)^(n₁ + n₂ - t).

theorem measureReal_add_eq_binomial (hXm : Measurable X) (hYm : Measurable Y)
    (hX : HasLaw X Bin(n₁, p) μ) (hY : HasLaw Y Bin(n₂, p) μ) (hXY : IndepFun X Y μ) (t : ℕ) :
    μ.real {ω | X ω + Y ω = t} = Bin(n₁ + n₂, p).real {t}

Used by 1

Used byFisher's exact conditional law

TheoremFisher's exact conditional law#✓fully proved

Let X ~ Bin(n₁, p) and Y ~ Bin(n₂, p) be independent with a common p ∈ (0, 1). Given the margin X + Y = t with t ≤ n₁ + n₂, the cell X is hypergeometric: P(X = k | X + Y = t) = C(n₁, k) C(n₂, t - k) / C(n₁ + n₂, t), whatever p.

theorem cond_measureReal_eq_hypergeometricReal (hp₀ : 0 < p) (hp₁ : p < 1)
    (hXm : Measurable X) (hYm : Measurable Y) (hX : HasLaw X Bin(n₁, p) μ)
    (hY : HasLaw Y Bin(n₂, p) μ) (hXY : IndepFun X Y μ) {t : ℕ} (ht : t ≤ n₁ + n₂) (k : ℕ) :
    (μ[|{ω | X ω + Y ω = t}]).real {ω | X ω = k} = hypergeometricReal (n₁ + n₂) n₁ t k

Sources

• Fisher (1934, §21.02; 1935); Lehmann–Romano (2005), §4.5.

Uses 3

Statement usesHypergeometric mass function

Proof usesSum of independent binomials · Hypergeometric mass vanishes above the number of draws

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.