Tumour purity, ploidy and copy-ratio algebra

DefinitionAverage absolute copy number of a tumor sample#✓fully proved

Average absolute copy number α q + 2 (1 - α) of a locus with copy number q in the cancer cells, in a sample of purity α whose normal cells are diploid (Carter et al. 2012). With q = τ this is the sample ploidy D of Eq. 1; with the local copy number it is D_s of Eq. 2.

def mixCopy (α q : ℝ) : ℝ := α * q + 2 * (1 - α)

Used by 21

Used byThe continuous CCF MLE · Purity and ploidy are identifiable from the slope and intercept of Eq. 1 · Relative copy ratio · Eq. 1 is affine in q · Ploidy-scaling non-identifiability, copy ratios · Expected allelic fraction of a germline variant · Ploidy-scaling non-identifiability, germline allelic fractions · Copy-ratio intercept · Positivity of the mixture copy number · Ploidy from copy-ratio slope and intercept · Purity from copy-ratio slope and intercept · Copy-ratio slope · Expected allelic fraction of a somatic mutation · Somatic allelic fraction decreases with copy number · Allelic fractions are determined by the copy-ratio slope · Somatic allelic fraction is at most one · Somatic allelic fraction increases with multiplicity · Somatic allelic fraction increases with purity · Nonnegativity of somatic allelic fractions · Ploidy-scaling non-identifiability, somatic allelic fractions · Calibrated copy ratios have mean 1

DefinitionRelative copy ratio#✓fully proved

Relative copy ratio R = (α q + 2 (1 - α)) / (α τ + 2 (1 - α)) of a locus with copy number q, purity α and cancer-cell ploidy τ (Carter et al. 2012, Eq. 1).

noncomputable def copyRatio (α τ q : ℝ) : ℝ := mixCopy α q / mixCopy α τ

Uses 1 · Used by 5

Statement usesAverage absolute copy number of a tumor sample

Used byGenome doubling · Eq. 1 is affine in q · Ploidy-scaling non-identifiability, copy ratios · Allelic fractions are determined by the copy-ratio slope · Calibrated copy ratios have mean 1

DefinitionCopy-ratio slope#✓fully proved

The copy-ratio slope α / D of Eq. 1 (Carter et al. 2012), the copy ratio of one extra copy per cancer cell.

noncomputable def slope (α τ : ℝ) : ℝ := α / mixCopy α τ

Uses 1 · Used by 5

Statement usesAverage absolute copy number of a tumor sample

Used byPurity and ploidy are identifiable from the slope and intercept of Eq. 1 · Eq. 1 is affine in q · Ploidy from copy-ratio slope and intercept · Purity from copy-ratio slope and intercept · Allelic fractions are determined by the copy-ratio slope

DefinitionCopy-ratio intercept#✓fully proved

The copy-ratio intercept 2 (1 - α) / D of Eq. 1 (Carter et al. 2012), the copy ratio of a homozygously deleted locus.

noncomputable def intercept (α τ : ℝ) : ℝ := 2 * (1 - α) / mixCopy α τ

Uses 1 · Used by 4

Statement usesAverage absolute copy number of a tumor sample

Used byPurity and ploidy are identifiable from the slope and intercept of Eq. 1 · Eq. 1 is affine in q · Ploidy from copy-ratio slope and intercept · Purity from copy-ratio slope and intercept

DefinitionExpected allelic fraction of a somatic mutation#✓fully proved

Expected allelic fraction α s / (α q + 2 (1 - α)) of a clonal somatic point mutation with multiplicity s (copies per cancer cell) at a locus of copy number q (Carter et al. 2012, Eq. 2; Eq. 10 is s = 1).

noncomputable def somaticAF (α q s : ℝ) : ℝ := α * s / mixCopy α q

Uses 1 · Used by 16

Statement usesAverage absolute copy number of a tumor sample

Used byMaximum-likelihood cancer cell fraction · Grid model for the cancer cell fraction · 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 · Power decreases with local copy number · Power increases with multiplicity · Power increases with purity · Somatic allelic fraction decreases with copy number · Allelic fractions are determined by the copy-ratio slope · Somatic allelic fraction is at most one · Somatic allelic fraction increases with multiplicity · Somatic allelic fraction increases with purity · Nonnegativity of somatic allelic fractions · Ploidy-scaling non-identifiability, somatic allelic fractions

DefinitionExpected allelic fraction of a germline variant#✓fully proved

Expected allelic fraction ((1 - α) + α g) / (α q + 2 (1 - α)) of a heterozygous germline variant present in g copies per cancer cell at a locus of copy number q (Carter et al. 2012, Eq. 11).

