Holm–Bonferroni method

DefinitionHolm's step-down count#✓fully proved

Holm's step-down count at level α: the largest r ∈ {0, …, m} such that for every k ∈ {1, …, r} the k-th smallest p-value is at most α / (m - k + 1), i.e. at least k p-values are at most α / (m - k + 1). (r = 0 always qualifies.)

noncomputable def holmIndex (α : ℝ) (p : Fin m → ℝ) : ℕ :=
  ((Finset.range (m + 1)).filter fun r : ℕ =>
    ∀ k ∈ Finset.Icc (1 : ℕ) r, k ≤ numBelow p (α / ((m : ℝ) - k + 1))).max' ⟨0, by simp; omega⟩

Uses 1 · Used by 8

Statement usesNumber of p-values below a threshold

Used byHolm's procedure is a closed test · Number of hypotheses rejected by Holm's procedure · Holm rejection bound for a set of hypotheses · Holm's step-down count is at most the number of tests · Hypotheses rejected by Holm's step-down procedure · Holm's count is the largest index where every step succeeds · Every step up to Holm's count succeeds · Holm's rejection set is closed under smaller p-values

DefinitionHypotheses rejected by Holm's step-down procedure#✓fully proved

The hypotheses rejected by Holm's step-down procedure at level α: those whose p-value is at most α / (m - r + 1) with r = holmIndex α p; these are the hypotheses with the r smallest p-values.

noncomputable def holmRejections (α : ℝ) (p : Fin m → ℝ) : Finset (Fin m) :=
  Finset.univ.filter fun i => p i ≤ α / ((m : ℝ) - holmIndex α p + 1)

Uses 1 · Used by 5

Statement usesHolm's step-down count

Used byHolm's procedure is a closed test · Number of hypotheses rejected by Holm's procedure · Holm rejection bound for a set of hypotheses · Holm's procedure controls the FWER · Holm's rejection set is closed under smaller p-values

TheoremHolm's step-down count is at most the number of tests#✓fully proved

Holm's step-down count is at most m.

theorem holmIndex_le (α : ℝ) (p : Fin m → ℝ) : holmIndex α p ≤ m

Uses 2 · Used by 1

Statement usesHolm's step-down count

Proof usesNumber of p-values below a threshold

Used byNumber of hypotheses rejected by Holm's procedure

TheoremEvery step up to Holm's count succeeds#✓fully proved

Every step up to Holm's count succeeds: for 1 ≤ k ≤ holmIndex α p, at least k p-values are at most α / (m - k + 1).

theorem le_numBelow_of_le_holmIndex {α : ℝ} {p : Fin m → ℝ} {k : ℕ} (hk₁ : 1 ≤ k)
    (hk : k ≤ holmIndex α p) : k ≤ numBelow p (α / ((m : ℝ) - k + 1))

Uses 2 · Used by 3

Statement usesHolm's step-down count · Number of p-values below a threshold

Used byHolm's procedure is a closed test · Number of hypotheses rejected by Holm's procedure · Holm rejection bound for a set of hypotheses

TheoremHolm's count is the largest index where every step succeeds#✓fully proved

Holm's count is the largest index up to which every step succeeds.

theorem le_holmIndex {α : ℝ} {p : Fin m → ℝ} {r : ℕ} (hr : r ≤ m)
    (h : ∀ k ∈ Finset.Icc (1 : ℕ) r, k ≤ numBelow p (α / ((m : ℝ) - k + 1))) :
    r ≤ holmIndex α p

Uses 2 · Used by 2

Statement usesHolm's step-down count · Number of p-values below a threshold

Used byHolm's procedure is a closed test · Number of hypotheses rejected by Holm's procedure

TheoremHolm's rejection set is closed under smaller p-values#✓fully proved

The rejection set is closed under smaller p-values.

theorem mem_holmRejections_of_le {α : ℝ} {p : Fin m → ℝ} {i j : Fin m} (hij : p i ≤ p j)
    (hj : j ∈ holmRejections α p) : i ∈ holmRejections α p

Uses 2 · Used by 1

Statement usesHypotheses rejected by Holm's step-down procedure

Proof usesHolm's step-down count

Used byHolm rejection bound for a set of hypotheses

TheoremNumber of hypotheses rejected by Holm's procedure#✓fully proved

Holm's procedure at level α ≥ 0 rejects exactly holmIndex α p hypotheses.

theorem card_holmRejections {α : ℝ} (hα : 0 ≤ α) (p : Fin m → ℝ) :
    (holmRejections α p).card = holmIndex α p

Uses 7 · Used by 2

Statement usesHolm's step-down count · Hypotheses rejected by Holm's step-down procedure

Proof usesHolm's step-down count is at most the number of tests · Holm's count is the largest index where every step succeeds · Every step up to Holm's count succeeds · Number of p-values below a threshold · Number of p-values below a threshold is monotone

Used byHolm's procedure is a closed test · Holm rejection bound for a set of hypotheses

TheoremHolm rejection bound for a set of hypotheses#✓fully proved

If Holm rejects a hypothesis in J, then some j ∈ J has p-value at most α / |J|: the first hypothesis of J in sorted order sits at a position k ≤ m - |J| + 1. This is the shared Holm rejection bound, used both for Holm's FWER control below and for identifying Holm's procedure with the closure of the Bonferroni local tests.

theorem exists_le_div_card_of_holmRejections {α : ℝ} (hα : 0 ≤ α)
    (p : Fin m → ℝ) (J : Finset (Fin m))
    (h : (holmRejections α p ∩ J).Nonempty) :
    ∃ j ∈ J, p j ≤ α / J.card

Uses 6 · Used by 2

Statement usesHypotheses rejected by Holm's step-down procedure

Proof usesNumber of hypotheses rejected by Holm's procedure · Holm's step-down count · Every step up to Holm's count succeeds · Holm's rejection set is closed under smaller p-values · Number of p-values below a threshold

Used byHolm's procedure is a closed test · Holm's procedure controls the FWER

TheoremHolm's procedure controls the FWER#✓fully proved

If every true-null p-value is valid, the probability that Holm's step-down procedure at level α ∈ [0, 1] rejects at least one true null is at most α. No independence is assumed.

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

Sources

• Holm (1979).

Uses 4

Statement usesValid p-value · Hypotheses rejected by Holm's step-down procedure

Proof usesHolm rejection bound for a set of hypotheses · Union bound for valid p-values

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.