TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Holm step-down controls strong FWER

Statement

Let $m \geq 1$ and let a fixed finite family of null hypotheses and valid p-value statistics be as in Null-valid p-values and familywise and false-discovery error rates. For $α \in [0, 1]$ , let $R_{α} (X)$ be the rejected-index set from Holm step-down procedure, and let $I_{0} (θ)$ be the true-null index set defined there. By Holm rejection events are measurable, the rejection events are measurable, so the familywise error rate is well-defined as ${FWER}_{θ} = P_{θ} (R_{α} (X) \cap I_{0} (θ) \neq \emptyset) .$ Then ${FWER}_{θ} \leq α$ for every $θ \in Θ$ . This is strong familywise error control and requires no independence or other restriction on the joint distribution of the p-values.

Facts & Assumptions

Given: A statistical experiment, a fixed finite family with valid p-values in the sense of Null-valid p-values and familywise and false-discovery error rates, and $α \in [0, 1]$ . The Holm rejected set is the initial ordered prefix passing its step-down cutoffs.

[F1]

Null-valid p-values and familywise and false-discovery error rates: for each $i$ , validity means $P_{θ} (p_{i} (X) \leq u) \leq u$ for every $θ \in H_{0 i}$ and $u \in [0, 1]$ .

[F2]

Null-valid p-values and familywise and false-discovery error rates: $I_{0} (θ) = {i : θ \in H_{0 i}}$ and FWER is the probability of at least one rejected true null.

[F3]

Holm step-down procedure: the procedure orders p-values, compares rank $j$ with $α / (m - j + 1)$ , and rejects exactly the prefix whose comparisons all pass.

[F4]

Holm rejection events are measurable: each Holm rejection event is measurable, so the FWER definition in [F2] applies.

[F5]

Strong familywise error control by Bonferroni: the equal-weight one-step Bonferroni rule on any fixed family of $q \geq 1$ valid p-values has strong FWER at most $α$ when it rejects at cutoff $α / q$ , under arbitrary dependence.

Proof

technique · direct

1.1givenF2F3F4choosealgebra

Fix $θ$ and put $I_{0} = I_{0} (θ)$ and $m_{0} = ∣ I_{0} ∣$ . By [F4], the Holm rejection events are measurable, so the FWER from [F2] is defined. If $m_{0} = 0$ , no true null can be rejected. Otherwise, let $j_{0}$ be the least rank occupied by a true null in the ordering from [F3]; it exists because $I_{0}$ is finite and nonempty. Since [F3] rejects only a prefix, any rejection of a true null forces rank $j_{0}$ to be rejected. Thus $p_{π (j_{0})} (X) \leq α / (m - j_{0} + 1)$ . All $m_{0}$ true nulls occur at ranks $j_{0}, \dots, m$ , so $m - j_{0} + 1 \geq m_{0}$ and $α / (m - j_{0} + 1) \leq α / m_{0}$ . Hence any false rejection implies $⋃_{i \in I_{0}} {p_{i} (X) \leq α / m_{0}}$ .

2.1F1F2F5step 1.1algebra∎

If $m_{0} \geq 1$ , fix $θ$ and consider the fixed subfamily indexed by $I_{0} (θ)$ ; it has $m_{0}$ members, all true under this $θ$ , and it is not selected from the observed p-values. By [F1] its p-values are valid. Applying the Bonferroni theorem [F5] to this subfamily at level $α$ bounds the probability of its threshold-union event $⋃_{i \in I_{0}} {p_{i} (X) \leq α / m_{0}}$ by $α$ . This contains the Holm false-rejection event from step 1.1, so ${FWER}_{θ} \leq α$ . If $m_{0} = 0$ , step 1.1 gives FWER zero. Since $θ$ was arbitrary, the control is strong.

Depends on

Used by

Holm step-down versus one-step Bonferroni Example

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jelle J. Goeman and Aldo Solari, The sequential rejection principle of familywise error control, The Annals of Statistics 38(6) (2010), Theorem 1 and Section 3 (standard reference, not scraped)
Gary W. Oehlert, A First Course in Design and Analysis of Experiments, Chapter 5, Sections 5.1–5.2 (standard reference, not scraped)