noncomputable def germlineAF (α q g : ℝ) : ℝ := ((1 - α) + α * g) / mixCopy α q

Uses 1 · Used by 1

Statement usesAverage absolute copy number of a tumor sample

Used byPloidy-scaling non-identifiability, germline allelic fractions

DefinitionRescaled purity#✓fully proved

The purity α / (m - (m - 1) α) that, together with all copy numbers multiplied by m, reproduces the copy ratios and allelic fractions of purity α (derived from Carter et al. 2012, Eqs. 1, 2, 11).

noncomputable def scaledPurity (m α : ℝ) : ℝ := α / (m - (m - 1) * α)

Used by 6

Used byGenome doubling · Ploidy-scaling non-identifiability, copy ratios · Ploidy-scaling non-identifiability, germline allelic fractions · Rescaled purity lies in (0, 1) · Rescaled purity differs from the original purity · Ploidy-scaling non-identifiability, somatic allelic fractions

TheoremPositivity of the mixture copy number#✓fully proved

The mixture copy number is positive in the biological domain 0 ≤ α ≤ 1, 0 < q.

theorem mixCopy_pos {α q : ℝ} (hα0 : 0 ≤ α) (hα1 : α ≤ 1) (hq : 0 < q) :
    0 < mixCopy α q

Uses 1 · Used by 9

Statement usesAverage absolute copy number of a tumor sample

Used byThe continuous CCF MLE · Purity and ploidy are identifiable from the slope and intercept of Eq. 1 · Ploidy from copy-ratio slope and intercept · Purity from copy-ratio slope and intercept · Somatic allelic fraction decreases with copy number · Somatic allelic fraction is at most one · Somatic allelic fraction increases with multiplicity · Somatic allelic fraction increases with purity · Nonnegativity of somatic allelic fractions

TheoremEq. 1 is affine in q#✓fully proved

R = (α / D) q + 2 (1 - α) / D, for all real arguments.

theorem copyRatio_eq_slope_mul_add_intercept (α τ q : ℝ) :
    copyRatio α τ q = slope α τ * q + intercept α τ

Uses 4

Statement usesRelative copy ratio · Copy-ratio intercept · Copy-ratio slope

Proof usesAverage absolute copy number of a tumor sample

TheoremCalibrated copy ratios have mean 1#✓fully proved

If the segment weights w sum to one and the ploidy is the weighted mean copy number τ = ∑ w q, the weighted mean copy ratio is 1 (Carter et al. 2012, Methods: "correctly calibrated copy-ratio data always has mean = 1").

theorem sum_mul_copyRatio_eq_one {ι : Type*} (s : Finset ι) (w q : ι → ℝ) {α : ℝ}
    (hw : ∑ i ∈ s, w i = 1) (hD : mixCopy α (∑ i ∈ s, w i * q i) ≠ 0) :
    ∑ i ∈ s, w i * copyRatio α (∑ j ∈ s, w j * q j) (q i) = 1

Uses 2

Statement usesRelative copy ratio · Average absolute copy number of a tumor sample

TheoremAllelic fractions are determined by the copy-ratio slope#✓fully proved

Allelic fractions are determined by the copy-ratio slope (Carter et al. 2012, Eq. 2): α s / D_s = (α / D) s / R, whenever D ≠ 0.

theorem somaticAF_eq_slope_mul_div_copyRatio {α τ q : ℝ} (s : ℝ) (hD : mixCopy α τ ≠ 0) :
    somaticAF α q s = slope α τ * s / copyRatio α τ q

Uses 4

Statement usesRelative copy ratio · Average absolute copy number of a tumor sample · Copy-ratio slope · Expected allelic fraction of a somatic mutation

TheoremPurity from copy-ratio slope and intercept#✓fully proved

Inverse of Eq. 1, purity: α = 2 b / (2 b + δ) for the slope b and intercept δ, when 0 < α ≤ 1 and 0 < τ.

theorem purity_eq {α τ : ℝ} (hα0 : 0 < α) (hα1 : α ≤ 1) (hτ : 0 < τ) :
    α = 2 * slope α τ / (2 * slope α τ + intercept α τ)

Uses 4 · Used by 1

Statement usesCopy-ratio intercept · Copy-ratio slope

Proof usesAverage absolute copy number of a tumor sample · Positivity of the mixture copy number

Used byPurity and ploidy are identifiable from the slope and intercept of Eq. 1

TheoremPloidy from copy-ratio slope and intercept#✓fully proved

Inverse of Eq. 1, ploidy: τ = (1 - δ) / b for the slope b and intercept δ, when 0 < α ≤ 1 and 0 < τ.

theorem ploidy_eq {α τ : ℝ} (hα0 : 0 < α) (hα1 : α ≤ 1) (hτ : 0 < τ) :
    τ = (1 - intercept α τ) / slope α τ

