Skip to content

Molecular timing of copy-number gains

16 fully proved

Mutation Timing

StructureCopy-number gain history#✓fully proved

A single copy-number event on a region: copies original copies, of which copy i has desc i copies after the event (0 if lost, 2 if duplicated).

structure GainHistory where
  /-- The number of copies of the region before the event. -/
  copies : ℕ
  /-- The number of copies descending from each original copy after the event. -/
  desc : Fin copies → ℕ
Used by 15
Used byNumber of amplified copies · Copy-neutral loss of heterozygosity · Copy-neutral LOH · Expected number of mutations of a given multiplicity · Identifiability · Copy number after a copy-number event · Positive copy number after an amplifying event · The mutation rate from the spectrum · Single-copy gain · Single gain · Expected count of mutations on amplified copies · The multiplicity-weighted total is time-invariant · The timing closed form · Whole-genome doubling event · Whole-genome doubling

Gain History

DefinitionCopy number after a copy-number event#✓fully proved

The copy number c₁ = ∑ i, desc i after the event.

def finalCopies (h : GainHistory) : ℕ := ∑ i, h.desc i
Uses 1 · Used by 10
Statement usesCopy-number gain history
Used byCopy-neutral LOH · Expected number of mutations of a given multiplicity · Identifiability · Positive copy number after an amplifying event · The mutation rate from the spectrum · Single gain · Expected count of mutations on amplified copies · The multiplicity-weighted total is time-invariant · The timing closed form · Whole-genome doubling

DefinitionNumber of amplified copies#✓fully proved

The number of original copies amplified by the event (desc i ≥ 2).

def amplified (h : GainHistory) : ℕ := (univ.filter fun i => 2 ≤ h.desc i).card
Uses 1 · Used by 4
Statement usesCopy-number gain history
Used byIdentifiability · Positive copy number after an amplifying event · Expected count of mutations on amplified copies · The timing closed form

DefinitionExpected number of mutations of a given multiplicity#✓fully proved

Expected number of mutations of multiplicity m: μ t #{i | desc i = m} + [m = 1] μ c₁ (1 - t) (per-copy rate μ, event at time t of the normalized history [0, 1]).

noncomputable def expectedCount (h : GainHistory) (μ t : ℝ) (m : ℕ) : ℝ :=
  μ * t * ((univ.filter fun i => h.desc i = m).card : ℝ) +
    if m = 1 then μ * h.finalCopies * (1 - t) else 0
Uses 2 · Used by 8
Statement usesCopy-number gain history · Copy number after a copy-number event
Used byCopy-neutral LOH · Identifiability · The mutation rate from the spectrum · Single gain · Expected count of mutations on amplified copies · The multiplicity-weighted total is time-invariant · The timing closed form · Whole-genome doubling

TheoremThe multiplicity-weighted total is time-invariant#✓fully proved

∑_m m E_m = μ c₁, summing over all multiplicities up to a bound B ≥ max(1, max_i desc i).

theorem sum_mul_expectedCount (h : GainHistory) (μ t : ℝ) {B : ℕ} (hB : ∀ i, h.desc i ≤ B)
    (hB1 : 1 ≤ B) :
    ∑ m ∈ range (B + 1), (m : ℝ) * h.expectedCount μ t m = μ * h.finalCopies
Uses 3 · Used by 2
Statement usesCopy-number gain history · Expected number of mutations of a given multiplicity · Copy number after a copy-number event
Used byThe mutation rate from the spectrum · The timing closed form

TheoremExpected count of mutations on amplified copies#✓fully proved

The mutations of multiplicity at least two number μ t #{i | desc i ≥ 2} in expectation: they all arose before the event, on an amplified copy.

theorem sum_expectedCount_amplified (h : GainHistory) (μ t : ℝ) {B : ℕ}
    (hB : ∀ i, h.desc i ≤ B) :
    ∑ m ∈ Ico 2 (B + 1), h.expectedCount μ t m = μ * t * h.amplified
Uses 4 · Used by 1
Statement usesCopy-number gain history · Number of amplified copies · Expected number of mutations of a given multiplicity
Proof usesCopy number after a copy-number event
Used byThe timing closed form

TheoremPositive copy number after an amplifying event#✓fully proved

An event that amplifies some copy leaves a positive copy number.

theorem finalCopies_pos {h : GainHistory} (ha : 0 < h.amplified) : 0 < h.finalCopies
Uses 3 · Used by 2
Statement usesCopy-number gain history · Number of amplified copies · Copy number after a copy-number event
Used byIdentifiability · The timing closed form

TheoremThe mutation rate from the spectrum#✓fully proved

μ = ∑_m m E_m / c₁ (c₁ > 0).

theorem rate_eq (h : GainHistory) (μ t : ℝ) {B : ℕ} (hB : ∀ i, h.desc i ≤ B) (hB1 : 1 ≤ B)
    (hc : 0 < h.finalCopies) :
    μ = (∑ m ∈ range (B + 1), (m : ℝ) * h.expectedCount μ t m) / h.finalCopies
