Skip to content

Two-groups model and local false discovery rates

38 fully proved

The two-groups model

StructureTwo-groups model#✓fully proved

The two-groups model of Efron et al. (2001): prior null probability π₀ ∈ [0, 1], null density f₀ and non-null density f₁ of the z-value (probability densities on ℝ).

MathlibExt.Probability.Statistics.TwoGroupsTesting.TwoGroupsModel · 27 lines 
structure TwoGroupsModel where
  /-- Prior probability that a case is null. -/
  π₀ : ℝ
  /-- Density of the z-value of a null case. -/
  f₀ : ℝ → ℝ
  /-- Density of the z-value of a non-null case. -/
  f₁ : ℝ → ℝ
  /-- The prior null probability is nonnegative. -/
  π₀_nonneg : 0 ≤ π₀
  /-- The prior null probability is at most one. -/
  π₀_le_one : π₀ ≤ 1
  /-- The null density is nonnegative. -/
  f₀_nonneg : ∀ z, 0 ≤ f₀ z
  /-- The non-null density is nonnegative. -/
  f₁_nonneg : ∀ z, 0 ≤ f₁ z
  /-- The null density is measurable. -/
  measurable_f₀ : Measurable f₀
  /-- The non-null density is measurable. -/
  measurable_f₁ : Measurable f₁
  /-- The null density is integrable. -/
  integrable_f₀ : Integrable f₀
  /-- The non-null density is integrable. -/
  integrable_f₁ : Integrable f₁
  /-- The null density integrates to one. -/
  integral_f₀ : ∫ z, f₀ z = 1
  /-- The non-null density integrates to one. -/
  integral_f₁ : ∫ z, f₁ z = 1
Used by 26
Used byLaw of a non-null z-value · Non-null law as the integral of the non-null density · Local fdr is the posterior null probability · Tail-area fdr is the posterior null probability given a region · Mixture density is integrable · Joint law of null indicator and z-value · Joint probability of a non-null case in a set · Joint probability of a null case in a set · Null probability as an integral of the local fdr · z-value has the mixture law · Local false discovery rate · Local false discovery rate is at most one · Local fdr times mixture density equals the null part · Local false discovery rate is nonnegative · Marginal z-value law of the joint law is the mixture · Local false discovery rate is measurable · Mixture density is measurable · Mixture density of the two-groups model · Mixture density is nonnegative · Null part of the mixture is dominated by the mixture · Law of a null z-value · Null law as the integral of the null density · Law of a test's null and rejection pair · Storey's theorem in the two-groups model · Tail-area false discovery rate · Tail-area fdr is the average local fdr over the region

DefinitionMixture density of the two-groups model#✓fully proved

The mixture density f = π₀ f₀ + (1 - π₀) f₁ of the z-values.

noncomputable def mixtureDensity (z : ℝ) : ℝ := M.π₀ * M.f₀ z + (1 - M.π₀) * M.f₁ z
Uses 1 · Used by 17
Statement usesTwo-groups model
Used byLocal fdr is the posterior null probability · Tail-area fdr is the posterior null probability given a region · Mixture density is integrable · Null probability as an integral of the local fdr · z-value has the mixture law · Local false discovery rate · Local false discovery rate is at most one · Local fdr times mixture density equals the null part · Local false discovery rate is nonnegative · Marginal z-value law of the joint law is the mixture · Local false discovery rate is measurable · Mixture density is measurable · Mixture density is nonnegative · Null part of the mixture is dominated by the mixture · Storey's theorem in the two-groups model · Tail-area false discovery rate · Tail-area fdr is the average local fdr over the region

DefinitionLaw of a null z-value#✓fully proved

The law P₀ of a null z-value.

noncomputable def nullLaw : Measure ℝ := volume.withDensity fun z => ENNReal.ofReal (M.f₀ z)
Uses 1 · Used by 4
Statement usesTwo-groups model
Used byJoint law of null indicator and z-value · Joint probability of a non-null case in a set · Joint probability of a null case in a set · Null law as the integral of the null density

DefinitionLaw of a non-null z-value#✓fully proved

The law P₁ of a non-null z-value.

