Pipeline-generated

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.

✓ 1 result · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 1 also cleared it.

BH independent FDR — Examples

1 · Prerequisites

2 · Summary

A two-hypothesis family with one exact-uniform true-null p-value and one false-null p-value fixed at zero attains the BH FDR bound while separating FDR from FWER. Under the global null, the two rates agree because the false discovery proportion is exactly the indicator of at least one rejection.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A two-test BH family distinguishes FDR from FWER

Example

Take two hypotheses and $q = 1 / 2$ . Under the specified law, $H_{1}$ is true with $P_{1} \sim Unif [0, 1]$ , while $H_{2}$ is false with $P_{2} = 0$ almost surely. The p-values are independent. The BH procedure has $FDR = 1 / 4$ and $FWER = 1 / 2$ , so its FDR bound is attained while FDR and FWER differ.

Facts & Assumptions

Given: $m = 2$ , $q = 1 / 2$ , $I_{0} = {1}$ , $P_{1} \sim Unif [0, 1]$ , and $P_{2} = 0$ almost surely under the fixed law.

[F1]

False discovery proportion, FDR, and FWER: if $V$ counts false rejections and $R$ counts all rejections, then $FDP = V / (R \lor 1)$ , $FDR = E [FDP]$ , and $FWER = P (V \geq 1)$ .

[F2]

Benjamini–Hochberg step-up procedure: BH rejects ranks through the largest $k$ with $p_{(k)} \leq k q / m$ .

[F3]

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

[F4]

Valid p-values: a p-value statistic takes values in $[0, 1]$ and is valid under a null law when $P (p \leq u) \leq u$ for every $u \in [0, 1]$ .

[F5]

Benjamini–Hochberg FDR under independence: under mutual independence and exactly uniform true-null p-values, BH has FDR $(m_{0} / m) q$ .

[A1]

In this example, $P_{2}$ is a constant random element and hence is independent of $P_{1}$ ; $P_{1}$ is exactly uniform and therefore valid under $H_{1}$ .

[A2]

For the global-null comparison in step 3.1, all hypotheses in the finite family are true, so $I_{0} = [m]$ .

Verification

1.1givenA1F2F3F4algebra

For Borel sets $A, B$ , $P (P_{1} \in A, P_{2} \in B) = P (P_{1} \in A) 1 {0 \in B} = P (P_{1} \in A) P (P_{2} \in B)$ , so [F3] confirms independence; also $P (P_{1} \leq u) = u$ for $u \in [0, 1]$ , so [F4] confirms true-null validity. The ordered values are $0, P_{1}$ : the first BH threshold is $q / 2 = 1 / 4$ and always passes, while the second is $q = 1 / 2$ and passes exactly when $P_{1} \leq 1 / 2$ . Thus both hypotheses are rejected when $P_{1} \leq 1 / 2$ , and only the false null $H_{2}$ is rejected otherwise.

2.1givenA1F1F5step 1.1algebra

If $P_{1} \leq 1 / 2$ , then $V = 1$ , $R = 2$ , and FDP $= 1 / 2$ ; if $P_{1} > 1 / 2$ , then $V = 0$ , $R = 1$ , and FDP $= 0$ . Since $P (P_{1} \leq 1 / 2) = 1 / 2$ , [F1] gives $FDR = 1 / 4$ and $FWER = 1 / 2$ . Here $(m_{0} / m) q = (1 / 2) (1 / 2) = 1 / 4$ , which attains the guarantee [F5].

3.1A2F1algebra∎

Under [A2], $V = R$ pointwise; when $R > 0$ , both $V / (R \lor 1)$ and $1 {V \geq 1}$ equal $1$ , and when $R = 0$ both equal $0$ . Thus the FDP is $1 {V \geq 1}$ pointwise, and evaluating its simple-function integral gives $E [1 {V \geq 1}] = 1 \cdot P (V \geq 1) + 0 \cdot P ((V \geq 1)^{c}) = P (V \geq 1)$ . By [F1], this gives $FDR = FWER$ under the global null.