Uses 4 · Used by 1
Statement usesCopy-number gain history · Expected number of mutations of a given multiplicity · Copy number after a copy-number event
Proof usesThe multiplicity-weighted total is time-invariant
Used byIdentifiability

TheoremThe timing closed form#✓fully proved

When some copy is amplified and μ ≠ 0, t = c₁ ∑_{m ≥ 2} E_m / (#{i | desc i ≥ 2} ∑_m m E_m).

theorem timing_eq (h : GainHistory) {μ : ℝ} (t : ℝ) (hμ : μ ≠ 0) {B : ℕ}
    (hB : ∀ i, h.desc i ≤ B) (hB1 : 1 ≤ B) (ha : 0 < h.amplified) :
    t = h.finalCopies * (∑ m ∈ Ico 2 (B + 1), h.expectedCount μ t m) /
      (h.amplified * ∑ m ∈ range (B + 1), (m : ℝ) * h.expectedCount μ t m)
Uses 7 · Used by 1
Statement usesCopy-number gain history · Number of amplified copies · Expected number of mutations of a given multiplicity · Copy number after a copy-number event
Proof usesPositive copy number after an amplifying event · Expected count of mutations on amplified copies · The multiplicity-weighted total is time-invariant
Used byIdentifiability

TheoremIdentifiability#✓fully proved

If some copy is amplified, two parameter pairs (μ, t), (μ', t') with μ, μ' ≠ 0 and the same expected multiplicity spectrum are equal.

theorem expectedCount_injective (h : GainHistory) {μ μ' t t' : ℝ} (hμ : μ ≠ 0) (hμ' : μ' ≠ 0)
    (ha : 0 < h.amplified) (heq : h.expectedCount μ t = h.expectedCount μ' t') :
    μ = μ' ∧ t = t'
Uses 7
Statement usesCopy-number gain history · Number of amplified copies · Expected number of mutations of a given multiplicity
Proof usesCopy number after a copy-number event · Positive copy number after an amplifying event · The mutation rate from the spectrum · The timing closed form

DefinitionSingle-copy gain#✓fully proved

A single-copy gain 1 + 1 → 2 + 1: one copy duplicated, the other kept.

def singleGain : GainHistory := ⟨2, ![2, 1]⟩
Uses 1 · Used by 1
Statement usesCopy-number gain history
Used bySingle gain

DefinitionCopy-neutral loss of heterozygosity#✓fully proved

Copy-neutral loss of heterozygosity 1 + 1 → 2 + 0: one copy duplicated, the other lost.

def cnLOH : GainHistory := ⟨2, ![2, 0]⟩
Uses 1 · Used by 1
Statement usesCopy-number gain history
Used byCopy-neutral LOH

DefinitionWhole-genome doubling event#✓fully proved

Whole-genome doubling of a diploid region 1 + 1 → 2 + 2.

def wgd : GainHistory := ⟨2, ![2, 2]⟩
Uses 1 · Used by 1
Statement usesCopy-number gain history
Used byWhole-genome doubling

TheoremSingle gain#✓fully proved

Single gain (2 + 1): t = 3 E₂ / (E₁ + 2 E₂), for μ ≠ 0.

theorem singleGain_timing {μ : ℝ} (t : ℝ) (hμ : μ ≠ 0) :
    t = 3 * singleGain.expectedCount μ t 2 /
      (singleGain.expectedCount μ t 1 + 2 * singleGain.expectedCount μ t 2)
Uses 4
Statement usesExpected number of mutations of a given multiplicity · Single-copy gain
Proof usesCopy-number gain history · Copy number after a copy-number event

TheoremCopy-neutral LOH#✓fully proved

Copy-neutral LOH (2 + 0): t = 2 E₂ / (E₁ + 2 E₂), for μ ≠ 0.

theorem cnLOH_timing {μ : ℝ} (t : ℝ) (hμ : μ ≠ 0) :
    t = 2 * cnLOH.expectedCount μ t 2 /
      (cnLOH.expectedCount μ t 1 + 2 * cnLOH.expectedCount μ t 2)
Uses 4
Statement usesCopy-neutral loss of heterozygosity · Expected number of mutations of a given multiplicity
Proof usesCopy-number gain history · Copy number after a copy-number event

TheoremWhole-genome doubling#✓fully proved

Whole-genome doubling (2 + 2): t = 2 E₂ / (E₁ + 2 E₂), for μ ≠ 0.

theorem wgd_timing {μ : ℝ} (t : ℝ) (hμ : μ ≠ 0) :
    t = 2 * wgd.expectedCount μ t 2 /
      (wgd.expectedCount μ t 1 + 2 * wgd.expectedCount μ t 2)
Uses 4
Statement usesExpected number of mutations of a given multiplicity · Whole-genome doubling event
Proof usesCopy-number gain history · Copy number after a copy-number event

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.