noncomputable def altLaw : Measure ℝ := volume.withDensity fun z => ENNReal.ofReal (M.f₁ z)
Uses 1 · Used by 4
Statement usesTwo-groups model
Used byNon-null law as the integral of the non-null density · Joint law of null indicator and z-value · Joint probability of a non-null case in a set · Joint probability of a null case in a set

DefinitionJoint law of null indicator and z-value#✓fully proved

Joint law of (null indicator, z-value) on Bool × ℝ; true means the case is null.

noncomputable def jointLaw : Measure (Bool × ℝ) :=
  ENNReal.ofReal M.π₀ • (Measure.dirac true).prod M.nullLaw +
    ENNReal.ofReal (1 - M.π₀) • (Measure.dirac false).prod M.altLaw
Uses 3 · Used by 9
Statement usesTwo-groups model · Law of a non-null z-value · Law of a null z-value
Used byLocal fdr is the posterior null probability · Tail-area fdr is the posterior null probability given a region · Joint probability of a non-null case in a set · Joint probability of a null case in a set · Null probability as an integral of the local fdr · z-value has the mixture law · Marginal z-value law of the joint law is the mixture · Law of a test's null and rejection pair · Storey's theorem in the two-groups model

DefinitionLocal false discovery rate#✓fully proved

Efron's local false discovery rate fdr(z) = π₀ f₀(z) / f(z) (zero where f(z) = 0).

noncomputable def localFdr (z : ℝ) : ℝ := M.π₀ * M.f₀ z / M.mixtureDensity z
Uses 2 · Used by 7
Statement usesTwo-groups model · Mixture density of the two-groups model
Used byLocal fdr is the posterior null probability · Null probability as an integral of the local fdr · Local false discovery rate is at most one · Local fdr times mixture density equals the null part · Local false discovery rate is nonnegative · Local false discovery rate is measurable · Tail-area fdr is the average local fdr over the region

DefinitionTail-area false discovery rate#✓fully proved

The tail-area false discovery rate of a region Γ: Fdr(Γ) = π₀ P₀(Γ) / P(Γ), written with the densities. Efron's Fdr(z) is tailFdr (Set.Iic z). It is 0 when P(Γ) = 0.

noncomputable def tailFdr (Γ : Set ℝ) : ℝ :=
  M.π₀ * (∫ z in Γ, M.f₀ z) / ∫ z in Γ, M.mixtureDensity z
Uses 2 · Used by 3
Statement usesTwo-groups model · Mixture density of the two-groups model
Used byTail-area fdr is the posterior null probability given a region · Storey's theorem in the two-groups model · Tail-area fdr is the average local fdr over the region

TheoremMixture density is nonnegative#✓fully proved

The mixture density is nonnegative.

theorem mixtureDensity_nonneg (z : ℝ) : 0 ≤ M.mixtureDensity z
Uses 2 · Used by 5
Statement usesTwo-groups model · Mixture density of the two-groups model
Used byTail-area fdr is the posterior null probability given a region · Null probability as an integral of the local fdr · Local false discovery rate is at most one · Local false discovery rate is nonnegative · Marginal z-value law of the joint law is the mixture

TheoremNull part of the mixture is dominated by the mixture#✓fully proved

The null part of the mixture is dominated by the mixture: π₀ f₀ ≤ f.

theorem mul_f₀_le_mixtureDensity (z : ℝ) : M.π₀ * M.f₀ z ≤ M.mixtureDensity z
Uses 2 · Used by 2
Statement usesTwo-groups model · Mixture density of the two-groups model
Used byLocal false discovery rate is at most one · Local fdr times mixture density equals the null part

TheoremMixture density is measurable#✓fully proved

The mixture density is measurable.

theorem measurable_mixtureDensity : Measurable M.mixtureDensity
Uses 2 · Used by 2
Statement usesTwo-groups model · Mixture density of the two-groups model
Used byNull probability as an integral of the local fdr · Local false discovery rate is measurable

TheoremMixture density is integrable#✓fully proved

The mixture density is integrable.

theorem integrable_mixtureDensity : Integrable M.mixtureDensity
Uses 2 · Used by 1
Statement usesTwo-groups model · Mixture density of the two-groups model
Used byMarginal z-value law of the joint law is the mixture

