Closed testing principle

DefinitionClosed testing procedure#✓fully proved

The closed testing procedure: given the decisions φ J of local tests of the intersection hypotheses H_J, reject Hᵢ exactly when φ J holds for every J containing i.

noncomputable def closedRejections (φ : Finset (Fin m) → Prop) : Finset (Fin m) := by
  classical
  exact Finset.univ.filter fun i => ∀ J : Finset (Fin m), i ∈ J → φ J

Used by 4

Used byHolm's procedure is a closed test · Closed testing rejection implies the intersection test rejects · The closed testing principle · Membership in the closed rejection set

TheoremMembership in the closed rejection set#✓fully proved

Membership in the closed rejection set.

theorem mem_closedRejections {φ : Finset (Fin m) → Prop} {i : Fin m} :
    i ∈ closedRejections φ ↔ ∀ J : Finset (Fin m), i ∈ J → φ J

Uses 1 · Used by 2

Statement usesClosed testing procedure

Used byHolm's procedure is a closed test · Closed testing rejection implies the intersection test rejects

TheoremClosed testing rejection implies the intersection test rejects#✓fully proved

If the closed procedure rejects a hypothesis in H0, then the local test of the intersection hypothesis H_{H0} rejects.

theorem inter_nonempty_closedRejections {φ : Finset (Fin m) → Prop} {H0 : Finset (Fin m)}
    (h : (closedRejections φ ∩ H0).Nonempty) : φ H0

Uses 2 · Used by 1

Statement usesClosed testing procedure

Proof usesMembership in the closed rejection set

Used byThe closed testing principle

TheoremThe closed testing principle#✓fully proved

If H0 is the set of true nulls and the local test of H_{H0} rejects with probability at most α, then the closed procedure rejects some true null with probability at most α. Applied to every possible H0, local level-α tests give strong control of the family-wise error rate. No assumption on the dependence between local tests is made.

theorem measure_closed_familywiseError_le (μ : Measure Ω) (φ : Finset (Fin m) → Ω → Prop)
    (H0 : Finset (Fin m)) {α : ENNReal} (hlocal : μ {ω | φ H0 ω} ≤ α) :
    μ {ω | (closedRejections (fun J => φ J ω) ∩ H0).Nonempty} ≤ α

Sources

• Marcus, Peritz and Gabriel (1976).

Uses 2

Statement usesClosed testing procedure

Proof usesClosed testing rejection implies the intersection test rejects

DefinitionBonferroni local test of an intersection hypothesis#✓fully proved

The Bonferroni local test of the intersection hypothesis H_J at level α: reject when some j ∈ J has p j ≤ α / |J|. (It never rejects H_∅.)

def bonferroniLocalTest (α : ℝ) (p : Fin m → ℝ) (J : Finset (Fin m)) : Prop :=
  ∃ j ∈ J, p j ≤ α / J.card

Used by 2

Used byHolm's procedure is a closed test · Level of the Bonferroni local test

TheoremLevel of the Bonferroni local test#✓fully proved

The Bonferroni local test of H_{H0} has level α ∈ [0, 1] when the p-values in H0 are valid.

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

Uses 3

Statement usesValid p-value · Bonferroni local test of an intersection hypothesis

Proof usesUnion bound for valid p-values

TheoremHolm's procedure is a closed test#✓fully proved

For α ≥ 0, the hypotheses rejected by Holm's step-down procedure are exactly those rejected by the closed testing procedure built on the Bonferroni local tests.

theorem holmRejections_eq_closedRejections {α : ℝ} (hα : 0 ≤ α) (p : Fin m → ℝ) :
    holmRejections α p = closedRejections (bonferroniLocalTest α p)

Sources

• Holm (1979) introduces the procedure; the closure is that of Marcus, Peritz and Gabriel (1976).

Uses 10

Statement usesBonferroni local test of an intersection hypothesis · Closed testing procedure · Hypotheses rejected by Holm's step-down procedure

Proof usesNumber of hypotheses rejected by Holm's procedure · Holm rejection bound for a set of hypotheses · Holm's step-down count · Holm's count is the largest index where every step succeeds · Every step up to Holm's count succeeds · Membership in the closed rejection set · Number of p-values below a threshold

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.