Detection power for somatic mutations

DefinitionBinomial probability mass function#✓fully proved

The binomial probability C(n, i) p^i (1 - p)^(n - i) of i successes in n trials, as a function of i : ℕ. It vanishes for i > n (the binomial coefficient is zero there, so the truncated subtraction n - i is harmless).

def binomPmf (n : ℕ) (p : ℝ) (i : ℕ) : ℝ := (n.choose i : ℝ) * p ^ i * (1 - p) ^ (n - i)

Used by 25

Used byThe binomial family is TP2 · The continuous CCF MLE · Positivity of the grid posterior normalizer · Posterior probability that the cancer cell fraction exceeds a threshold · The CCF posterior is stochastically increasing in the read count · Binomial probabilities vanish above n · The binomial likelihood is unimodal in p, decreasing part · The binomial likelihood is unimodal in p, increasing part · Nonnegativity of binomial probabilities · Positivity of binomial probabilities · Power of the randomized mutation detection test · Detection power as a mixture of tail probabilities · Exact size · Binomial probabilities sum to one · Binomial upper tail probability · Binomial upper tail is decreasing · Recursion for the binomial upper tail · Binomial upper tail as one minus a lower sum · Binomial upper tail beyond n is zero · Binomial tails increase with the success probability · Nonnegativity of binomial tail probabilities · Tail gap at the critical count · Binomial upper tail from zero is one · Saturation power of the binomial gene discovery test · Power tends to one

DefinitionBinomial upper tail probability#✓fully proved

The binomial upper tail ℙ_p(X ≥ m) = ∑_{m ≤ i ≤ n} C(n, i) p^i (1 - p)^(n - i), Carter's P(m) with p = ε / 3.

def upperTail (n : ℕ) (p : ℝ) (m : ℕ) : ℝ := ∑ i ∈ Ico m (n + 1), binomPmf n p i

Uses 1 · Used by 21

Statement usesBinomial probability mass function

Used byCritical count of the mutation detection test · Upper bound on the critical count · Positivity of the critical count · Minimality of the critical count · Power of the randomized mutation detection test · Detection power as a mixture of tail probabilities · Power increases with the allelic fraction · Exact size · Randomization probability of the detection test · The randomization is a probability · Binomial upper tail is decreasing · Critical count meets the false-positive bound · Recursion for the binomial upper tail · Binomial upper tail as one minus a lower sum · Binomial upper tail beyond n is zero · Binomial tails increase with the success probability · Nonnegativity of binomial tail probabilities · Tail gap at the critical count · Binomial upper tail from zero is one · Saturation power of the binomial gene discovery test · Power tends to one

TheoremNonnegativity of binomial probabilities#✓fully proved

Binomial probabilities are nonnegative for 0 ≤ p ≤ 1.

