Ranked labeled histories of coalescent trees

AbbreviationUnordered pairs of lineages#✓fully proved

The unordered pairs of lineages when there are k lineages labeled 0, …, k - 1.

abbrev LineagePair (k : ℕ) : Type := {s : Finset (Fin k) // s.card = 2}

Used by 36

Used byNo anomalous gene trees on the balanced four-species tree · Coalescence along one branch of the species tree · Only balanced gene trees can be anomalous on the caterpillar · Additivity of the exit law · Exit law of a constant continuation · Nonnegativity of the exit law · The multispecies coalescent · No anomalous unrooted quartets, balanced species tree · Probability of quartet split 02|13 on the balanced tree · Probability of quartet split 03|12 on the balanced tree · Probability of the gene tree ((A, B), (C, D)) on the caterpillar · Probability of the gene tree ((A, C), (B, D)) on the caterpillar · Probability of the gene tree ((A, D), (B, C)) on the caterpillar · The matching gene tree · No anomalous unrooted quartets, caterpillar species tree · Probability of quartet split 02|13 on the caterpillar tree · Probability of quartet split 03|12 on the caterpillar tree · Total gene-tree probability is one · Gene-tree probabilities are nonnegative · Additivity · Probability of the discordant three-species gene tree with cherry \(\{0, 2\}\) · Probability of the discordant three-species gene tree with cherry \(\{1, 2\}\) · Three-species concordance · Normalization · Expectation under random joining as an average over histories · Rational-valued expectation under random joining · Clade probability · Clade probability under random joining for at most five genes · Random-joining probability as a fraction of ranked histories · Number of pairs of lineages · Number of ranked labeled histories · Number of ranked labeled histories · Random joining · Each ranked labeled history has probability 2^{n-1} / (n! (n - 1)!) · Every ranked history is equally likely under random joining · Ranked labeled history

AbbreviationRanked labeled history#✓fully proved

A ranked labeled history of n labeled genes, encoded by its coalescence events: at step i < n - 1 there are n - i lineages and the step records the pair that merges (the merged lineage takes the smaller label; the others keep their relative order).

abbrev RankedHistory (n : ℕ) : Type := (i : Fin (n - 1)) → LineagePair (n - i)

Uses 1 · Used by 41

Statement usesUnordered pairs of lineages

Used byNo anomalous gene trees on the balanced four-species tree · Coalescence along one branch of the species tree · Only balanced gene trees can be anomalous on the caterpillar · Clusters formed along a ranked history · Additivity of the exit law · Exit law of a constant continuation · Nonnegativity of the exit law · The multispecies coalescent · No anomalous unrooted quartets, balanced species tree · Probability of quartet split 02|13 on the balanced tree · Probability of quartet split 03|12 on the balanced tree · Probability of the gene tree ((A, B), (C, D)) on the caterpillar · Probability of the gene tree ((A, C), (B, D)) on the caterpillar · Probability of the gene tree ((A, D), (B, C)) on the caterpillar · The matching gene tree · No anomalous unrooted quartets, caterpillar species tree · Probability of quartet split 02|13 on the caterpillar tree · Probability of quartet split 03|12 on the caterpillar tree · Total gene-tree probability is one · Gene-tree probabilities are nonnegative · Additivity · Probability of the discordant three-species gene tree with cherry \(\{0, 2\}\) · Probability of the discordant three-species gene tree with cherry \(\{1, 2\}\) · Three-species concordance · Normalization · Expectation under random joining as an average over histories · Rational-valued expectation under random joining · Clade of a ranked history · Lineages after the first coalescence events of a ranked history · Merging lineages from singletons gives the ancestral blocks · Clade probability · Clade probability under random joining for at most five genes · Random-joining probability as a fraction of ranked histories · Lineage blocks after the first coalescence events · Ancestral partitions along a history, indexed by lineage label · Number of ranked labeled histories · Number of ranked labeled histories · Ancestral partitions along a history as sets of blocks · Random joining · Each ranked labeled history has probability 2^{n-1} / (n! (n - 1)!) · Every ranked history is equally likely under random joining

TheoremNumber of pairs of lineages#✓fully proved

The number of pairs of k lineages is k.choose 2.

theorem card_lineagePair (k : ℕ) : Fintype.card (LineagePair k) = k.choose 2

Uses 1 · Used by 2

Statement usesUnordered pairs of lineages

Used byNumber of ranked labeled histories · Every ranked history is equally likely under random joining

14 fully proved

Ancestral partitions of a history

DefinitionMerging two lineage blocks#✓fully proved

Merge the lineages (blocks of sampled genes) at positions a < b of a list of blocks: the merged block replaces position a, and position b is removed.

def mergeBlocks {n : ℕ} (bs : List (Finset (Fin n))) (a b : ℕ) : List (Finset (Fin n)) :=
  (bs.set a (bs.getD a ∅ ∪ bs.getD b ∅)).eraseIdx b

Used by 3

Used byLineages after the first coalescence events of a ranked history · Clade probability · Lineage blocks after the first coalescence events

DefinitionLineage blocks after the first coalescence events#✓fully proved

The lineages (as blocks of sampled genes, indexed by lineage label) after the first t coalescence events of a history, starting from the singletons {0}, …, {n - 1}.

def blocksAfter {n : ℕ} (h : RankedHistory n) (t : ℕ) : List (Finset (Fin n)) :=
  ((List.finRange (n - 1)).take t).foldl
    (fun bs i =>
      let s : Finset ℕ := (h i).1.map Fin.valEmbedding
      mergeBlocks bs (s.min.getD 0) (s.max.getD 0))
    ((List.finRange n).map fun j => {j})

Uses 2 · Used by 3

Statement usesRanked labeled history · Merging two lineage blocks

Used byMerging lineages from singletons gives the ancestral blocks · Clade probability · Ancestral partitions along a history, indexed by lineage label

DefinitionAncestral partitions along a history, indexed by lineage label#✓fully proved

The ancestral partitions of the sample along a history, as lists of blocks indexed by lineage label; entry t (for t < n) is the partition after t coalescence events.

def blocksOf {n : ℕ} (h : RankedHistory n) : List (List (Finset (Fin n))) :=
  (List.range n).map (blocksAfter h)

Uses 2 · Used by 1

Statement usesRanked labeled history · Lineage blocks after the first coalescence events

Used byAncestral partitions along a history as sets of blocks

DefinitionAncestral partitions along a history as sets of blocks#✓fully proved

The ancestral partitions of the sample along a history, as sets of blocks (forgetting the lineage labels): the ranked labeled history in the sense of Edwards (1970).

def partitionsOf {n : ℕ} (h : RankedHistory n) : List (Finset (Finset (Fin n))) :=
  (blocksOf h).map List.toFinset

Uses 2 · Used by 2

Statement usesRanked labeled history · Ancestral partitions along a history, indexed by lineage label

Used byClade of a ranked history · Clade probability

Counting

TheoremProduct of pair counts times a power of two is \(n!(n-1)!\)#✓fully proved

∏_{k=2}^n C(k, 2) * 2^{n-1} = n! (n - 1)!.

theorem prod_choose_two_mul_two_pow (n : ℕ) :
    (∏ k ∈ Icc 2 n, k.choose 2) * 2 ^ (n - 1) = n.factorial * (n - 1).factorial

Used by 2

Used byNumber of ranked labeled histories · Each ranked labeled history has probability 2^{n-1} / (n! (n - 1)!)

TheoremReindexing the product of pair counts#✓fully proved

Reindexing: ∏_{i < n - 1} C(n - i, 2) = ∏_{k=2}^n C(k, 2).

theorem prod_fin_choose_two (n : ℕ) :
    ∏ i : Fin (n - 1), (n - (i : ℕ)).choose 2 = ∏ k ∈ Icc 2 n, k.choose 2

Used by 2

Used byNumber of ranked labeled histories · Every ranked history is equally likely under random joining

TheoremNumber of ranked labeled histories#✓fully proved

∏_{k=2}^n C(k, 2) (Edwards 1970).

theorem card_rankedHistory (n : ℕ) :
    Fintype.card (RankedHistory n) = ∏ k ∈ Icc 2 n, k.choose 2

Uses 4 · Used by 2

Statement usesUnordered pairs of lineages · Ranked labeled history

Proof usesNumber of pairs of lineages · Reindexing the product of pair counts

Used byClade probability · Number of ranked labeled histories

TheoremNumber of ranked labeled histories#✓fully proved

#histories * 2^{n-1} = n! (n - 1)!, i.e. there are n! (n - 1)! / 2^{n-1} ranked labeled histories of n labeled genes (Edwards 1970).

theorem card_rankedHistory_mul_two_pow (n : ℕ) :
    Fintype.card (RankedHistory n) * 2 ^ (n - 1) = n.factorial * (n - 1).factorial

Uses 4

Statement usesUnordered pairs of lineages · Ranked labeled history

Proof usesNumber of ranked labeled histories · Product of pair counts times a power of two is \(n!(n-1)!\)

Random joining

DefinitionRandom joining#✓fully proved

Random joining (Edwards 1970; Kingman 1982): the pair merging at each step is uniform among the current (n - i).choose 2 pairs and independent of the earlier steps. Kingman (1982) shows that this is the law of the tree topology of the coalescent.

noncomputable def randomJoining (n : ℕ) : Measure (RankedHistory n) :=
  Measure.pi fun i => ProbabilityTheory.uniformOn (Set.univ : Set (LineagePair (n - i)))

Uses 2 · Used by 31

Statement usesUnordered pairs of lineages · Ranked labeled history

Used byNo anomalous gene trees on the balanced four-species tree · Coalescence along one branch of the species tree · Only balanced gene trees can be anomalous on the caterpillar · Additivity of the exit law · Exit law of a constant continuation · Nonnegativity of the exit law · The multispecies coalescent · No anomalous unrooted quartets, balanced species tree · Probability of quartet split 02|13 on the balanced tree · Probability of quartet split 03|12 on the balanced tree · Probability of the gene tree ((A, B), (C, D)) on the caterpillar · Probability of the gene tree ((A, C), (B, D)) on the caterpillar · Probability of the gene tree ((A, D), (B, C)) on the caterpillar · The matching gene tree · No anomalous unrooted quartets, caterpillar species tree · Probability of quartet split 02|13 on the caterpillar tree · Probability of quartet split 03|12 on the caterpillar tree · Total gene-tree probability is one · Gene-tree probabilities are nonnegative · Additivity · Probability of the discordant three-species gene tree with cherry \(\{0, 2\}\) · Probability of the discordant three-species gene tree with cherry \(\{1, 2\}\) · Three-species concordance · Normalization · Expectation under random joining as an average over histories · Rational-valued expectation under random joining · Clade probability · Clade probability under random joining for at most five genes · Random-joining probability as a fraction of ranked histories · Each ranked labeled history has probability 2^{n-1} / (n! (n - 1)!) · Every ranked history is equally likely under random joining

TheoremEvery ranked history is equally likely under random joining#✓fully proved

Under random joining each history has probability ∏_{k=2}^n C(k, 2)⁻¹.

theorem randomJoining_singleton_eq_inv (n : ℕ) (h : RankedHistory n) :
    randomJoining n {h} = ((∏ k ∈ Icc 2 n, k.choose 2 : ℕ) : ENNReal)⁻¹

Uses 5 · Used by 2

Statement usesUnordered pairs of lineages · Ranked labeled history · Random joining

Proof usesNumber of pairs of lineages · Reindexing the product of pair counts

Used byExpectation under random joining as an average over histories · Each ranked labeled history has probability 2^{n-1} / (n! (n - 1)!)

TheoremEach ranked labeled history has probability 2^{n-1} / (n! (n - 1)!)#✓fully proved

Each ranked labeled history has probability 2^{n-1} / (n! (n - 1)!) under random joining (Edwards 1970; Tajima 1983).

theorem randomJoining_singleton (n : ℕ) (h : RankedHistory n) :
    randomJoining n {h} = 2 ^ (n - 1) / (n.factorial * (n - 1).factorial : ℕ)

Uses 5

Statement usesUnordered pairs of lineages · Ranked labeled history · Random joining

Proof usesProduct of pair counts times a power of two is \(n!(n-1)!\) · Every ranked history is equally likely under random joining

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.