Benjamini–Hochberg procedure

DefinitionBenjamini–Hochberg step-up index#✓fully proved

The Benjamini–Hochberg step-up index: the largest k ∈ {0, …, m} such that at least k p-values are at most q k / m (k = 0 always qualifies).

noncomputable def bhIndex (q : ℝ) (p : Fin m → ℝ) : ℕ :=
  ((Finset.range (m + 1)).filter fun k : ℕ => k ≤ numBelow p (q * (k : ℝ) / m)).max'
    ⟨0, by simp⟩

Uses 1 · Used by 6

Statement usesNumber of p-values below a threshold

Used byBenjamini–Hochberg index is at most the number of hypotheses · Benjamini–Hochberg index satisfies the step-up condition · Benjamini–Hochberg rejection set · Number of Benjamini–Hochberg rejections · Benjamini–Hochberg FDR control · Maximality of the Benjamini–Hochberg index

DefinitionBenjamini–Hochberg rejection set#✓fully proved

The hypotheses rejected by the Benjamini–Hochberg procedure at level q: those whose p-value is at most q * bhIndex q p / m.

noncomputable def bhRejections (q : ℝ) (p : Fin m → ℝ) : Finset (Fin m) :=
  Finset.univ.filter fun i => p i ≤ q * bhIndex q p / m

Uses 1 · Used by 2

Statement usesBenjamini–Hochberg step-up index

Used byNumber of Benjamini–Hochberg rejections · Benjamini–Hochberg FDR control

TheoremBenjamini–Hochberg index is at most the number of hypotheses#✓fully proved

The BH step-up index is at most m.

theorem bhIndex_le (q : ℝ) (p : Fin m → ℝ) : bhIndex q p ≤ m

Uses 2 · Used by 1

Statement usesBenjamini–Hochberg step-up index

Proof usesNumber of p-values below a threshold

Used byBenjamini–Hochberg FDR control

TheoremBenjamini–Hochberg index satisfies the step-up condition#✓fully proved

At the BH step-up index k, at least k p-values are at most q k / m.

theorem bhIndex_le_numBelow (q : ℝ) (p : Fin m → ℝ) :
    bhIndex q p ≤ numBelow p (q * bhIndex q p / m)

Uses 2 · Used by 2

Statement usesBenjamini–Hochberg step-up index · Number of p-values below a threshold

Used byNumber of Benjamini–Hochberg rejections · Benjamini–Hochberg FDR control

TheoremMaximality of the Benjamini–Hochberg index#✓fully proved

The BH step-up index is the largest k ≤ m with at least k p-values at most q k / m.

theorem le_bhIndex {q : ℝ} {p : Fin m → ℝ} {k : ℕ} (hk : k ≤ m)
    (h : k ≤ numBelow p (q * k / m)) : k ≤ bhIndex q p

Uses 2 · Used by 2

Statement usesBenjamini–Hochberg step-up index · Number of p-values below a threshold

Used byNumber of Benjamini–Hochberg rejections · Benjamini–Hochberg FDR control

TheoremNumber of Benjamini–Hochberg rejections#✓fully proved

The BH procedure at level q ≥ 0 rejects exactly bhIndex q p hypotheses.

theorem card_bhRejections {q : ℝ} (hq : 0 ≤ q) (p : Fin m → ℝ) :
    (bhRejections q p).card = bhIndex q p

Uses 7 · Used by 1

Statement usesBenjamini–Hochberg step-up index · Benjamini–Hochberg rejection set

Proof usesBenjamini–Hochberg index satisfies the step-up condition · Maximality of the Benjamini–Hochberg index · Number of p-values below a threshold · Number of p-values below a threshold is at most the total · Number of p-values below a threshold is monotone

Used byBenjamini–Hochberg FDR control

TheoremBenjamini–Hochberg FDR control#✓fully proved

If the p-values are independent and every true-null p-value is uniformly distributed on [0, 1], the BH procedure at level q ∈ [0, 1] has false discovery rate at most q |H0| / m. Nothing is assumed about the false-null p-values beyond measurability and independence. (For m = 0 both sides are 0.)

theorem integral_falseDiscoveryProportion_bhRejections_le {Ω : Type*}
    [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (p : Fin m → Ω → ℝ)
    (hp : ∀ i, Measurable (p i)) (hindep : iIndepFun p μ) (H0 : Finset (Fin m))
    (hnull : ∀ i ∈ H0, HasLaw (p i) (volume.restrict (Set.Icc (0 : ℝ) 1)) μ)
    (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q ≤ 1) :
    ∫ ω, falseDiscoveryProportion H0 (bhRejections q fun i => p i ω) ∂μ ≤ q * H0.card / m

Sources

• Benjamini & Hochberg (1995), Theorem 1.

Uses 10

Statement usesBenjamini–Hochberg rejection set · False discovery proportion

Proof usesValid p-value · Benjamini–Hochberg step-up index · Benjamini–Hochberg index is at most the number of hypotheses · Benjamini–Hochberg index satisfies the step-up condition · Number of Benjamini–Hochberg rejections · Uniform p-values are valid · Maximality of the Benjamini–Hochberg index · Number of p-values below a threshold

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.