TheoremLocal false discovery rate is measurable#✓fully proved

The local false discovery rate is measurable.

theorem measurable_localFdr : Measurable M.localFdr
Uses 4 · Used by 2
Statement usesTwo-groups model · Local false discovery rate
Proof usesMixture density is measurable · Mixture density of the two-groups model
Used byLocal fdr is the posterior null probability · Null probability as an integral of the local fdr

TheoremLocal fdr times mixture density equals the null part#✓fully proved

The basic identity fdr(z) f(z) = π₀ f₀(z), for every z (where f(z) = 0 both sides vanish because π₀ f₀ ≤ f).

theorem localFdr_mul_mixtureDensity (z : ℝ) :
    M.localFdr z * M.mixtureDensity z = M.π₀ * M.f₀ z
Uses 4 · Used by 2
Statement usesTwo-groups model · Local false discovery rate · Mixture density of the two-groups model
Proof usesNull part of the mixture is dominated by the mixture
Used byNull probability as an integral of the local fdr · Tail-area fdr is the average local fdr over the region

TheoremLocal false discovery rate is nonnegative#✓fully proved

The local false discovery rate is nonnegative.

theorem localFdr_nonneg (z : ℝ) : 0 ≤ M.localFdr z
Uses 4 · Used by 1
Statement usesTwo-groups model · Local false discovery rate
Proof usesMixture density of the two-groups model · Mixture density is nonnegative
Used byLocal fdr is the posterior null probability

TheoremLocal false discovery rate is at most one#✓fully proved

The local false discovery rate is at most one.

theorem localFdr_le_one (z : ℝ) : M.localFdr z ≤ 1
Uses 5 · Used by 1
Statement usesTwo-groups model · Local false discovery rate
Proof usesMixture density of the two-groups model · Mixture density is nonnegative · Null part of the mixture is dominated by the mixture
Used byLocal fdr is the posterior null probability

TheoremNull law as the integral of the null density#✓fully proved

P₀(A) = ∫_A f₀.

theorem nullLaw_apply {A : Set ℝ} (hA : MeasurableSet A) :
    M.nullLaw A = ENNReal.ofReal (∫ z in A, M.f₀ z)
Uses 2 · Used by 2
Statement usesTwo-groups model · Law of a null z-value
Used byJoint probability of a non-null case in a set · Joint probability of a null case in a set

TheoremNon-null law as the integral of the non-null density#✓fully proved

P₁(A) = ∫_A f₁.

theorem altLaw_apply {A : Set ℝ} (hA : MeasurableSet A) :
    M.altLaw A = ENNReal.ofReal (∫ z in A, M.f₁ z)
Uses 2 · Used by 2
Statement usesTwo-groups model · Law of a non-null z-value
Used byJoint probability of a non-null case in a set · Joint probability of a null case in a set

TheoremJoint probability of a null case in a set#✓fully proved

P(H = 0, Z ∈ A) = π₀ P₀(A).

theorem jointLaw_null_prod {A : Set ℝ} (hA : MeasurableSet A) :
    M.jointLaw ({true} ×ˢ A) = ENNReal.ofReal (M.π₀ * ∫ z in A, M.f₀ z)
Uses 6 · Used by 4
Statement usesTwo-groups model · Joint law of null indicator and z-value
Proof usesLaw of a non-null z-value · Non-null law as the integral of the non-null density · Law of a null z-value · Null law as the integral of the null density
Used byTail-area fdr is the posterior null probability given a region · Null probability as an integral of the local fdr · z-value has the mixture law · Storey's theorem in the two-groups model

TheoremJoint probability of a non-null case in a set#✓fully proved

P(H = 1, Z ∈ A) = (1 - π₀) P₁(A).

theorem jointLaw_alt_prod {A : Set ℝ} (hA : MeasurableSet A) :
    M.jointLaw ({false} ×ˢ A) = ENNReal.ofReal ((1 - M.π₀) * ∫ z in A, M.f₁ z)
Uses 6 · Used by 2
Statement usesTwo-groups model · Joint law of null indicator and z-value
Proof usesLaw of a non-null z-value · Non-null law as the integral of the non-null density · Law of a null z-value · Null law as the integral of the null density
Used byz-value has the mixture law · Storey's theorem in the two-groups model

