Bonferroni correction

DefinitionBonferroni rejection set#✓fully proved

The hypotheses rejected by the Bonferroni procedure at level α: those whose p-value is at most α / m.

noncomputable def bonferroniRejections (α : ℝ) (p : Fin m → ℝ) : Finset (Fin m) :=
  Finset.univ.filter fun i => p i ≤ α / m

Used by 1

Used byThe Bonferroni procedure controls the FWER

TheoremUnion bound for valid p-values#✓fully proved

If every true-null p-value is valid and c ∈ [0, 1], the probability that some true null has p-value at most c is at most |H0| c. No independence is assumed.

theorem measure_exists_mem_le_le (μ : Measure Ω) (p : Fin m → Ω → ℝ) (H0 : Finset (Fin m))
    (hnull : ∀ i ∈ H0, IsValidPValue μ (p i)) {c : ℝ} (hc : c ∈ Set.Icc (0 : ℝ) 1) :
    μ {ω | ∃ i ∈ H0, p i ω ≤ c} ≤ ENNReal.ofReal (H0.card * c)

Uses 1 · Used by 3

Statement usesValid p-value

Used byBonferroni inequality · Level of the Bonferroni local test · Holm's procedure controls the FWER

TheoremBonferroni inequality#✓fully proved

If every true-null p-value is valid, the probability that some true null has p-value at most α / m is at most α |H0| / m, for α ∈ [0, 1]. No independence is assumed. (For m = 0 there is no hypothesis and both sides are 0.)

theorem measure_exists_le_div_le (μ : Measure Ω) (p : Fin m → Ω → ℝ) (H0 : Finset (Fin m))
    (hnull : ∀ i ∈ H0, IsValidPValue μ (p i)) {α : ℝ} (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1) :
    μ {ω | ∃ i ∈ H0, p i ω ≤ α / m} ≤ ENNReal.ofReal (α * H0.card / m)

Sources

• Bonferroni (1936); Dunn (1961).

Uses 2 · Used by 1

Statement usesValid p-value

Proof usesUnion bound for valid p-values

Used byThe Bonferroni procedure controls the FWER

TheoremThe Bonferroni procedure controls the FWER#✓fully proved

If every true-null p-value is valid, the probability that the Bonferroni procedure at level α ∈ [0, 1] rejects at least one true null is at most α.

theorem measure_bonferroni_familywiseError_le (μ : Measure Ω) (p : Fin m → Ω → ℝ)
    (H0 : Finset (Fin m)) (hnull : ∀ i ∈ H0, IsValidPValue μ (p i)) {α : ℝ} (hα₀ : 0 ≤ α)
    (hα₁ : α ≤ 1) :
    μ {ω | (bonferroniRejections α (fun i => p i ω) ∩ H0).Nonempty} ≤ ENNReal.ofReal α

Uses 3

Statement usesValid p-value · Bonferroni rejection set

Proof usesBonferroni inequality

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.