Valid p-values and false discovery proportion

DefinitionValid p-value#✓fully proved

A real random variable X is a valid (super-uniform) p-value under μ if μ {X ≤ t} ≤ t for every level t ∈ [0, 1]. Uniform p-values are the equality case.

def IsValidPValue (μ : Measure Ω) (X : Ω → ℝ) : Prop :=
  ∀ t ∈ Set.Icc (0 : ℝ) 1, μ {ω | X ω ≤ t} ≤ ENNReal.ofReal t

Used by 10

Used byBenjamini–Hochberg FDR control · The Bonferroni procedure controls the FWER · Bonferroni inequality · Union bound for valid p-values · Level of the Bonferroni local test · Holm's procedure controls the FWER · Validity of Monte Carlo permutation p-values · Validity of permutation p-values · Conservative bias of Storey's null proportion estimator · Uniform p-values are valid

TheoremUniform p-values are valid#✓fully proved

A p-value distributed uniformly on [0, 1] is valid.

theorem isValidPValue_of_hasLaw_uniform {μ : Measure Ω} {X : Ω → ℝ}
    (hX : HasLaw X (volume.restrict (Set.Icc (0 : ℝ) 1)) μ) : IsValidPValue μ X

Uses 1 · Used by 1

Statement usesValid p-value

Used byBenjamini–Hochberg FDR control

DefinitionNumber of p-values below a threshold#✓fully proved

The number of p-values that are at most t.

noncomputable def numBelow (p : Fin m → ℝ) (t : ℝ) : ℕ :=
  (Finset.univ.filter fun i => p i ≤ t).card

Used by 15

Used byBenjamini–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 · Benjamini–Hochberg FDR control · Maximality of the Benjamini–Hochberg index · Holm's procedure is a closed test · Number of hypotheses rejected by Holm's procedure · Holm rejection bound for a set of hypotheses · Holm's step-down count · Holm's step-down count is at most the number of tests · Holm's count is the largest index where every step succeeds · Every step up to Holm's count succeeds · Number of p-values below a threshold is at most the total · Number of p-values below a threshold is monotone

TheoremNumber of p-values below a threshold is at most the total#✓fully proved

At most m p-values lie below any threshold.

theorem numBelow_le (p : Fin m → ℝ) (t : ℝ) : numBelow p t ≤ m

Uses 1 · Used by 1

Statement usesNumber of p-values below a threshold

Used byNumber of Benjamini–Hochberg rejections

TheoremNumber of p-values below a threshold is monotone#✓fully proved

numBelow p is monotone in the threshold.

theorem numBelow_mono (p : Fin m → ℝ) {s t : ℝ} (hst : s ≤ t) : numBelow p s ≤ numBelow p t

Uses 1 · Used by 2

Statement usesNumber of p-values below a threshold

Used byNumber of Benjamini–Hochberg rejections · Number of hypotheses rejected by Holm's procedure

DefinitionFalse discovery proportion#✓fully proved

The false discovery proportion of a rejection set R when H0 is the set of true nulls: |R ∩ H0| / max |R| 1 (zero when nothing is rejected).

noncomputable def falseDiscoveryProportion (H0 R : Finset (Fin m)) : ℝ :=
  ((R ∩ H0).card : ℝ) / max (R.card : ℝ) 1

Used by 5

Used byBenjamini–Hochberg FDR control · Storey's positive false discovery rate · Storey's theorem: pFDR is a posterior null probability · False discovery proportion is at most one · False discovery proportion is nonnegative

TheoremFalse discovery proportion is nonnegative#✓fully proved

The false discovery proportion is nonnegative.

theorem falseDiscoveryProportion_nonneg (H0 R : Finset (Fin m)) :
    0 ≤ falseDiscoveryProportion H0 R

Uses 1

Statement usesFalse discovery proportion

TheoremFalse discovery proportion is at most one#✓fully proved

The false discovery proportion is at most one.

theorem falseDiscoveryProportion_le_one (H0 R : Finset (Fin m)) :
    falseDiscoveryProportion H0 R ≤ 1

Uses 1

Statement usesFalse discovery proportion

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.