Uses 4 · Used by 1

Statement usesCopy-ratio intercept · Copy-ratio slope

Proof usesAverage absolute copy number of a tumor sample · Positivity of the mixture copy number

Used byPurity and ploidy are identifiable from the slope and intercept of Eq. 1

TheoremPurity and ploidy are identifiable from the slope and intercept of Eq. 1#✓fully proved

The map (α, τ) ↦ (α / D, 2 (1 - α) / D) is a bijection from {0 < α ≤ 1, 0 < τ} onto {0 < b, 0 ≤ δ < 1}.

theorem bijOn_slope_intercept :
    Set.BijOn (fun p : ℝ × ℝ => (slope p.1 p.2, intercept p.1 p.2))
      {p | 0 < p.1 ∧ p.1 ≤ 1 ∧ 0 < p.2} {x | 0 < x.1 ∧ 0 ≤ x.2 ∧ x.2 < 1}

Uses 6

Statement usesCopy-ratio intercept · Copy-ratio slope

Proof usesAverage absolute copy number of a tumor sample · Positivity of the mixture copy number · Ploidy from copy-ratio slope and intercept · Purity from copy-ratio slope and intercept

TheoremPositivity of the rescaled purity denominator#✓fully proved

The denominator m - (m - 1) α = m (1 - α) + α of the rescaled purity is positive for m > 0 and 0 ≤ α ≤ 1.

theorem scaledPurity_denom_pos {m α : ℝ} (hm : 0 < m) (hα0 : 0 ≤ α) (hα1 : α ≤ 1) :
    0 < m - (m - 1) * α

Used by 5

Used byPloidy-scaling non-identifiability, copy ratios · Ploidy-scaling non-identifiability, germline allelic fractions · Rescaled purity lies in (0, 1) · Rescaled purity differs from the original purity · Ploidy-scaling non-identifiability, somatic allelic fractions

TheoremRescaled purity lies in (0, 1)#✓fully proved

The rescaled purity is again a purity: 0 ≤ α / (m - (m - 1) α) ≤ 1 for m > 0 and 0 ≤ α ≤ 1.

theorem scaledPurity_mem {m α : ℝ} (hm : 0 < m) (hα0 : 0 ≤ α) (hα1 : α ≤ 1) :
    0 ≤ scaledPurity m α ∧ scaledPurity m α ≤ 1

Uses 2

Statement usesRescaled purity

Proof usesPositivity of the rescaled purity denominator

TheoremPloidy-scaling non-identifiability, copy ratios#✓fully proved

Scaling every copy number and the ploidy by m > 0 and the purity to α / (m - (m - 1) α) leaves every copy ratio of Eq. 1 unchanged.

theorem copyRatio_scale {m α : ℝ} (hm : 0 < m) (hα0 : 0 ≤ α) (hα1 : α ≤ 1) (τ q : ℝ) :
    copyRatio (scaledPurity m α) (m * τ) (m * q) = copyRatio α τ q

Uses 4 · Used by 1

Statement usesRelative copy ratio · Rescaled purity

Proof usesAverage absolute copy number of a tumor sample · Positivity of the rescaled purity denominator

Used byGenome doubling

TheoremPloidy-scaling non-identifiability, somatic allelic fractions#✓fully proved

Ploidy-scaling non-identifiability, somatic allelic fractions (Eq. 2): with copy number and multiplicity both scaled by m > 0 and the purity rescaled, the allelic fraction is unchanged.

theorem somaticAF_scale {m α : ℝ} (hm : 0 < m) (hα0 : 0 ≤ α) (hα1 : α ≤ 1) (q s : ℝ) :
    somaticAF (scaledPurity m α) (m * q) (m * s) = somaticAF α q s

Uses 4

Statement usesRescaled purity · Expected allelic fraction of a somatic mutation

Proof usesAverage absolute copy number of a tumor sample · Positivity of the rescaled purity denominator

TheoremPloidy-scaling non-identifiability, germline allelic fractions#✓fully proved

Ploidy-scaling non-identifiability, germline allelic fractions (Eq. 11): with copy number and germline multiplicity both scaled by m > 0 and the purity rescaled, the allelic fraction is unchanged.

theorem germlineAF_scale {m α : ℝ} (hm : 0 < m) (hα0 : 0 ≤ α) (hα1 : α ≤ 1) (q g : ℝ) :
    germlineAF (scaledPurity m α) (m * q) (m * g) = germlineAF α q g

Uses 4

Statement usesExpected allelic fraction of a germline variant · Rescaled purity

Proof usesAverage absolute copy number of a tumor sample · Positivity of the rescaled purity denominator

