TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Benjamini–Hochberg FDR under independence

Statement

Let $E = ((X, A), Θ, (P_{θ})_{θ \in Θ})$ be a statistical experiment, let $m \geq 1$ , and fix a prespecified family of nonempty null hypotheses $H_{01}, \dots, H_{0 m} \subseteq Θ$ with valid p-value statistics $p_{i} : X \to [0, 1]$ . For each $θ$ , put

$I_{0} (θ) = {i : θ \in H_{0 i}}, m_{0} (θ) = ∣ I_{0} (θ) ∣ .$

Suppose that under every $P_{θ}$ the $m$ p-values are mutually independent and that

$P_{θ} ({x \in X : p_{i} (x) \leq u}) = u (i \in I_{0} (θ), 0 \leq u \leq 1) .$

False-null p-value laws may otherwise be arbitrary. For every $q \in (0, 1)$ , the BH rule in Benjamini–Hochberg step-up procedure satisfies

${FDR}_{θ} = \frac{m_{0} (θ)}{m} q \leq q .$

This is an FDR guarantee; no FWER bound is asserted.

Facts & Assumptions

Given: The fixed finite family and statistical experiment in the Statement, $q \in (0, 1)$ , and the stated independence and exact-uniformity conditions under each $P_{θ}$ .

[F1]

False discovery proportion, FDR, and FWER: for true-null index set $I_{0}$ , $V$ counts rejected true nulls, $R$ is the number rejected, and $FDR = E [V / (R \lor 1)]$ .

[F2]

Benjamini–Hochberg step-up procedure: for sorted values $p_{(k)}$ , BH takes the largest $R$ with $p_{(R)} \leq R q / m$ and rejects the first $R$ ranks.

[F3]

Valid p-values: a p-value statistic is a measurable statistic into $[0, 1]$ ; validity requires $P_{θ} (p_{i} \leq u) \leq u$ under every null law.

[F4]

Independent random elements: random elements on one probability space are independent when their generated sigma-algebras are independent.

[F5]

Disjoint groups of an independent sigma-algebra family remain independent: disjoint groups of an independent family of sigma-algebras remain independent after taking the sigma-algebras they generate.

[F6]

Independent random elements have product joint law: a finite independent family of random elements has joint law equal to the finite product of its marginal laws.

[F7]

Leave-one-out identity for the BH step-up rule: for each $i$ , the leave-one-out variable $S_{i}$ is measurable with respect to the other p-values, and $I_{i} / (R \lor 1) = 1 {p_{i} \leq (S_{i} + 1) q / m} / (S_{i} + 1)$ .

[F8]

The expectation of an indicator is the probability of the event: for every event $A$ , $E [1_{A}] = P (A)$ .

[F9]

Linearity, monotonicity, and the modulus bound for expectation: finite sums of integrable random variables have expectation equal to the sum of their expectations.

[F10]

Expectation of a nonnegative or integrable random variable: expectation is the integral against the specified probability law.

[A1]

For every fixed $θ$ , the p-values are mutually independent under $P_{θ}$ , and each $i \in I_{0} (θ)$ has the exact uniform law, so $P_{θ} ({x \in X : p_{i} (x) \leq u}) = u$ on $[0, 1]$ .

Proof

1.1givenA1F2F3F4F5F6F7choose

Fix $θ$ and work on the probability space $(X, A, P_{θ})$ , regarding each $P_{i} : = p_{i}$ as a random element; [F3] makes these functions measurable. For $k \in {1, \dots, m}$ and $a \in R$ , ${P_{(k)} \leq a} = ⋃_{J \subseteq [m], ∣ J ∣ = k} ⋂_{j \in J} {P_{j} \leq a}$ , so each rank-threshold event is measurable. The events ${R = r}$ are finite Boolean combinations of the rank-threshold events, so $R$ is measurable. If $0 < R < m$ , maximality in [F2] gives $P_{(R)} \leq R q / m$ and $P_{(R + 1)} > (R + 1) q / m > R q / m$ , so the rejected hypotheses are exactly those with $P_{i} \leq R q / m$ . If $R = m$ , all values are at most $q = R q / m$ ; if $R = 0$ , no value is zero because then rank $1$ would qualify. Hence the same characterization holds in every case. The rejection events are measurable because ${P_{i} \leq R q / m} = ⋃_{r = 0}^{m} ({R = r} \cap {P_{i} \leq r q / m})$ , so the BH rule is a measurable map into the finite set $2^{[m]}$ . Now fix $i \in I_{0} (θ)$ . [A1] and [F4] give independence; [F5] groups $P_{i}$ and the remaining $P_{j}$ , while [F7] makes $S_{i}$ measurable with respect to the latter group. Thus $P_{i}$ and $S_{i}$ are independent random elements, and [F6] gives their product joint law.

2.1A1F6step 1.1algebra

For $r \in {0, \dots, m - 1}$ put $t_{r} = (r + 1) q / m \leq q < 1$ . By [A1], $P_{θ} (P_{i} \leq t_{r}) = t_{r}$ ; independence from step 1.1 and the product law [F6] give $P_{θ} (P_{i} \leq t_{r}, S_{i} = r) = t_{r} P_{θ} (S_{i} = r)$ .

3.1F7F8F9F10step 2.1algebra

By [F7], partitioning on the finite-valued $S_{i}$ expresses $I_{i} / (R \lor 1)$ as $\sum_{r = 0}^{m - 1} 1 {P_{i} \leq t_{r}, S_{i} = r} / (r + 1)$ . Each event is measurable, and [F8] and [F10] give the absolute expectation of its summand as $P_{θ} (P_{i} \leq t_{r}, S_{i} = r) / (r + 1) \leq 1$ , so each summand is integrable. Then [F8], [F9], and step 2.1 give $E_{θ} [I_{i} / (R \lor 1)] = \sum_{r = 0}^{m - 1} t_{r} P_{θ} (S_{i} = r) / (r + 1) = (q / m) \sum_{r = 0}^{m - 1} P_{θ} (S_{i} = r) = q / m$ .

4.1F1F9step 1.1step 3.1algebra∎

The measurable BH rejection rule from step 1.1 lets us apply [F1] with $P = P_{θ}$ and $I_{0} = I_{0} (θ)$ . Thus $V = \sum_{i \in I_{0} (θ)} I_{i}$ and ${FDR}_{θ} = E_{θ} [V / (R \lor 1)]$ ; repeated finite linearity [F9] and step 3.1 give ${FDR}_{θ} = \sum_{i \in I_{0} (θ)} q / m = (m_{0} (θ) / m) q \leq q$ , since $m_{0} (θ) \leq m$ . This is the FDR defined in [F1], not an FWER conclusion.

Remarks

No choice axiom is used: the family is finite, each leave-one-out index is fixed in the proof, and the product-law supplier is applied only to finite families.

Depends on

Used by

A two-test BH family distinguishes FDR from FWER Example

Dependency tree · two levels

35 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

Yoav Benjamini and Yosef Hochberg, Controlling the False Discovery Rate: A Practical and Powerful Approach to Multiple Testing, JRSS B 57(1) (1995), Theorem 1 and Appendix A (standard reference, not scraped)
Yoav Benjamini and Daniel Yekutieli, The Control of the False Discovery Rate in Multiple Testing under Dependency, The Annals of Statistics 29(4) (2001), §5, PDF pp. 16–17 (standard reference, not scraped)
STATS 200: Introduction to Statistical Inference, Lecture 11: Testing Multiple Hypotheses, Stanford University, PDF pp. 28–36 (standard reference, not scraped)