Theoremz-value has the mixture law#✓fully proved

The z-value has the mixture law: P(Z ∈ A) = ∫_A f.

theorem jointLaw_univ_prod {A : Set ℝ} (hA : MeasurableSet A) :
    M.jointLaw (Set.univ ×ˢ A) = ENNReal.ofReal (∫ z in A, M.mixtureDensity z)
Uses 5 · Used by 3
Statement usesTwo-groups model · Joint law of null indicator and z-value · Mixture density of the two-groups model
Proof usesJoint probability of a non-null case in a set · Joint probability of a null case in a set
Used byLocal fdr is the posterior null probability · Tail-area fdr is the posterior null probability given a region · Marginal z-value law of the joint law is the mixture

TheoremMarginal z-value law of the joint law is the mixture#✓fully proved

The law of the z-value under the joint law is the mixture f · Lebesgue.

theorem map_snd_jointLaw :
    M.jointLaw.map Prod.snd =
      volume.withDensity fun z => ENNReal.ofReal (M.mixtureDensity z)
Uses 6 · Used by 1
Statement usesTwo-groups model · Joint law of null indicator and z-value · Mixture density of the two-groups model
Proof usesMixture density is integrable · z-value has the mixture law · Mixture density is nonnegative
Used byNull probability as an integral of the local fdr

TheoremNull probability as an integral of the local fdr#✓fully proved

Efron et al. (2001): P(H = 0, Z ∈ A) = ∫_A fdr(z) dP_Z(z) for every measurable A, so fdr(Z) is a version of the posterior null probability P(H = 0 | Z).

theorem jointLaw_null_prod_eq_lintegral_localFdr {A : Set ℝ} (hA : MeasurableSet A) :
    M.jointLaw ({true} ×ˢ A) =
      ∫⁻ z in A, ENNReal.ofReal (M.localFdr z) ∂(M.jointLaw.map Prod.snd)
Uses 10 · Used by 1
Statement usesTwo-groups model · Joint law of null indicator and z-value · Local false discovery rate
Proof usesJoint probability of a null case in a set · Local fdr times mixture density equals the null part · Marginal z-value law of the joint law is the mixture · Local false discovery rate is measurable · Mixture density is measurable · Mixture density of the two-groups model · Mixture density is nonnegative
Used byLocal fdr is the posterior null probability

TheoremLocal fdr is the posterior null probability#✓fully proved

Efron et al. (2001): fdr(Z) = P(H = 0 | Z) almost surely, as a conditional expectation of the null indicator given the z-value.

theorem condExp_null_eq_localFdr :
    M.jointLaw[{p : Bool × ℝ | p.1 = true}.indicator 1 |
        MeasurableSpace.comap Prod.snd (inferInstance : MeasurableSpace ℝ)]
      =ᵐ[M.jointLaw] fun p => M.localFdr p.2
Uses 9
Statement usesTwo-groups model · Joint law of null indicator and z-value · Local false discovery rate
Proof usesNull probability as an integral of the local fdr · z-value has the mixture law · Local false discovery rate is at most one · Local false discovery rate is nonnegative · Local false discovery rate is measurable · Mixture density of the two-groups model

TheoremTail-area fdr is the posterior null probability given a region#✓fully proved

P(H = 0 | Z ∈ Γ) = Fdr(Γ): the tail-area false discovery rate is the posterior null probability given Z ∈ Γ (Storey 2002, Theorem 1; Efron 2010, ch. 2). Both sides are 0 when P(Z ∈ Γ) = 0.

