Saturation power for cancer gene discovery

DefinitionSaturation power of the binomial gene discovery test#✓fully proved

Power of the one-sided binomial test of Lawrence et al. (2014): the probability, when each of N patients is mutated with probability p₁, of observing a count x whose background p-value ℙ_{p₀}(X ≥ x) is at most γ.

noncomputable def saturationPower (N : ℕ) (p₀ p₁ γ : ℝ) : ℝ :=
  ∑ x ∈ range (N + 1) with upperTail N p₀ x ≤ γ, binomPmf N p₁ x

Uses 2 · Used by 2

Statement usesBinomial probability mass function · Binomial upper tail probability

Used byN_β exists · Power tends to one

DefinitionBackground mutation probability per patient#✓fully proved

Background probability p₀ = 1 - (1 - μ f_g)^(3L/4) that a patient carries at least one non-silent background mutation in a gene of L coding bases (Lawrence et al. 2014).

noncomputable def lawrenceP0 (μ fg L : ℝ) : ℝ := 1 - (1 - μ * fg) ^ (3 * L / 4)

Used by 1

Used byBackground mutation probability lies in (0, 1)

DefinitionSignal mutation probability per patient#✓fully proved

Signal probability p₁ = p₀ + r (1 - m) for a gene mutated in a fraction r of patients above background, with miss rate m (Lawrence et al. 2014).

def lawrenceP1 (p₀ r m : ℝ) : ℝ := p₀ + r * (1 - m)

Used by 1

Used byDriver genes raise the per-patient mutation probability

TheoremPower tends to one#✓fully proved

For 0 ≤ p₀ < p₁ ≤ 1 and any level γ > 0, the power of the binomial test tends to 1 as the number of patients grows.

theorem tendsto_saturationPower {p₀ p₁ γ : ℝ} (hp₀ : 0 ≤ p₀) (hp₀₁ : p₀ < p₁) (hp₁ : p₁ ≤ 1)
    (hγ : 0 < γ) : Tendsto (fun N => saturationPower N p₀ p₁ γ) atTop (𝓝 1)

Uses 5 · Used by 1

Statement usesSaturation power of the binomial gene discovery test

Proof usesBinomial probability mass function · Nonnegativity of binomial probabilities · Binomial probabilities sum to one · Binomial upper tail probability

Used byN_β exists

TheoremN_β exists#✓fully proved

For every target power β < 1 there is a cohort size beyond which the power is at least β (Lawrence et al. 2014 take β = 0.9).

theorem eventually_le_saturationPower {p₀ p₁ γ β : ℝ} (hp₀ : 0 ≤ p₀) (hp₀₁ : p₀ < p₁)
    (hp₁ : p₁ ≤ 1) (hγ : 0 < γ) (hβ : β < 1) :
    ∃ N₀, ∀ N ≥ N₀, β ≤ saturationPower N p₀ p₁ γ

Uses 2

Statement usesSaturation power of the binomial gene discovery test

Proof usesPower tends to one

TheoremBackground mutation probability lies in (0, 1)#✓fully proved

The background probability is a probability below one: 0 ≤ p₀ < 1 for 0 ≤ μ f_g < 1 and L ≥ 0.

theorem lawrenceP0_mem {μ fg L : ℝ} (h0 : 0 ≤ μ * fg) (h1 : μ * fg < 1) (hL : 0 ≤ L) :
    0 ≤ lawrenceP0 μ fg L ∧ lawrenceP0 μ fg L < 1

Uses 1

Statement usesBackground mutation probability per patient

TheoremDriver genes raise the per-patient mutation probability#✓fully proved

A driver mutated above background raises the per-patient probability: p₀ < p₀ + r (1 - m) for r > 0 and m < 1.

theorem lawrenceP0_lt_lawrenceP1 {p₀ r m : ℝ} (hr : 0 < r) (hm : m < 1) :
    p₀ < lawrenceP1 p₀ r m

Uses 1

Statement usesSignal mutation probability per patient

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.