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
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
noncomputable def tailRatio (prior lik c : ι → ℝ) (t : ℝ) : ℝ :=
(∑ i with t < c i, prior i * lik i) / ∑ i, prior i * lik i
MathlibExt/Biology/CancerGenomics/CancerCellFraction.lean:76
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
def binomPmf (n : ℕ) (p : ℝ) (i : ℕ) : ℝ := (n.choose i : ℝ) * p ^ i * (1 - p) ^ (n - i)
MathlibExt/Biology/CancerGenomics/DetectionPower.lean:70
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
noncomputable def tailRatio (prior lik c : ι → ℝ) (t : ℝ) : ℝ :=
(∑ i with t < c i, prior i * lik i) / ∑ i, prior i * lik i
MathlibExt/Biology/CancerGenomics/CancerCellFraction.lean:76
def binomPmf (n : ℕ) (p : ℝ) (i : ℕ) : ℝ := (n.choose i : ℝ) * p ^ i * (1 - p) ^ (n - i)
MathlibExt/Biology/CancerGenomics/DetectionPower.lean:70
noncomputable def somaticAF (α q s : ℝ) : ℝ := α * s / mixCopy α q
MathlibExt/Biology/CancerGenomics/Absolute.lean:94
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
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
MathlibExt/Biology/CancerGenomics/CancerCellFraction.lean:145
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
noncomputable def somaticAF (α q s : ℝ) : ℝ := α * s / mixCopy α q
MathlibExt/Biology/CancerGenomics/Absolute.lean:94
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
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
MathlibExt/Biology/CancerGenomics/CancerCellFraction.lean:157
def binomPmf (n : ℕ) (p : ℝ) (i : ℕ) : ℝ := (n.choose i : ℝ) * p ^ i * (1 - p) ^ (n - i)
MathlibExt/Biology/CancerGenomics/DetectionPower.lean:70
noncomputable def somaticAF (α q s : ℝ) : ℝ := α * s / mixCopy α q
MathlibExt/Biology/CancerGenomics/Absolute.lean:94
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
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
MathlibExt/Biology/CancerGenomics/CancerCellFraction.lean:157
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
MathlibExt/Biology/CancerGenomics/CancerCellFraction.lean:145
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 γ
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
MathlibExt/Biology/CancerGenomics/CancerCellFraction.lean:157
def IsClonal {m : ℕ} (prior grid : Fin m → ℝ) (α q : ℝ) (n a : ℕ) (t γ : ℝ) : Prop :=
γ < posteriorTail prior grid α q n a t
MathlibExt/Biology/CancerGenomics/CancerCellFraction.lean:150
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
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
MathlibExt/Biology/CancerGenomics/CancerCellFraction.lean:157
def IsClonal {m : ℕ} (prior grid : Fin m → ℝ) (α q : ℝ) (n a : ℕ) (t γ : ℝ) : Prop :=
γ < posteriorTail prior grid α q n a t
MathlibExt/Biology/CancerGenomics/CancerCellFraction.lean:150
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)
noncomputable def somaticAF (α q s : ℝ) : ℝ := α * s / mixCopy α q
MathlibExt/Biology/CancerGenomics/Absolute.lean:94
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)
def binomPmf (n : ℕ) (p : ℝ) (i : ℕ) : ℝ := (n.choose i : ℝ) * p ^ i * (1 - p) ^ (n - i)
MathlibExt/Biology/CancerGenomics/DetectionPower.lean:70
noncomputable def somaticAF (α q s : ℝ) : ℝ := α * s / mixCopy α q
MathlibExt/Biology/CancerGenomics/Absolute.lean:94
noncomputable def ccfMLE (α q : ℝ) (n a : ℕ) : ℝ := min 1 ((a : ℝ) / n / somaticAF α q 1)
MathlibExt/Biology/CancerGenomics/CancerCellFraction.lean:219
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.