TheoremRescaled purity differs from the original purity#✓fully proved

The rescaled solution is a genuinely different purity: for 0 < α < 1 and m ≠ 1, α / (m - (m - 1) α) ≠ α.

theorem scaledPurity_ne {m α : ℝ} (hm : 0 < m) (hm1 : m ≠ 1) (hα0 : 0 < α) (hα1 : α < 1) :
    scaledPurity m α ≠ α

Uses 2

Statement usesRescaled purity

Proof usesPositivity of the rescaled purity denominator

TheoremGenome doubling#✓fully proved

Doubling every copy number and the ploidy and replacing the purity by α / (2 - α) reproduces every copy ratio (the m = 2 case of copyRatio_scale).

theorem copyRatio_doubling {α : ℝ} (hα0 : 0 ≤ α) (hα1 : α ≤ 1) (τ q : ℝ) :
    copyRatio (α / (2 - α)) (2 * τ) (2 * q) = copyRatio α τ q

Uses 3

Statement usesRelative copy ratio

Proof usesPloidy-scaling non-identifiability, copy ratios · Rescaled purity

TheoremNonnegativity of somatic allelic fractions#✓fully proved

Somatic allelic fractions are nonnegative in the biological domain.

theorem somaticAF_nonneg {α q s : ℝ} (hα0 : 0 ≤ α) (hα1 : α ≤ 1) (hq : 0 < q) (hs : 0 ≤ s) :
    0 ≤ somaticAF α q s

Uses 3 · Used by 5

Statement usesExpected allelic fraction of a somatic mutation

Proof usesAverage absolute copy number of a tumor sample · Positivity of the mixture copy number

Used byPositivity of the grid posterior normalizer · The CCF posterior is stochastically increasing in the read count · Power decreases with local copy number · Power increases with multiplicity · Power increases with purity

TheoremSomatic allelic fraction is at most one#✓fully proved

A somatic allelic fraction is at most one when the multiplicity does not exceed the copy number (s ≤ q).

theorem somaticAF_le_one {α q s : ℝ} (hα0 : 0 ≤ α) (hα1 : α ≤ 1) (hq : 0 < q) (hsq : s ≤ q) :
    somaticAF α q s ≤ 1

Uses 3 · Used by 6

Statement usesExpected allelic fraction of a somatic mutation

Proof usesAverage absolute copy number of a tumor sample · Positivity of the mixture copy number

Used byThe continuous CCF MLE · Positivity of the grid posterior normalizer · The CCF posterior is stochastically increasing in the read count · Power decreases with local copy number · Power increases with multiplicity · Power increases with purity

TheoremSomatic allelic fraction increases with purity#✓fully proved

The somatic allelic fraction increases with the purity (0 ≤ s, 0 < q).

theorem somaticAF_mono_purity {α α' q s : ℝ} (hα0 : 0 ≤ α) (hαα' : α ≤ α') (hα1 : α' ≤ 1)
    (hq : 0 < q) (hs : 0 ≤ s) : somaticAF α q s ≤ somaticAF α' q s

Uses 3 · Used by 1

Statement usesExpected allelic fraction of a somatic mutation

Proof usesAverage absolute copy number of a tumor sample · Positivity of the mixture copy number

Used byPower increases with purity

TheoremSomatic allelic fraction decreases with copy number#✓fully proved

The somatic allelic fraction decreases with the local copy number (0 ≤ α ≤ 1, 0 ≤ s, 0 < q ≤ q').

theorem somaticAF_anti_copy {α q q' s : ℝ} (hα0 : 0 ≤ α) (hα1 : α ≤ 1) (hq : 0 < q)
    (hqq' : q ≤ q') (hs : 0 ≤ s) : somaticAF α q' s ≤ somaticAF α q s

Uses 3 · Used by 1

Statement usesExpected allelic fraction of a somatic mutation

Proof usesAverage absolute copy number of a tumor sample · Positivity of the mixture copy number

Used byPower decreases with local copy number

TheoremSomatic allelic fraction increases with multiplicity#✓fully proved

The somatic allelic fraction increases with the multiplicity (0 ≤ α ≤ 1, 0 < q).

theorem somaticAF_mono_mult {α q s s' : ℝ} (hα0 : 0 ≤ α) (hα1 : α ≤ 1) (hq : 0 < q)
    (hss' : s ≤ s') : somaticAF α q s ≤ somaticAF α q s'

Uses 3 · Used by 2

Statement usesExpected allelic fraction of a somatic mutation

Proof usesAverage absolute copy number of a tumor sample · Positivity of the mixture copy number

Used byThe CCF posterior is stochastically increasing in the read count · Power increases with multiplicity

26 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.