theorem binomPmf_nonneg {n : ℕ} {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (i : ℕ) :
    0 ≤ binomPmf n p i

Uses 1 · Used by 6

Statement usesBinomial probability mass function

Used byPositivity of the grid posterior normalizer · The binomial likelihood is unimodal in p, decreasing part · The binomial likelihood is unimodal in p, increasing part · Binomial upper tail is decreasing · Nonnegativity of binomial tail probabilities · Power tends to one

TheoremPositivity of binomial probabilities#✓fully proved

Binomial probabilities are positive on {0, …, n} for 0 < p < 1.

theorem binomPmf_pos {n i : ℕ} {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (hi : i ≤ n) :
    0 < binomPmf n p i

Uses 1 · Used by 1

Statement usesBinomial probability mass function

Used byPositivity of the grid posterior normalizer

TheoremBinomial probabilities vanish above n#✓fully proved

Binomial probabilities vanish above n.

theorem binomPmf_eq_zero {n i : ℕ} (p : ℝ) (hi : n < i) : binomPmf n p i = 0

Uses 1 · Used by 2

Statement usesBinomial probability mass function

Used byThe binomial family is TP2 · Binomial upper tail as one minus a lower sum

TheoremBinomial probabilities sum to one#✓fully proved

The binomial law sums to one (the binomial theorem), for every real p.

theorem sum_binomPmf (n : ℕ) (p : ℝ) : ∑ i ∈ range (n + 1), binomPmf n p i = 1

Uses 1 · Used by 3

Statement usesBinomial probability mass function

Used byBinomial upper tail as one minus a lower sum · Binomial upper tail from zero is one · Power tends to one

TheoremNonnegativity of binomial tail probabilities#✓fully proved

Tail probabilities are nonnegative for 0 ≤ p ≤ 1.

theorem upperTail_nonneg {n : ℕ} {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (m : ℕ) :
    0 ≤ upperTail n p m

Uses 3

Statement usesBinomial upper tail probability

Proof usesBinomial probability mass function · Nonnegativity of binomial probabilities

TheoremBinomial upper tail from zero is one#✓fully proved

P(0) = 1, for every real p.

theorem upperTail_zero (n : ℕ) (p : ℝ) : upperTail n p 0 = 1

Uses 3 · Used by 1

Statement usesBinomial upper tail probability

Proof usesBinomial probability mass function · Binomial probabilities sum to one

Used byPositivity of the critical count

TheoremBinomial upper tail beyond n is zero#✓fully proved

P(m) = 0 for m > n.

theorem upperTail_eq_zero {n m : ℕ} (p : ℝ) (hm : n < m) : upperTail n p m = 0

Uses 2 · Used by 3

Statement usesBinomial upper tail probability

Proof usesBinomial probability mass function

Used byUpper bound on the critical count · Critical count meets the false-positive bound · Binomial upper tail as one minus a lower sum

TheoremBinomial upper tail as one minus a lower sum#✓fully proved

Carter's form of the tail: P(m) = 1 - ∑_{i < m} Binom(i | n, p), for every m.

theorem upperTail_eq_one_sub_sum (n : ℕ) (p : ℝ) (m : ℕ) :
    upperTail n p m = 1 - ∑ i ∈ range m, binomPmf n p i

Uses 5 · Used by 1

Statement usesBinomial probability mass function · Binomial upper tail probability

Proof usesBinomial probabilities vanish above n · Binomial probabilities sum to one · Binomial upper tail beyond n is zero

Used byRecursion for the binomial upper tail

TheoremRecursion for the binomial upper tail#✓fully proved

One step of the tail recursion: P(m) = Binom(m | n, p) + P(m + 1).

theorem upperTail_eq_add (n : ℕ) (p : ℝ) (m : ℕ) :
    upperTail n p m = binomPmf n p m + upperTail n p (m + 1)

Uses 3 · Used by 3

Statement usesBinomial probability mass function · Binomial upper tail probability

Proof usesBinomial upper tail as one minus a lower sum

Used byDetection power as a mixture of tail probabilities · Binomial upper tail is decreasing · Tail gap at the critical count

TheoremBinomial upper tail is decreasing#✓fully proved

m ↦ P(m) is antitone for 0 ≤ p ≤ 1.

theorem upperTail_antitone {n : ℕ} {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) :
    Antitone (upperTail n p)

Uses 4

Statement usesBinomial upper tail probability

Proof usesBinomial probability mass function · Nonnegativity of binomial probabilities · Recursion for the binomial upper tail

TheoremBinomial tails increase with the success probability#✓fully proved

For 0 ≤ p ≤ p' ≤ 1, ℙ_p(X ≥ m) ≤ ℙ_{p'}(X ≥ m).

theorem upperTail_mono {n : ℕ} {p p' : ℝ} (hp0 : 0 ≤ p) (hpp' : p ≤ p') (hp1 : p' ≤ 1)
    (m : ℕ) : upperTail n p m ≤ upperTail n p' m

Uses 2 · Used by 1

Statement usesBinomial upper tail probability

Proof usesBinomial probability mass function

Used byPower increases with the allelic fraction

TheoremThe binomial likelihood is unimodal in p, increasing part#✓fully proved

For a ≤ n and 0 ≤ p ≤ p' ≤ a / n, Binom(a | n, p) ≤ Binom(a | n, p').

theorem binomPmf_le_binomPmf_of_le_div {n a : ℕ} {p p' : ℝ} (ha : a ≤ n) (hp0 : 0 ≤ p)
    (hpp' : p ≤ p') (hp' : p' ≤ a / n) : binomPmf n p a ≤ binomPmf n p' a

Uses 2 · Used by 1

Statement usesBinomial probability mass function

Proof usesNonnegativity of binomial probabilities

Used byThe continuous CCF MLE

TheoremThe binomial likelihood is unimodal in p, decreasing part#✓fully proved

For a ≤ n and a / n ≤ p ≤ p' ≤ 1, Binom(a | n, p') ≤ Binom(a | n, p).

theorem binomPmf_le_binomPmf_of_div_le {n a : ℕ} {p p' : ℝ} (ha : a ≤ n) (hp : a / n ≤ p)
    (hpp' : p ≤ p') (hp1 : p' ≤ 1) : binomPmf n p' a ≤ binomPmf n p a

Uses 2 · Used by 1

Statement usesBinomial probability mass function

Proof usesNonnegativity of binomial probabilities

Used byThe continuous CCF MLE

DefinitionCritical count of the mutation detection test#✓fully proved

Carter's critical count k = min {m | P(m) ≤ FPR} for the null success probability p₀ = ε / 3 (Online Methods, before Eq. 9).

noncomputable def criticalCount (n : ℕ) (p₀ fpr : ℝ) : ℕ := sInf {m | upperTail n p₀ m ≤ fpr}

Uses 1 · Used by 11

Statement usesBinomial upper tail probability

Used byUpper bound on the critical count · Positivity of the critical count · Minimality of the critical count · Power of the randomized mutation detection test · Detection power as a mixture of tail probabilities · Power increases with the allelic fraction · Exact size · Randomization probability of the detection test · The randomization is a probability · Critical count meets the false-positive bound · Tail gap at the critical count

DefinitionRandomization probability of the detection test#✓fully proved

The randomization probability d = (FPR - P(k)) / (P(k - 1) - P(k)) of Eq. 9.

noncomputable def randomization (n : ℕ) (p₀ fpr : ℝ) : ℝ :=
  (fpr - upperTail n p₀ (criticalCount n p₀ fpr)) /
    (upperTail n p₀ (criticalCount n p₀ fpr - 1) - upperTail n p₀ (criticalCount n p₀ fpr))

Uses 2 · Used by 5

Statement usesCritical count of the mutation detection test · Binomial upper tail probability

Used byPower of the randomized mutation detection test · Detection power as a mixture of tail probabilities · Power increases with the allelic fraction · Exact size · The randomization is a probability

DefinitionPower of the randomized mutation detection test#✓fully proved

The power Pow(n, f) = P_f(X ≥ k) + d Binom(k - 1 | n, f) of the exact-size randomized test (Carter et al. 2012, Eq. 9, with the randomization at k - 1; see the module doc).

noncomputable def power (n : ℕ) (p₀ fpr f : ℝ) : ℝ :=
  upperTail n f (criticalCount n p₀ fpr) +
    randomization n p₀ fpr * binomPmf n f (criticalCount n p₀ fpr - 1)

Uses 4 · Used by 6

Statement usesBinomial probability mass function · Critical count of the mutation detection test · Randomization probability of the detection test · Binomial upper tail probability

Used byDetection power as a mixture of tail probabilities · Power increases with the allelic fraction · Exact size · Power decreases with local copy number · Power increases with multiplicity · Power increases with purity

TheoremCritical count meets the false-positive bound#✓fully proved

The critical count meets the false-positive bound: P(k) ≤ FPR (for FPR ≥ 0).

theorem upperTail_criticalCount_le {n : ℕ} {p₀ fpr : ℝ} (hfpr : 0 ≤ fpr) :
    upperTail n p₀ (criticalCount n p₀ fpr) ≤ fpr

Uses 3 · Used by 3

Statement usesCritical count of the mutation detection test · Binomial upper tail probability

Proof usesBinomial upper tail beyond n is zero

Used byPositivity of the critical count · Exact size · The randomization is a probability

TheoremUpper bound on the critical count#✓fully proved

The critical count is at most n + 1 (for FPR ≥ 0).

theorem criticalCount_le {n : ℕ} {p₀ fpr : ℝ} (hfpr : 0 ≤ fpr) :
    criticalCount n p₀ fpr ≤ n + 1

Uses 3

Statement usesCritical count of the mutation detection test

Proof usesBinomial upper tail probability · Binomial upper tail beyond n is zero

TheoremPositivity of the critical count#✓fully proved

The critical count is positive when FPR < 1.

theorem criticalCount_pos {n : ℕ} {p₀ fpr : ℝ} (hfpr : 0 ≤ fpr) (hfpr1 : fpr < 1) :
    0 < criticalCount n p₀ fpr

Uses 4 · Used by 3

Statement usesCritical count of the mutation detection test

Proof usesBinomial upper tail probability · Critical count meets the false-positive bound · Binomial upper tail from zero is one

Used byMinimality of the critical count · Detection power as a mixture of tail probabilities · Tail gap at the critical count

TheoremMinimality of the critical count#✓fully proved

Minimality of the critical count: FPR < P(k - 1) (for 0 ≤ FPR < 1).

theorem lt_upperTail_criticalCount_sub_one {n : ℕ} {p₀ fpr : ℝ} (hfpr : 0 ≤ fpr)
    (hfpr1 : fpr < 1) : fpr < upperTail n p₀ (criticalCount n p₀ fpr - 1)

Uses 3 · Used by 2

Statement usesCritical count of the mutation detection test · Binomial upper tail probability

Proof usesPositivity of the critical count

Used byExact size · The randomization is a probability

TheoremTail gap at the critical count#✓fully proved

The gap P(k - 1) - P(k) is the null probability of the boundary point k - 1.

theorem upperTail_sub_one_sub {n : ℕ} {p₀ fpr : ℝ} (hfpr : 0 ≤ fpr) (hfpr1 : fpr < 1) :
    upperTail n p₀ (criticalCount n p₀ fpr - 1) - upperTail n p₀ (criticalCount n p₀ fpr) =
      binomPmf n p₀ (criticalCount n p₀ fpr - 1)

Uses 5 · Used by 1

Statement usesBinomial probability mass function · Critical count of the mutation detection test · Binomial upper tail probability

Proof usesPositivity of the critical count · Recursion for the binomial upper tail

Used byExact size

TheoremThe randomization is a probability#✓fully proved

0 ≤ d < 1 for 0 ≤ FPR < 1.

theorem randomization_mem {n : ℕ} {p₀ fpr : ℝ} (hfpr : 0 ≤ fpr) (hfpr1 : fpr < 1) :
    0 ≤ randomization n p₀ fpr ∧ randomization n p₀ fpr < 1

Uses 5 · Used by 1

Statement usesRandomization probability of the detection test

Proof usesCritical count of the mutation detection test · Minimality of the critical count · Binomial upper tail probability · Critical count meets the false-positive bound

Used byPower increases with the allelic fraction

TheoremExact size#✓fully proved

Exact size (Carter et al. 2012, Eq. 9 with the randomization at k - 1): under the null f = p₀ the rejection probability is exactly FPR, for 0 ≤ FPR < 1.

theorem power_self {n : ℕ} {p₀ fpr : ℝ} (hfpr : 0 ≤ fpr) (hfpr1 : fpr < 1) :
    power n p₀ fpr p₀ = fpr

Uses 8

Statement usesPower of the randomized mutation detection test

Proof usesBinomial probability mass function · Critical count of the mutation detection test · Minimality of the critical count · Randomization probability of the detection test · Binomial upper tail probability · Critical count meets the false-positive bound · Tail gap at the critical count

TheoremDetection power as a mixture of tail probabilities#✓fully proved

The power is the mixture (1 - d) P_f(X ≥ k) + d P_f(X ≥ k - 1) of two tail probabilities.

theorem power_eq_mix {n : ℕ} {p₀ fpr : ℝ} (hfpr : 0 ≤ fpr) (hfpr1 : fpr < 1) (f : ℝ) :
    power n p₀ fpr f = (1 - randomization n p₀ fpr) * upperTail n f (criticalCount n p₀ fpr) +
      randomization n p₀ fpr * upperTail n f (criticalCount n p₀ fpr - 1)

Uses 7 · Used by 1

Statement usesCritical count of the mutation detection test · Power of the randomized mutation detection test · Randomization probability of the detection test · Binomial upper tail probability

Proof usesBinomial probability mass function · Positivity of the critical count · Recursion for the binomial upper tail

Used byPower increases with the allelic fraction

TheoremPower increases with the allelic fraction#✓fully proved

Pow(n, f) ≤ Pow(n, f') for 0 ≤ f ≤ f' ≤ 1.

theorem power_mono {n : ℕ} {p₀ fpr f f' : ℝ} (hfpr : 0 ≤ fpr) (hfpr1 : fpr < 1) (hf0 : 0 ≤ f)
    (hff' : f ≤ f') (hf1 : f' ≤ 1) : power n p₀ fpr f ≤ power n p₀ fpr f'

Uses 7 · Used by 3

Statement usesPower of the randomized mutation detection test

Proof usesCritical count of the mutation detection test · Detection power as a mixture of tail probabilities · Randomization probability of the detection test · The randomization is a probability · Binomial upper tail probability · Binomial tails increase with the success probability

Used byPower decreases with local copy number · Power increases with multiplicity · Power increases with purity

TheoremPower increases with purity#✓fully proved

Power increases with purity at the ABSOLUTE allelic fraction α s / (α q + 2 (1 - α)) of a clonal mutation of multiplicity 0 ≤ s ≤ q (Carter et al. 2012, Eqs. 2, 9, 10).

theorem power_somaticAF_mono_purity {n : ℕ} {p₀ fpr α α' q s : ℝ} (hfpr : 0 ≤ fpr)
    (hfpr1 : fpr < 1) (hα0 : 0 ≤ α) (hαα' : α ≤ α') (hα1 : α' ≤ 1) (hq : 0 < q) (hs : 0 ≤ s)
    (hsq : s ≤ q) : power n p₀ fpr (somaticAF α q s) ≤ power n p₀ fpr (somaticAF α' q s)

Uses 6

Statement usesExpected allelic fraction of a somatic mutation · Power of the randomized mutation detection test

Proof usesSomatic allelic fraction is at most one · Somatic allelic fraction increases with purity · Nonnegativity of somatic allelic fractions · Power increases with the allelic fraction

TheoremPower decreases with local copy number#✓fully proved

Power decreases with local copy number at the ABSOLUTE allelic fraction, for a clonal mutation of multiplicity 0 ≤ s ≤ q ≤ q' (Carter et al. 2012, Eqs. 2, 9, 10).

theorem power_somaticAF_anti_copy {n : ℕ} {p₀ fpr α q q' s : ℝ} (hfpr : 0 ≤ fpr)
    (hfpr1 : fpr < 1) (hα0 : 0 ≤ α) (hα1 : α ≤ 1) (hq : 0 < q) (hqq' : q ≤ q') (hs : 0 ≤ s)
    (hsq : s ≤ q) : power n p₀ fpr (somaticAF α q' s) ≤ power n p₀ fpr (somaticAF α q s)

Uses 6

Statement usesExpected allelic fraction of a somatic mutation · Power of the randomized mutation detection test

Proof usesSomatic allelic fraction decreases with copy number · Somatic allelic fraction is at most one · Nonnegativity of somatic allelic fractions · Power increases with the allelic fraction

TheoremPower increases with multiplicity#✓fully proved

Power increases with multiplicity at the ABSOLUTE allelic fraction, for 0 ≤ s ≤ s' ≤ q (Carter et al. 2012, Eqs. 2, 9).

theorem power_somaticAF_mono_mult {n : ℕ} {p₀ fpr α q s s' : ℝ} (hfpr : 0 ≤ fpr)
    (hfpr1 : fpr < 1) (hα0 : 0 ≤ α) (hα1 : α ≤ 1) (hq : 0 < q) (hs : 0 ≤ s) (hss' : s ≤ s')
    (hs'q : s' ≤ q) : power n p₀ fpr (somaticAF α q s) ≤ power n p₀ fpr (somaticAF α q s')

Uses 6

Statement usesExpected allelic fraction of a somatic mutation · Power of the randomized mutation detection test

Proof usesSomatic allelic fraction is at most one · Somatic allelic fraction increases with multiplicity · Nonnegativity of somatic allelic fractions · Power increases with the allelic fraction

30 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.