Cancer cell fraction estimation

DefinitionPosterior tail probability on a grid#✓fully proved

Posterior probability that the parameter c i exceeds t, for prior weights prior and likelihoods lik i of the observed data: ∑_{c i > t} prior i lik i / ∑_i prior i lik i.

noncomputable def tailRatio (prior lik c : ι → ℝ) (t : ℝ) : ℝ :=
  (∑ i with t < c i, prior i * lik i) / ∑ i, prior i * lik i
Used by 2

TheoremMonotone likelihood ratio implies stochastically larger posteriors#✓fully proved

If the kernels L (data x) and L' (data x') satisfy the TP2 inequality L' i L j ≥ L i L' j whenever c j ≤ c i, then for a nonnegative prior every posterior tail P(c > t) is at least as large under L' as under L (both normalizers positive).

theorem posteriorTail_mono_of_tp2 (prior L L' c : ι → ℝ) (t : ℝ)
    (hprior : ∀ i, 0 ≤ prior i)
    (htp2 : ∀ i j, c j ≤ c i → L i * L' j ≤ L' i * L j)
    (hZ : 0 < ∑ i, prior i * L i) (hZ' : 0 < ∑ i, prior i * L' i) :
    tailRatio prior L c t ≤ tailRatio prior L' c t
Uses 1 · Used by 1

TheoremThe binomial family is TP2#✓fully proved

The binomial family is TP2 (monotone likelihood ratio in the success probability): for a ≤ a' and 0 ≤ p ≤ p' ≤ 1, Binom(a | n, p') Binom(a' | n, p) ≤ Binom(a' | n, p') Binom(a | n, p).

theorem binomPmf_mul_le_mul {n a a' : ℕ} {p p' : ℝ} (haa' : a ≤ a') (hp0 : 0 ≤ p)
    (hpp' : p ≤ p') (hp1 : p' ≤ 1) :
    binomPmf n p' a * binomPmf n p a' ≤ binomPmf n p' a' * binomPmf n p a
Uses 2 · Used by 1

DefinitionPosterior probability that the cancer cell fraction exceeds a threshold#✓fully proved

Landau et al.'s posterior probability that the CCF exceeds t, given a of n reads, purity α, copy number q, a prior prior on the grid points grid k: ∑_{grid k > t} π_k Binom(a | n, f(grid k)) / ∑_k π_k Binom(a | n, f(grid k)), with f(c) = α c / (α q + 2 (1 - α)).

noncomputable def posteriorTail {m : ℕ} (prior grid : Fin m → ℝ) (α q : ℝ) (n a : ℕ)
    (t : ℝ) : ℝ :=
  tailRatio prior (fun k => binomPmf n (somaticAF α q (grid k)) a) grid t
Uses 3 · Used by 3

DefinitionClonal call for a mutation#✓fully proved

Landau et al.'s clonal call: P(CCF > t | a) > γ (they take t = 0.95, γ = 0.5).

def IsClonal {m : ℕ} (prior grid : Fin m → ℝ) (α q : ℝ) (n a : ℕ) (t γ : ℝ) : Prop :=
  γ < posteriorTail prior grid α q n a t
Uses 1 · Used by 2

StructureGrid model for the cancer cell fraction#✓fully proved

Hypotheses on the CCF grid model: purity 0 < α ≤ 1, copy number q > 0, grid in [0, q] and within the defining CCF bound ≤ 1, a nonnegative prior, and one grid point of positive prior weight whose allelic fraction lies strictly inside (0, 1) (this makes every posterior well defined).

structure GridModel {m : ℕ} (prior grid : Fin m → ℝ) (α q : ℝ) : Prop where
  purity_pos : 0 < α
  purity_le_one : α ≤ 1
  copy_pos : 0 < q
  grid_nonneg : ∀ k, 0 ≤ grid k
  grid_le : ∀ k, grid k ≤ q
  grid_le_one : ∀ k, grid k ≤ 1
  prior_nonneg : ∀ k, 0 ≤ prior k
  exists_interior : ∃ k, 0 < prior k ∧ 0 < somaticAF α q (grid k) ∧ somaticAF α q (grid k) < 1
Uses 1 · Used by 4

TheoremPositivity of the grid posterior normalizer#✓fully proved

In a grid model every posterior normalizer ∑_k π_k Binom(a | n, f(grid k)), a ≤ n, is positive.

theorem GridModel.normalizer_pos {m : ℕ} {prior grid : Fin m → ℝ} {α q : ℝ}
    (h : GridModel prior grid α q) {n a : ℕ} (ha : a ≤ n) :
    0 < ∑ k, prior k * binomPmf n (somaticAF α q (grid k)) a
Uses 7 · Used by 1

TheoremThe CCF posterior is stochastically increasing in the read count#✓fully proved

The CCF posterior is stochastically increasing in the read count (Landau et al. 2013 with the monotone-likelihood-ratio argument): P(CCF > t | a) ≤ P(CCF > t | a') for a ≤ a' ≤ n.

theorem posteriorTail_mono {m : ℕ} {prior grid : Fin m → ℝ} {α q : ℝ}
    (h : GridModel prior grid α q) {n a a' : ℕ} (haa' : a ≤ a') (ha' : a' ≤ n) (t : ℝ) :
    posteriorTail prior grid α q n a t ≤ posteriorTail prior grid α q n a' t
Uses 10 · Used by 1

TheoremThe clonal call is upward closed in the read count#✓fully proved

The clonal call is upward closed in the read count.

theorem IsClonal.mono {m : ℕ} {prior grid : Fin m → ℝ} {α q : ℝ}
    (h : GridModel prior grid α q) {n a a' : ℕ} {t γ : ℝ} (haa' : a ≤ a') (ha' : a' ≤ n)
    (hc : IsClonal prior grid α q n a t γ) : IsClonal prior grid α q n a' t γ
Uses 4 · Used by 1

TheoremThe clonal call is a read-count threshold#✓fully proved

For every CCF threshold t and posterior level γ there is a₀ such that, for a ≤ n, the mutation is called clonal iff a₀ ≤ a (a₀ = n + 1 when no count is called clonal).

theorem exists_threshold {m : ℕ} {prior grid : Fin m → ℝ} {α q : ℝ}
    (h : GridModel prior grid α q) (n : ℕ) (t γ : ℝ) :
    ∃ a₀, ∀ a ≤ n, IsClonal prior grid α q n a t γ ↔ a₀ ≤ a
Uses 3

DefinitionMaximum-likelihood cancer cell fraction#✓fully proved

The continuous maximum-likelihood CCF ĉ = min 1 (a / (n κ)) for the allelic-fraction slope κ = α / (α q + 2 (1 - α)). Landau et al. (2013) use the grid posterior; this continuous maximizer over [0, 1] is derived here.

noncomputable def ccfMLE (α q : ℝ) (n a : ℕ) : ℝ := min 1 ((a : ℝ) / n / somaticAF α q 1)
Uses 1 · Used by 1

TheoremThe continuous CCF MLE#✓fully proved

For 0 < α ≤ 1, q ≥ 1, a ≤ n and 0 < n, the likelihood c ↦ Binom(a | n, f(c)) on [0, 1] is maximized at ĉ = min 1 (a / (n κ)).

theorem isMaxOn_ccfMLE {α q : ℝ} {n a : ℕ} (hα0 : 0 < α) (hα1 : α ≤ 1) (hq : 1 ≤ q)
    (ha : a ≤ n) (hn : 0 < n) :
    IsMaxOn (fun c => binomPmf n (somaticAF α q c) a) (Set.Icc 0 1) (ccfMLE α q n a)
Uses 8
12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.