theorem cond_null_eq_tailFdr {Γ : Set ℝ} (hΓ : MeasurableSet Γ) :
    (M.jointLaw[{p | p.1 = true} | Prod.snd ⁻¹' Γ]).toReal = M.tailFdr Γ
Uses 7
Statement usesTwo-groups model · Joint law of null indicator and z-value · Tail-area false discovery rate
Proof usesJoint probability of a null case in a set · z-value has the mixture law · Mixture density of the two-groups model · Mixture density is nonnegative

TheoremTail-area fdr is the average local fdr over the region#✓fully proved

E[fdr(Z) | Z ∈ Γ] = Fdr(Γ), written with densities: the tail-area false discovery rate is the f-weighted average of the local false discovery rate over Γ (Efron 2010, ch. 5).

theorem tailFdr_eq_setIntegral_localFdr (Γ : Set ℝ) :
    M.tailFdr Γ =
      (∫ z in Γ, M.localFdr z * M.mixtureDensity z) / ∫ z in Γ, M.mixtureDensity z
Uses 5
Statement usesTwo-groups model · Local false discovery rate · Mixture density of the two-groups model · Tail-area false discovery rate
Proof usesLocal fdr times mixture density equals the null part

Storey's positive false discovery rate for i.i.d. tests

DefinitionTrue-null set of a test outcome vector#✓fully proved

The true-null set of an outcome vector x : Fin m → Bool × Bool, where (x i).1 records that hypothesis i is null and (x i).2 that it is rejected.

def nullSet (x : Fin m → Bool × Bool) : Finset (Fin m) := univ.filter fun i => (x i).1 = true
Used by 2
Used byStorey's positive false discovery rate · Storey's theorem: pFDR is a posterior null probability

DefinitionRejection set of a test outcome vector#✓fully proved

The rejection set of an outcome vector.

def rejectedSet (x : Fin m → Bool × Bool) : Finset (Fin m) :=
  univ.filter fun i => (x i).2 = true
Used by 2
Used byStorey's positive false discovery rate · Storey's theorem: pFDR is a posterior null probability

DefinitionProbability of a test outcome vector#✓fully proved

The probability ∏ᵢ q(xᵢ) of an outcome vector when the m (null, rejected) pairs are i.i.d. with law q.

def outcomeWeight (q : Bool × Bool → ℝ) (x : Fin m → Bool × Bool) : ℝ := ∏ i, q (x i)
Used by 2
Used byStorey's positive false discovery rate · Storey's theorem: pFDR is a posterior null probability

DefinitionStorey's positive false discovery rate#✓fully proved

Storey's positive false discovery rate pFDR = E[V / R | R > 0] for m tests whose (null, rejected) indicator pairs are i.i.d. with law q: V / R is the false discovery proportion.

noncomputable def positiveFDR (q : Bool × Bool → ℝ) (m : ℕ) : ℝ :=
  (∑ x : Fin m → Bool × Bool, outcomeWeight q x *
      falseDiscoveryProportion (nullSet x) (rejectedSet x)) /
    ∑ x : Fin m → Bool × Bool, if (rejectedSet x).Nonempty then outcomeWeight q x else 0
Uses 4 · Used by 2
Statement usesFalse discovery proportion · True-null set of a test outcome vector · Probability of a test outcome vector · Rejection set of a test outcome vector
Used byStorey's theorem: pFDR is a posterior null probability · Storey's theorem in the two-groups model

TheoremStorey's theorem: pFDR is a posterior null probability#✓fully proved

Storey (2002), Theorem 1: for m ≥ 1 i.i.d. tests, pFDR = P(H = 0 | T ∈ Γ), where q (true, true) = P(H = 0, T ∈ Γ) and q (false, true) = P(H = 1, T ∈ Γ). The identity is homogeneous in q, so only q ≥ 0 is assumed; when P(T ∈ Γ) = 0 both sides are 0.

theorem positiveFDR_eq (q : Bool × Bool → ℝ) (hq : ∀ b, 0 ≤ q b) (hm : 0 < m) :
    positiveFDR q m = q (true, true) / (q (true, true) + q (false, true))
Uses 5 · Used by 1
Statement usesStorey's positive false discovery rate
Proof usesFalse discovery proportion · True-null set of a test outcome vector · Probability of a test outcome vector · Rejection set of a test outcome vector
Used byStorey's theorem in the two-groups model

DefinitionLaw of a test's null and rejection pair#✓fully proved

The law of one test's (null, rejected) pair in the two-groups model when the test rejects iff its z-value lies in Γ.

noncomputable def pairLaw (Γ : Set ℝ) (b : Bool × Bool) : ℝ :=
  (M.jointLaw ({b.1} ×ˢ if b.2 then Γ else Γᶜ)).toReal
Uses 2 · Used by 1
Statement usesTwo-groups model · Joint law of null indicator and z-value
Used byStorey's theorem in the two-groups model

TheoremStorey's theorem in the two-groups model#✓fully proved

Storey (2002), Theorem 1, in the two-groups model: for m ≥ 1 i.i.d. tests rejecting on Γ, pFDR(Γ) = π₀ P₀(Γ) / P(Γ) = Fdr(Γ).

theorem positiveFDR_pairLaw_eq_tailFdr {Γ : Set ℝ} (hΓ : MeasurableSet Γ) (hm : 0 < m) :
    positiveFDR (M.pairLaw Γ) m = M.tailFdr Γ
Uses 9
Statement usesTwo-groups model · Law of a test's null and rejection pair · Tail-area false discovery rate · Storey's positive false discovery rate
Proof usesJoint law of null indicator and z-value · Joint probability of a non-null case in a set · Joint probability of a null case in a set · Mixture density of the two-groups model · Storey's theorem: pFDR is a posterior null probability

Storey's estimator of the null proportion

DefinitionStorey's estimator of the null proportion#✓fully proved

Storey's estimator π̂₀(t) = #{i | pᵢ > t} / (m (1 - t)) of the proportion of true nulls, for a tuning parameter t ∈ [0, 1).

noncomputable def storeyPi0 (t : ℝ) (p : Fin m → ℝ) : ℝ :=
  ((univ.filter fun i => t < p i).card : ℝ) / (m * (1 - t))
Used by 1
Used byConservative bias of Storey's null proportion estimator

TheoremConservative bias of Storey's null proportion estimator#✓fully proved

Conservative bias of Storey's (2002) estimator for a fixed set H0 of true nulls: if their p-values are valid, then E[π̂₀(t)] ≥ m₀ / m for every t ∈ [0, 1). No independence is assumed; the non-null p-values are arbitrary measurable functions.

theorem le_integral_storeyPi0 {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
    [IsProbabilityMeasure μ] {p : Fin m → Ω → ℝ} (hp : ∀ i, Measurable (p i))
    {H0 : Finset (Fin m)} (hnull : ∀ i ∈ H0, IsValidPValue μ (p i)) {t : ℝ} (ht0 : 0 ≤ t)
    (ht1 : t < 1) :
    (H0.card : ℝ) / m ≤ ∫ ω, storeyPi0 t (fun i => p i ω) ∂μ
Uses 2
Statement usesValid p-value · Storey's estimator of the null proportion

Storey's q-value

DefinitionStorey's q-value#✓fully proved

Storey's (2003) q-value for a nested family of rejection regions Γ_s = {T ≤ s} with pFDR(Γ_s) = pfdr s: q(t) = inf_{s ≥ t} pfdr s, the smallest pFDR over the regions that contain the observed statistic t.

noncomputable def qValue (pfdr : ℝ → ℝ) (t : ℝ) : ℝ := ⨅ s : Set.Ici t, pfdr s
Used by 3
Used byq-value is monotone in the statistic · q-value equals the pFDR when the pFDR is monotone · q-value is at most the pFDR of the smallest region

Theoremq-value is at most the pFDR of the smallest region#✓fully proved

The q-value is at most the pFDR of the smallest region containing the statistic.

theorem qValue_le {pfdr : ℝ → ℝ} (h0 : ∀ s, 0 ≤ pfdr s) (t : ℝ) : qValue pfdr t ≤ pfdr t
Uses 1
Statement usesStorey's q-value

Theoremq-value is monotone in the statistic#✓fully proved

The q-value is monotone in the statistic.

theorem monotone_qValue {pfdr : ℝ → ℝ} (h0 : ∀ s, 0 ≤ pfdr s) : Monotone (qValue pfdr)
Uses 1
Statement usesStorey's q-value

Theoremq-value equals the pFDR when the pFDR is monotone#✓fully proved

When the pFDR is nondecreasing along the nested regions, the q-value is the pFDR.

theorem qValue_eq_of_monotone {pfdr : ℝ → ℝ} (h : Monotone pfdr) (t : ℝ) :
    qValue pfdr t = pfdr t
Uses 1
Statement usesStorey's q-value

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.