Multispecies coalescent

76 fully proved

Species trees

InductiveRooted binary species tree with branch lengths#✓fully proved

A rooted binary species tree on the species Fin n with branch lengths: leaf i is species i, and node l r t is the ancestral species of the species below l and r, where t is the length, in coalescent units (2N generations), of the branch above the node, i.e. the time during which the ancestral population of l and r exists before it merges with a sister population. The length stored at the root node is not used: the root population lasts until all lineages have coalesced. Leaf branch lengths are not recorded, because one gene lineage is sampled per species and a single lineage cannot coalesce. A species tree on the species Fin n labels each species by exactly one leaf; the type does not enforce this, and the theorems below are about concrete trees with this property. The type accepts any real branch length; the probabilistic statements assume nonnegative lengths (NonnegLengths).

inductive SpeciesTree (n : ℕ) where
  /-- The species `i`. -/
  | leaf : Fin n → SpeciesTree n
  /-- The ancestor of `l` and `r`, with branch length `t` above it. -/
  | node : SpeciesTree n → SpeciesTree n → ℝ → SpeciesTree n

Used by 31

Used byBalanced four-species tree · No anomalous gene trees on the balanced four-species tree · Caterpillar four-species tree · Clusters of a species tree · Clusters of the caterpillar species tree · Clusters of the three-species tree · Law of the lineages leaving a species-tree branch · 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 at most one · Root branch length does not affect gene-tree probabilities · Gene-tree probabilities are nonnegative · Additivity · Normalization · Species tree with nonnegative branch lengths · Topology of a species tree · Species below a node of a species tree · Three-species tree ((0, 1), 2)

DefinitionSpecies tree with nonnegative branch lengths#✓fully proved

Every branch length of the species tree, including the unused one stored at the root, is nonnegative. On such trees geneTreeProb is a probability law; for a negative length it is only a signed weight.

def NonnegLengths : SpeciesTree n → Prop
  | leaf _ => True
  | node l r t => l.NonnegLengths ∧ r.NonnegLengths ∧ 0 ≤ t

Uses 1 · Used by 3

Statement usesRooted binary species tree with branch lengths

Used byNonnegativity of the exit law · Gene-tree probabilities are at most one · Gene-tree probabilities are nonnegative

DefinitionSpecies below a node of a species tree#✓fully proved

The species below a node.

def taxa : SpeciesTree n → Finset (Fin n)
  | leaf i => {i}
  | node l r _ => l.taxa ∪ r.taxa

Uses 1 · Used by 3

Statement usesRooted binary species tree with branch lengths

Used byClusters of a species tree · Clusters of the caterpillar species tree · Clusters of the three-species tree

DefinitionClusters of a species tree#✓fully proved

The clusters (clades) of a species tree: the sets of species below its vertices, including the singletons and the full set of species.

def clusters : SpeciesTree n → Finset (Finset (Fin n))
  | leaf i => {{i}}
  | node l r _ => insert (l.taxa ∪ r.taxa) (l.clusters ∪ r.clusters)

Uses 2 · Used by 6

Statement usesRooted binary species tree with branch lengths · Species below a node of a species tree

Used byAnomaly of ((A, C), (B, D)) and ((A, D), (B, C)) on the caterpillar · Anomalous gene tree on four species · The four-species anomaly zone · Clusters of the caterpillar species tree · Clusters of the three-species tree · No anomalous gene trees for three species

DefinitionTopology of a species tree#✓fully proved

The topology of a species tree, forgetting branch lengths, as a planar rooted binary tree.

def shape : SpeciesTree n → MathlibExt.Biology.Phylogenetics.TreeCount.PlaneTree (Fin n)
  | leaf i => .leaf i
  | node l r _ => .node l.shape r.shape

Uses 2

Statement usesPlanar rooted binary tree with labeled leaves · Rooted binary species tree with branch lengths

Tavaré's probabilities sum to one

TheoremTavaré's probabilities sum to one#✓fully proved

From m ≥ 1 lineages, the number of ancestors at time t is one of 1, …, m. (The rows of exp (t • G) restricted to the states ≥ 1 sum to one because G kills the indicator of {1, …, n}; an identity for every real t.)

theorem sum_tavareProb {m : ℕ} (hm : 1 ≤ m) (t : ℝ) :
    ∑ j ∈ Finset.Icc 1 m, tavareProb m j t = 1

Uses 3 · Used by 1

Statement usesTavaré's formula for the number of ancestral lineages

Proof usesGenerator of Kingman's block-counting process · Tavaré's formula

Used byExit law of a constant continuation

TheoremTavaré's probabilities are nonnegative#✓fully proved

Tavaré's probabilities are nonnegative for t ≥ 0: exp (t • G) is the entrywise limit of powers of the Wright–Fisher transition matrix (tendsto_wfLineageMatrix_pow_floor), whose entries are nonnegative. (For t < 0 they can be negative or exceed one.)

theorem tavareProb_nonneg {m j : ℕ} (hj : j ∈ Icc 1 m) {t : ℝ} (ht : 0 ≤ t) :
    0 ≤ tavareProb m j t

Uses 5 · Used by 3

Statement usesTavaré's formula for the number of ancestral lineages

Proof usesGenerator of Kingman's block-counting process · Tavaré's formula · Kingman's theorem for the lineage count · Wright–Fisher transition matrix of the lineage count

Used byNo anomalous gene trees on the balanced four-species tree · Only balanced gene trees can be anomalous on the caterpillar · Nonnegativity of the exit law

Coalescence inside one population

DefinitionLineages after the first coalescence events of a ranked history#✓fully proved

The lineages after the first t coalescence events of the ranked history h (of m lineages), starting from the lineages bs, each given as the set of sampled genes it is ancestral to. Events follow the encoding of RankedHistory: the pair {a, b} with a < b merges into position a, and position b is removed (mergeBlocks). With the singletons as starting lineages this is blocksAfter (mergeAlong_singletons).

def mergeAlong {m : ℕ} (bs : List (Finset (Fin n))) (h : RankedHistory m) (t : ℕ) :
    List (Finset (Fin n)) :=
  ((List.finRange (m - 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))
    bs

Uses 2 · Used by 22

Statement usesRanked labeled history · Merging two lineage blocks

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 · 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 · 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 · Merging lineages from singletons gives the ancestral blocks · Clade probability

TheoremMerging lineages from singletons gives the ancestral blocks#✓fully proved

Starting from the singletons, mergeAlong is blocksAfter.

theorem mergeAlong_singletons (h : RankedHistory n) (t : ℕ) :
    mergeAlong ((List.finRange n).map fun j => {j}) h t = blocksAfter h t

Uses 3

Statement usesRanked labeled history · Lineage blocks after the first coalescence events · Lineages after the first coalescence events of a ranked history

DefinitionClusters formed along a ranked history#✓fully proved

The clusters formed during the first t coalescence events of h from the lineages bs: every lineage present at some step u ≤ t, as the set of sampled genes it is ancestral to.

def cladesAlong {m : ℕ} (bs : List (Finset (Fin n))) (h : RankedHistory m) (t : ℕ) :
    Finset (Finset (Fin n)) :=
  (range (t + 1)).biUnion fun u => (mergeAlong bs h u).toFinset

Uses 2 · Used by 24

Statement usesRanked labeled history · Lineages after the first coalescence events of a ranked 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

The multispecies coalescent

DefinitionCoalescence along one branch of the species tree#✓fully proved

One population of the multispecies coalescent along a branch of length t. It receives m lineages bs (and the clusters acc formed below it). Under Kingman's coalescent the number j of lineages left at the top of the branch has law tavareProb m j t (Tavaré's formula, exp_blockCountingGenerator_apply), and, independently of the coalescence times, the order of the m - j coalescences is the beginning of a random-joining history of the m lineages (randomJoining). The continuation k receives the number of exiting lineages, the lineages, and the clusters formed so far.

def branchStep (t : ℝ) (m : ℕ) (bs : List (Finset (Fin n))) (acc : Finset (Finset (Fin n)))
    (k : ℕ → List (Finset (Fin n)) → Finset (Finset (Fin n)) → ℝ) : ℝ :=
  ∑ j ∈ Icc 1 m, tavareProb m j t *
    ∫ h, k j (mergeAlong bs h (m - j)) (acc ∪ cladesAlong bs h (m - j)) ∂randomJoining m

Uses 6 · Used by 11

Statement usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Clusters formed along a ranked history · Lineages after the first coalescence events of a ranked history

Used byLaw of the lineages leaving a species-tree branch · Additivity of the exit law · Exit law of a constant continuation · Nonnegativity of the exit law · 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

DefinitionLaw of the lineages leaving a species-tree branch#✓fully proved

The law of the lineages leaving the top of the branch above a vertex of the species tree, in continuation-passing form: exitLaw T k is the expectation of k m bs acc, where m is the number of exiting lineages, bs the lineages and acc the clusters formed below. The two daughter populations evolve independently, and their lineages enter the ancestral population together.

def exitLaw : SpeciesTree n → (ℕ → List (Finset (Fin n)) → Finset (Finset (Fin n)) → ℝ) → ℝ
  | leaf i, k => k 1 [{i}] {{i}}
  | node l r t, k => exitLaw l fun ml bl al => exitLaw r fun mr br ar =>
      branchStep t (ml + mr) (bl ++ br) (al ∪ ar) k

Uses 2 · Used by 19

Statement usesRooted binary species tree with branch lengths · Coalescence along one branch of the species tree

Used byNo anomalous gene trees on the balanced four-species tree · 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 · Normalization

DefinitionThe multispecies coalescent#✓fully proved

The multispecies coalescent (Pamilo & Nei 1988; Degnan & Salter 2005), one lineage sampled per species: the probability that the gene tree, given by its set of clusters, lies in the event E. Below the root, each branch population runs Kingman's coalescent for the branch length (branchStep); in the root population all remaining lineages coalesce by random joining. The definition accepts any real branch lengths; it is a probability law on species trees with nonnegative branch lengths (geneTreeProb_nonneg, geneTreeProb_or, geneTreeProb_true), and only a signed weight otherwise (with internal branch -1, the matching three-species gene tree gets 1 - (2/3) e < 0).

def geneTreeProb (T : SpeciesTree n) (E : Finset (Finset (Fin n)) → Prop) [DecidablePred E] :
    ℝ :=
  match T with
  | leaf i => if E {{i}} then 1 else 0
  | node l r _ => exitLaw l fun ml bl al => exitLaw r fun mr br ar =>
      ∫ h, (if E (al ∪ ar ∪ cladesAlong (bl ++ br) h (ml + mr - 1)) then 1 else 0)
        ∂randomJoining (ml + mr)

Uses 6 · Used by 26

Statement usesUnordered pairs of lineages · Ranked labeled history · Random joining · Rooted binary species tree with branch lengths · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch

Used byNo anomalous gene trees on the balanced four-species tree · Anomaly of ((A, C), (B, D)) and ((A, D), (B, C)) on the caterpillar · Anomalous gene tree on four species · The four-species anomaly zone · Only balanced gene trees can be anomalous on the caterpillar · 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 at most one · Root branch length does not affect gene-tree probabilities · 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 · The species quartet maximizes quartet support · No anomalous gene trees for three species

TheoremRoot branch length does not affect gene-tree probabilities#✓fully proved

The branch length stored at the root of a species tree does not affect the gene tree.

theorem geneTreeProb_node_length (l r : SpeciesTree n) (t t' : ℝ)
    (E : Finset (Finset (Fin n)) → Prop) [DecidablePred E] :
    geneTreeProb (.node l r t) E = geneTreeProb (.node l r t') E

Uses 2

Statement usesRooted binary species tree with branch lengths · The multispecies coalescent

TheoremExit law of a constant continuation#✓fully proved

If a continuation takes the constant value c whenever at least one lineage exits, then so does exitLaw (Tavaré's probabilities sum to one and random joining is a probability).

theorem exitLaw_eq_const (T : SpeciesTree n) (c : ℝ)
    (k : ℕ → List (Finset (Fin n)) → Finset (Finset (Fin n)) → ℝ)
    (hk : ∀ m bs acc, 1 ≤ m → k m bs acc = c) : exitLaw T k = c

Uses 10 · Used by 2

Statement usesRooted binary species tree with branch lengths · Law of the lineages leaving a species-tree branch

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Coalescence along one branch of the species tree · Clusters formed along a ranked history · Lineages after the first coalescence events of a ranked history · Tavaré's probabilities sum to one

Used byTotal gene-tree probability is one · Normalization

TheoremNormalization#✓fully proved

For every species tree, the event "any gene tree" has weight one (an identity for every real branch length). With geneTreeProb_nonneg and geneTreeProb_or this makes geneTreeProb T a probability law when T.NonnegLengths.

theorem geneTreeProb_true (T : SpeciesTree n) : geneTreeProb T (fun _ => True) = 1

Uses 8

Statement usesRooted binary species tree with branch lengths · The multispecies coalescent

Proof usesUnordered pairs of lineages · Ranked labeled history · Random joining · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch · Exit law of a constant continuation

TheoremTotal gene-tree probability is one#✓fully proved

An event containing every gene tree has weight one, for every species tree.

theorem geneTreeProb_eq_one (T : SpeciesTree n) (E : Finset (Finset (Fin n)) → Prop)
    [DecidablePred E] (hE : ∀ G, E G) : geneTreeProb T E = 1

Uses 8 · Used by 1

Statement usesRooted binary species tree with branch lengths · The multispecies coalescent

Proof usesUnordered pairs of lineages · Ranked labeled history · Random joining · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch · Exit law of a constant continuation

Used byGene-tree probabilities are at most one

TheoremNonnegativity of the exit law#✓fully proved

On a species tree with nonnegative branch lengths, exitLaw of a continuation that is nonnegative whenever at least one lineage exits is nonnegative (Tavaré's probabilities are nonnegative, tavareProb_nonneg).

theorem exitLaw_nonneg : ∀ (T : SpeciesTree n), T.NonnegLengths →
    ∀ k : ℕ → List (Finset (Fin n)) → Finset (Finset (Fin n)) → ℝ,
      (∀ m bs acc, 1 ≤ m → 0 ≤ k m bs acc) → 0 ≤ exitLaw T k

Uses 11 · Used by 1

Statement usesRooted binary species tree with branch lengths · Species tree with nonnegative branch lengths · Law of the lineages leaving a species-tree branch

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Coalescence along one branch of the species tree · Clusters formed along a ranked history · Lineages after the first coalescence events of a ranked history · Tavaré's probabilities are nonnegative

Used byGene-tree probabilities are nonnegative

TheoremGene-tree probabilities are nonnegative#✓fully proved

Gene-tree probabilities are nonnegative on species trees with nonnegative branch lengths. (For a negative branch length they need not be.)

theorem geneTreeProb_nonneg {T : SpeciesTree n} (hT : T.NonnegLengths)
    (E : Finset (Finset (Fin n)) → Prop) [DecidablePred E] : 0 ≤ geneTreeProb T E

Uses 9 · Used by 1

Statement usesRooted binary species tree with branch lengths · Species tree with nonnegative branch lengths · The multispecies coalescent

Proof usesUnordered pairs of lineages · Ranked labeled history · Random joining · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch · Nonnegativity of the exit law

Used byGene-tree probabilities are at most one

Evaluating random-joining expectations

TheoremExpectation under random joining as an average over histories#✓fully proved

An expectation under random joining is the average over the ∏_{k=2}^m C(k, 2) ranked histories.

theorem integral_randomJoining (m : ℕ) (f : RankedHistory m → ℝ) :
    ∫ h, f h ∂randomJoining m = (∑ h, f h) / ∏ k ∈ Icc 2 m, ((k.choose 2 : ℕ) : ℝ)

Uses 4 · Used by 4

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

Proof usesEvery ranked history is equally likely under random joining

Used byNo anomalous gene trees on the balanced four-species tree · Only balanced gene trees can be anomalous on the caterpillar · Rational-valued expectation under random joining · Random-joining probability as a fraction of ranked histories

TheoremRational-valued expectation under random joining#✓fully proved

integral_randomJoining for a rational-valued function, with a rational result (used to evaluate random-joining probabilities by computation).

theorem integral_randomJoining_ratCast (m : ℕ) (q : RankedHistory m → ℚ) :
    ∫ h, (q h : ℝ) ∂randomJoining m =
      (((∑ h, q h) / ∏ k ∈ Icc 2 m, ((k.choose 2 : ℕ) : ℚ) : ℚ) : ℝ)

Uses 4 · Used by 13

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

Proof usesExpectation under random joining as an average over histories

Used byNo 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 · 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

TheoremRandom-joining probability as a fraction of ranked histories#✓fully proved

The probability of an event under random joining is the fraction of ranked histories in it.

theorem randomJoining_real (m : ℕ) (A : Set (RankedHistory m)) [DecidablePred (· ∈ A)] :
    (randomJoining m).real A = (#{h | h ∈ A} : ℝ) / ∏ k ∈ Icc 2 m, ((k.choose 2 : ℕ) : ℝ)

Uses 4 · Used by 1

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

Proof usesExpectation under random joining as an average over histories

Used byClade probability

TheoremAdditivity of the exit law#✓fully proved

exitLaw is additive in the continuation.

theorem exitLaw_add (T : SpeciesTree n)
    (k₁ k₂ : ℕ → List (Finset (Fin n)) → Finset (Finset (Fin n)) → ℝ) :
    exitLaw T (fun m bs acc => k₁ m bs acc + k₂ m bs acc) = exitLaw T k₁ + exitLaw T k₂

Uses 9 · Used by 1

Statement usesRooted binary species tree with branch lengths · Law of the lineages leaving a species-tree branch

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Coalescence along one branch of the species tree · Clusters formed along a ranked history · Lineages after the first coalescence events of a ranked history

Used byAdditivity

TheoremAdditivity#✓fully proved

The probabilities of two disjoint events of gene trees add up. With geneTreeProb_nonneg and geneTreeProb_true, geneTreeProb T is a probability law when T.NonnegLengths.

theorem geneTreeProb_or (T : SpeciesTree n) (E F : Finset (Finset (Fin n)) → Prop)
    [DecidablePred E] [DecidablePred F] (hEF : ∀ G, E G → ¬ F G) :
    geneTreeProb T (fun G => E G ∨ F G) = geneTreeProb T E + geneTreeProb T F

Uses 8 · Used by 1

Statement usesRooted binary species tree with branch lengths · The multispecies coalescent

Proof usesUnordered pairs of lineages · Ranked labeled history · Random joining · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch · Additivity of the exit law

Used byGene-tree probabilities are at most one

TheoremGene-tree probabilities are at most one#✓fully proved

On a species tree with nonnegative branch lengths, every gene-tree probability is at most one.

theorem geneTreeProb_le_one {T : SpeciesTree n} (hT : T.NonnegLengths)
    (E : Finset (Finset (Fin n)) → Prop) [DecidablePred E] : geneTreeProb T E ≤ 1

Uses 6

Statement usesRooted binary species tree with branch lengths · Species tree with nonnegative branch lengths · The multispecies coalescent

Proof usesTotal gene-tree probability is one · Gene-tree probabilities are nonnegative · Additivity

Tavaré's formula for two and three lineages

TheoremTwo lineages remain distinct with probability \(e^{-t}\)#✓fully proved

Two lineages are still distinct after time t with probability e^{-t}.

theorem tavareProb_two_two (t : ℝ) : tavareProb 2 2 t = Real.exp (-t)

Uses 1 · Used by 14

Statement usesTavaré's formula for the number of ancestral lineages

Used byNo 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 · 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 · Wright–Fisher limit of the no-coalescence probability

TheoremTwo lineages coalesce with probability \(1 - e^{-t}\)#✓fully proved

Two lineages have coalesced within time t with probability 1 - e^{-t}.

theorem tavareProb_two_one (t : ℝ) : tavareProb 2 1 t = 1 - Real.exp (-t)

Uses 1 · Used by 9

Statement usesTavaré's formula for the number of ancestral lineages

Used byNo anomalous unrooted quartets, balanced species 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 · Three-species concordance

TheoremThree lineages remain distinct with probability \(e^{-3t}\)#✓fully proved

Three lineages are still distinct after time t with probability e^{-3t}.

theorem tavareProb_three_three (t : ℝ) : tavareProb 3 3 t = Real.exp (-(3 * t))

Uses 1 · Used by 7

Statement usesTavaré's formula for the number of ancestral lineages

Used byProbability 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

TheoremThree lineages have two ancestors at time \(t\)#✓fully proved

Three lineages have two ancestors at time t with probability (3/2)(e^{-t} - e^{-3t}).

theorem tavareProb_three_two (t : ℝ) :
    tavareProb 3 2 t = 3 / 2 * (Real.exp (-t) - Real.exp (-(3 * t)))

Uses 1 · Used by 7

Statement usesTavaré's formula for the number of ancestral lineages

Used byProbability 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

TheoremThree lineages have one ancestor at time \(t\)#✓fully proved

Three lineages have one ancestor at time t with probability 1 - (3/2) e^{-t} + (1/2) e^{-3t}.

theorem tavareProb_three_one (t : ℝ) :
    tavareProb 3 1 t = 1 - 3 / 2 * Real.exp (-t) + 1 / 2 * Real.exp (-(3 * t))

Uses 1 · Used by 7

Statement usesTavaré's formula for the number of ancestral lineages

Used byProbability 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

Three species

DefinitionThree-species tree ((0, 1), 2)#✓fully proved

The three-species tree ((0, 1), 2) with internal branch length t.

def triple (t : ℝ) : SpeciesTree 3 := .node (.node (.leaf 0) (.leaf 1) t) (.leaf 2) 0

Uses 1 · Used by 5

Statement usesRooted binary species tree with branch lengths

Used byClusters of the three-species tree · 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 · No anomalous gene trees for three species

DefinitionThree-gene tree with a given cherry#✓fully proved

The gene tree on three genes with cherry c (a pair of genes), as a set of clusters.

def tripleTree (c : Finset (Fin 3)) : Finset (Finset (Fin 3)) := {{0}, {1}, {2}, c, univ}

Used by 5

Used byClusters of the three-species tree · 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 · No anomalous gene trees for three species

TheoremClusters of the three-species tree#✓fully proved

The species tree ((0, 1), 2) has the clusters of the gene tree with cherry {0, 1}.

theorem clusters_triple (t : ℝ) : (triple t).clusters = tripleTree {0, 1}

Uses 5 · Used by 1

Statement usesClusters of a species tree · Three-species tree ((0, 1), 2) · Three-gene tree with a given cherry

Proof usesRooted binary species tree with branch lengths · Species below a node of a species tree

Used byNo anomalous gene trees for three species

TheoremThree-species concordance#✓fully proved

Three-species concordance (Hudson 1983; Pamilo & Nei 1988): with one lineage per species and internal branch length t, the gene tree matches the species tree with probability 1 - (2/3) e^{-t}. (An identity for every real t; branch lengths are t ≥ 0.)

theorem geneTreeProb_triple_matching (t : ℝ) :
    geneTreeProb (triple t) (· = tripleTree {0, 1}) = 1 - 2 / 3 * Real.exp (-t)

Uses 12 · Used by 1

Statement usesThe multispecies coalescent · Three-species tree ((0, 1), 2) · Three-gene tree with a given cherry

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Clusters formed along a ranked history · Rational-valued expectation under random joining · Lineages after the first coalescence events of a ranked history · Two lineages coalesce with probability \(1 - e^{-t}\) · Two lineages remain distinct with probability \(e^{-t}\)

Used byNo anomalous gene trees for three species

TheoremProbability of the discordant three-species gene tree with cherry \(\{0, 2\}\)#✓fully proved

With one lineage per species and internal branch length \(t\), the gene tree of the species tree \(((0, 1), 2)\) whose cherry is \(\{0, 2\}\) has probability \(\frac{1}{3} e^{-t}\). (An identity for every real \(t\); branch lengths are \(t \ge 0\).)

theorem geneTreeProb_triple_cherry_02 (t : ℝ) :
    geneTreeProb (triple t) (· = tripleTree {0, 2}) = 1 / 3 * Real.exp (-t)

Uses 11 · Used by 1

Statement usesThe multispecies coalescent · Three-species tree ((0, 1), 2) · Three-gene tree with a given cherry

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Clusters formed along a ranked history · Rational-valued expectation under random joining · Lineages after the first coalescence events of a ranked history · Two lineages remain distinct with probability \(e^{-t}\)

Used byNo anomalous gene trees for three species

TheoremProbability of the discordant three-species gene tree with cherry \(\{1, 2\}\)#✓fully proved

With one lineage per species and internal branch length \(t\), the gene tree of the species tree \(((0, 1), 2)\) whose cherry is \(\{1, 2\}\) has probability \(\frac{1}{3} e^{-t}\). (An identity for every real \(t\); branch lengths are \(t \ge 0\).)

theorem geneTreeProb_triple_cherry_12 (t : ℝ) :
    geneTreeProb (triple t) (· = tripleTree {1, 2}) = 1 / 3 * Real.exp (-t)

Uses 11 · Used by 1

Statement usesThe multispecies coalescent · Three-species tree ((0, 1), 2) · Three-gene tree with a given cherry

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Clusters formed along a ranked history · Rational-valued expectation under random joining · Lineages after the first coalescence events of a ranked history · Two lineages remain distinct with probability \(e^{-t}\)

Used byNo anomalous gene trees for three species

TheoremNo anomalous gene trees for three species#✓fully proved

No anomalous gene trees for three species (Degnan & Rosenberg 2006): for a positive internal branch, each discordant gene tree is strictly less probable than the matching one.

theorem triple_no_anomaly {t : ℝ} (ht : 0 < t) :
    geneTreeProb (triple t) (· = tripleTree {0, 2}) <
        geneTreeProb (triple t) (· = (triple t).clusters) ∧
      geneTreeProb (triple t) (· = tripleTree {1, 2}) <
        geneTreeProb (triple t) (· = (triple t).clusters)

Uses 8

Statement usesClusters of a species tree · The multispecies coalescent · Three-species tree ((0, 1), 2) · Three-gene tree with a given cherry

Proof usesClusters of the three-species tree · 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

TheoremWright–Fisher limit of the no-coalescence probability#✓fully proved

The three-species probabilities come from the Wright–Fisher model: in a population of M gene copies, the lineages of species 0 and 1 have distinct parents in each of the ⌊t M⌋ generations of the internal branch (t ≥ 0 coalescent units) with probability noCoalProb M 2 ^ ⌊t M⌋, which tends to tavareProb 2 2 t = e^{-t}, the weight of the case in which three lineages reach the root population.

theorem tendsto_noCoalProb_pow_floor_two {t : ℝ} (ht : 0 ≤ t) :
    Tendsto (fun M : ℕ => noCoalProb M 2 ^ ⌊t * M⌋₊) atTop (𝓝 (tavareProb 2 2 t))

Uses 4

Statement usesTavaré's formula for the number of ancestral lineages · Probability of no coalescence in one Wright–Fisher generation

Proof usesWright–Fisher coalescence times converge to exponential laws · Two lineages remain distinct with probability \(e^{-t}\)

Four species: the anomaly zone

DefinitionCaterpillar four-species tree#✓fully proved

The asymmetric (caterpillar) species tree (((0, 1), 2), 3): x is the length of the deeper internal branch (above the ancestor of 0, 1, 2) and y that of the shallower one (above the ancestor of 0, 1), as in Degnan & Rosenberg (2006).

def caterpillar (x y : ℝ) : SpeciesTree 4 :=
  .node (.node (.node (.leaf 0) (.leaf 1) y) (.leaf 2) x) (.leaf 3) 0

Uses 1 · Used by 13

Statement usesRooted binary species tree with branch lengths

Used byAnomaly of ((A, C), (B, D)) and ((A, D), (B, C)) on the caterpillar · Anomalous gene tree on four species · The four-species anomaly zone · Only balanced gene trees can be anomalous on the caterpillar · Clusters of the caterpillar species 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 · The species quartet maximizes quartet support

DefinitionBalanced four-species tree#✓fully proved

The symmetric (balanced) species tree ((0, 1), (2, 3)) with internal branch lengths y₁ (above the ancestor of 0, 1) and y₂ (above the ancestor of 2, 3).

def balanced (y₁ y₂ : ℝ) : SpeciesTree 4 :=
  .node (.node (.leaf 0) (.leaf 1) y₁) (.node (.leaf 2) (.leaf 3) y₂) 0

Uses 1 · Used by 5

Statement usesRooted binary species tree with branch lengths

Used byNo anomalous gene trees on the balanced four-species tree · 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 · The species quartet maximizes quartet support

DefinitionCaterpillar four-gene tree#✓fully proved

The asymmetric gene tree (((a, b), c), d) on four genes, as a set of clusters.

def caterpillarTree (a b c d : Fin 4) : Finset (Finset (Fin 4)) :=
  {{a}, {b}, {c}, {d}, {a, b}, {a, b, c}, univ}

Used by 6

Used byAnomaly of ((A, C), (B, D)) and ((A, D), (B, C)) on the caterpillar · Anomalous gene tree on four species · The four-species anomaly zone · Only balanced gene trees can be anomalous on the caterpillar · Clusters of the caterpillar species tree · The matching gene tree

DefinitionBalanced four-gene tree#✓fully proved

The symmetric gene tree ((a, b), (c, d)) on four genes, as a set of clusters.

def balancedTree (a b c d : Fin 4) : Finset (Finset (Fin 4)) :=
  {{a}, {b}, {c}, {d}, {a, b}, {c, d}, univ}

Used by 9

Used byNo anomalous gene trees on the balanced four-species tree · Anomaly of ((A, C), (B, D)) and ((A, D), (B, C)) on the caterpillar · Anomalous gene tree on four species · The four-species anomaly zone · Only balanced gene trees can be anomalous on the caterpillar · 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 · Balanced gene tree on four genes

TheoremClusters of the caterpillar species tree#✓fully proved

The species tree (((0, 1), 2), 3) has the clusters of the gene tree (((0, 1), 2), 3).

theorem clusters_caterpillar (x y : ℝ) : (caterpillar x y).clusters = caterpillarTree 0 1 2 3

Uses 5 · Used by 3

Statement usesClusters of a species tree · Caterpillar four-species tree · Caterpillar four-gene tree

Proof usesRooted binary species tree with branch lengths · Species below a node of a species tree

Used byAnomaly of ((A, C), (B, D)) and ((A, D), (B, C)) on the caterpillar · Anomalous gene tree on four species · The four-species anomaly zone

DefinitionDegnan–Rosenberg probability of the matching caterpillar gene tree#✓fully proved

Degnan & Rosenberg (2006), eq. (1): f(x, y), the probability of the matching gene tree (((A, B), C), D) on the caterpillar species tree.

def drF (x y : ℝ) : ℝ :=
  1 - 2 / 3 * Real.exp (-x) - 2 / 3 * Real.exp (-y) + 1 / 3 * Real.exp (-(x + y)) +
    1 / 18 * Real.exp (-(3 * x + y))

Used by 5

Used byAnomaly of ((A, C), (B, D)) and ((A, D), (B, C)) on the caterpillar · Anomalous gene tree on four species · Degnan–Rosenberg criterion: \(f(x, y) < g(x, y)\) iff \(y < b(x)\) · The boundary a(x) of the anomaly zone · The matching gene tree

DefinitionDegnan–Rosenberg formula g for the gene tree ((A, C), (B, D))#✓fully proved

Degnan & Rosenberg (2006), eq. (2): g(x, y), the probability of the gene tree ((A, C), (B, D)) (and of ((A, D), (B, C))) on the caterpillar species tree.

def drG (x y : ℝ) : ℝ := 1 / 6 * Real.exp (-(x + y)) - 1 / 18 * Real.exp (-(3 * x + y))

Used by 7

Used byAnomaly of ((A, C), (B, D)) and ((A, D), (B, C)) on the caterpillar · The four-species anomaly zone · Degnan–Rosenberg criterion: \(f(x, y) < g(x, y)\) iff \(y < b(x)\) · \(g(x, y) \le h(x, y)\) for a nonnegative shallower branch · \(g(x, y) < h(x, y)\) for a positive shallower branch · Probability of the gene tree ((A, C), (B, D)) on the caterpillar · Probability of the gene tree ((A, D), (B, C)) on the caterpillar

DefinitionDegnan–Rosenberg formula h for the gene tree ((A, B), (C, D))#✓fully proved

Degnan & Rosenberg (2006), eq. (3): h(x, y), the probability of the gene tree ((A, B), (C, D)) on the caterpillar species tree.

def drH (x y : ℝ) : ℝ :=
  1 / 3 * Real.exp (-x) - 1 / 6 * Real.exp (-(x + y)) - 1 / 18 * Real.exp (-(3 * x + y))

Used by 6

Used byAnomalous gene tree on four species · The four-species anomaly zone · The boundary a(x) of the anomaly zone · \(g(x, y) \le h(x, y)\) for a nonnegative shallower branch · \(g(x, y) < h(x, y)\) for a positive shallower branch · Probability of the gene tree ((A, B), (C, D)) on the caterpillar

TheoremThe matching gene tree#✓fully proved

The matching gene tree on the caterpillar species tree has probability f(x, y) (Degnan & Rosenberg 2006, eq. (1)). An identity for all real x, y.

theorem geneTreeProb_caterpillar_matching (x y : ℝ) :
    geneTreeProb (caterpillar x y) (· = caterpillarTree 0 1 2 3) = drF x y

Uses 19 · Used by 2

Statement usesCaterpillar four-species tree · Caterpillar four-gene tree · Degnan–Rosenberg probability of the matching caterpillar gene tree · The multispecies coalescent

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Rooted binary species tree with branch lengths · Coalescence along one branch of the species tree · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch · Rational-valued expectation under random joining · Lineages after the first coalescence events of a ranked history · Three lineages have one ancestor at time \(t\) · Three lineages remain distinct with probability \(e^{-3t}\) · Three lineages have two ancestors at time \(t\) · Two lineages coalesce with probability \(1 - e^{-t}\) · Two lineages remain distinct with probability \(e^{-t}\)

Used byAnomaly of ((A, C), (B, D)) and ((A, D), (B, C)) on the caterpillar · Anomalous gene tree on four species

TheoremProbability of the gene tree ((A, C), (B, D)) on the caterpillar#✓fully proved

The symmetric gene tree ((A, C), (B, D)) on the caterpillar species tree has probability g(x, y) (Degnan & Rosenberg 2006, eq. (2)).

theorem geneTreeProb_caterpillar_AC_BD (x y : ℝ) :
    geneTreeProb (caterpillar x y) (· = balancedTree 0 2 1 3) = drG x y

Uses 19 · Used by 2

Statement usesBalanced four-gene tree · Caterpillar four-species tree · Degnan–Rosenberg formula g for the gene tree ((A, C), (B, D)) · The multispecies coalescent

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Rooted binary species tree with branch lengths · Coalescence along one branch of the species tree · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch · Rational-valued expectation under random joining · Lineages after the first coalescence events of a ranked history · Three lineages have one ancestor at time \(t\) · Three lineages remain distinct with probability \(e^{-3t}\) · Three lineages have two ancestors at time \(t\) · Two lineages coalesce with probability \(1 - e^{-t}\) · Two lineages remain distinct with probability \(e^{-t}\)

Used byAnomaly of ((A, C), (B, D)) and ((A, D), (B, C)) on the caterpillar · The four-species anomaly zone

TheoremProbability of the gene tree ((A, D), (B, C)) on the caterpillar#✓fully proved

The symmetric gene tree ((A, D), (B, C)) on the caterpillar species tree has probability g(x, y), the same as ((A, C), (B, D)) (Degnan & Rosenberg 2006).

theorem geneTreeProb_caterpillar_AD_BC (x y : ℝ) :
    geneTreeProb (caterpillar x y) (· = balancedTree 0 3 1 2) = drG x y

Uses 19 · Used by 1

Statement usesBalanced four-gene tree · Caterpillar four-species tree · Degnan–Rosenberg formula g for the gene tree ((A, C), (B, D)) · The multispecies coalescent

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Rooted binary species tree with branch lengths · Coalescence along one branch of the species tree · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch · Rational-valued expectation under random joining · Lineages after the first coalescence events of a ranked history · Three lineages have one ancestor at time \(t\) · Three lineages remain distinct with probability \(e^{-3t}\) · Three lineages have two ancestors at time \(t\) · Two lineages coalesce with probability \(1 - e^{-t}\) · Two lineages remain distinct with probability \(e^{-t}\)

Used byThe four-species anomaly zone

TheoremProbability of the gene tree ((A, B), (C, D)) on the caterpillar#✓fully proved

The symmetric gene tree ((A, B), (C, D)) on the caterpillar species tree has probability h(x, y) (Degnan & Rosenberg 2006, eq. (3)).

theorem geneTreeProb_caterpillar_AB_CD (x y : ℝ) :
    geneTreeProb (caterpillar x y) (· = balancedTree 0 1 2 3) = drH x y

Uses 19 · Used by 2

Statement usesBalanced four-gene tree · Caterpillar four-species tree · Degnan–Rosenberg formula h for the gene tree ((A, B), (C, D)) · The multispecies coalescent

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Rooted binary species tree with branch lengths · Coalescence along one branch of the species tree · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch · Rational-valued expectation under random joining · Lineages after the first coalescence events of a ranked history · Three lineages have one ancestor at time \(t\) · Three lineages remain distinct with probability \(e^{-3t}\) · Three lineages have two ancestors at time \(t\) · Two lineages coalesce with probability \(1 - e^{-t}\) · Two lineages remain distinct with probability \(e^{-t}\)

Used byAnomalous gene tree on four species · The four-species anomaly zone

DefinitionBoundary of the four-species anomaly zone#✓fully proved

Degnan & Rosenberg (2006), eq. (4): the boundary a(x) of the four-species anomaly zone, for a deeper internal branch of length x > 0 (at x = 0 the denominator vanishes and Lean's a / 0 = 0 gives the junk value log (2/3 - 0); a(x) → ∞ as x → 0⁺).

def anomalyA (x : ℝ) : ℝ :=
  Real.log (2 / 3 + (3 * Real.exp (2 * x) - 2) / (18 * (Real.exp (3 * x) - Real.exp (2 * x))))

Used by 4

Used byAnomalous gene tree on four species · The four-species anomaly zone · The boundary a(x) of the anomaly zone · Anomaly-zone boundary blows up for short deep branches

DefinitionBoundary for three anomalous gene trees#✓fully proved

Degnan & Rosenberg (2006), eq. (5): the boundary b(x) below which the caterpillar species tree has three anomalous gene trees (defined for x ≥ 0).

def anomalyB (x : ℝ) : ℝ :=
  Real.log (2 / 3 + (5 * Real.exp (2 * x) - 2) / (6 * (3 * Real.exp (3 * x) -
    2 * Real.exp (2 * x))))

Used by 4

Used byThree-anomaly boundary is maximal at zero · Value \(\log(7/6)\) of the three-anomaly boundary at zero · Anomaly of ((A, C), (B, D)) and ((A, D), (B, C)) on the caterpillar · Degnan–Rosenberg criterion: \(f(x, y) < g(x, y)\) iff \(y < b(x)\)

Theorem\(g(x, y) < h(x, y)\) for a positive shallower branch#✓fully proved

For a positive shallower branch, the symmetric gene tree ((A, B), (C, D)) is strictly more probable than ((A, C), (B, D)): g(x, y) < h(x, y) (Degnan & Rosenberg 2006).

theorem drG_lt_drH (x : ℝ) {y : ℝ} (hy : 0 < y) : drG x y < drH x y

Uses 2

Statement usesDegnan–Rosenberg formula g for the gene tree ((A, C), (B, D)) · Degnan–Rosenberg formula h for the gene tree ((A, B), (C, D))

TheoremThe boundary a(x) of the anomaly zone#✓fully proved

The boundary a(x) of the anomaly zone (Degnan & Rosenberg 2006): for a deeper internal branch x > 0, the symmetric gene tree ((A, B), (C, D)) is more probable than the matching gene tree, f(x, y) < h(x, y), if and only if y < a(x).

theorem drF_lt_drH_iff {x : ℝ} (hx : 0 < x) (y : ℝ) : drF x y < drH x y ↔ y < anomalyA x

Uses 3 · Used by 1

Statement usesBoundary of the four-species anomaly zone · Degnan–Rosenberg probability of the matching caterpillar gene tree · Degnan–Rosenberg formula h for the gene tree ((A, B), (C, D))

Used byAnomalous gene tree on four species

TheoremDegnan–Rosenberg criterion: \(f(x, y) < g(x, y)\) iff \(y < b(x)\)#✓fully proved

Degnan & Rosenberg (2006): for x ≥ 0, the gene tree ((A, C), (B, D)) (equivalently ((A, D), (B, C))) is more probable than the matching gene tree, f(x, y) < g(x, y), if and only if y < b(x).

theorem drF_lt_drG_iff {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : drF x y < drG x y ↔ y < anomalyB x

Uses 3 · Used by 1

Statement usesBoundary for three anomalous gene trees · Degnan–Rosenberg probability of the matching caterpillar gene tree · Degnan–Rosenberg formula g for the gene tree ((A, C), (B, D))

Used byAnomaly of ((A, C), (B, D)) and ((A, D), (B, C)) on the caterpillar

TheoremValue \(\log(7/6)\) of the three-anomaly boundary at zero#✓fully proved

b(0) = log (7/6) (Degnan & Rosenberg 2006): if y ≥ log (7/6), then y ≥ b(x) for every x ≥ 0 (anomalyB_le_anomalyB_zero).

theorem anomalyB_zero : anomalyB 0 = Real.log (7 / 6)

Uses 1 · Used by 1

Statement usesBoundary for three anomalous gene trees

Used byThree-anomaly boundary is maximal at zero

TheoremThree-anomaly boundary is maximal at zero#✓fully proved

b is maximal at 0: b(x) ≤ log (7/6) for x ≥ 0, so for y ≥ log (7/6) at most one gene tree is anomalous.

theorem anomalyB_le_anomalyB_zero {x : ℝ} (hx : 0 ≤ x) : anomalyB x ≤ anomalyB 0

Uses 2

Statement usesBoundary for three anomalous gene trees

Proof usesValue \(\log(7/6)\) of the three-anomaly boundary at zero

TheoremAnomaly-zone boundary blows up for short deep branches#✓fully proved

a(x) → ∞ as x → 0⁺ (Degnan & Rosenberg 2006): very short deep branches produce an anomalous gene tree however long the shallower branch is.

theorem tendsto_anomalyA : Tendsto anomalyA (𝓝[>] 0) atTop

Uses 1

Statement usesBoundary of the four-species anomaly zone

TheoremAnomalous gene tree on four species#✓fully proved

Anomalous gene tree on four species (Degnan & Rosenberg 2006): on the caterpillar species tree with deeper branch x > 0 and shallower branch y, the symmetric gene tree ((A, B), (C, D)) is more probable than the gene tree matching the species tree if and only if y < a(x). With caterpillar_le_matching this gives caterpillar_exists_anomalous_iff.

theorem caterpillar_anomalous_iff {x : ℝ} (hx : 0 < x) (y : ℝ) :
    geneTreeProb (caterpillar x y) (· = (caterpillar x y).clusters) <
        geneTreeProb (caterpillar x y) (· = balancedTree 0 1 2 3) ↔ y < anomalyA x

Uses 12 · Used by 1

Statement usesClusters of a species tree · Boundary of the four-species anomaly zone · Balanced four-gene tree · Caterpillar four-species tree · The multispecies coalescent

Proof usesCaterpillar four-gene tree · Clusters of the caterpillar species tree · Degnan–Rosenberg probability of the matching caterpillar gene tree · The boundary a(x) of the anomaly zone · Degnan–Rosenberg formula h for the gene tree ((A, B), (C, D)) · Probability of the gene tree ((A, B), (C, D)) on the caterpillar · The matching gene tree

Used byThe four-species anomaly zone

TheoremAnomaly of ((A, C), (B, D)) and ((A, D), (B, C)) on the caterpillar#✓fully proved

On the caterpillar species tree with x ≥ 0, the gene trees ((A, C), (B, D)) and ((A, D), (B, C)) are more probable than the matching gene tree if and only if y < b(x).

theorem caterpillar_anomalous_AC_BD_iff {x : ℝ} (hx : 0 ≤ x) (y : ℝ) :
    geneTreeProb (caterpillar x y) (· = (caterpillar x y).clusters) <
        geneTreeProb (caterpillar x y) (· = balancedTree 0 2 1 3) ↔ y < anomalyB x

Uses 12

Statement usesClusters of a species tree · Boundary for three anomalous gene trees · Balanced four-gene tree · Caterpillar four-species tree · The multispecies coalescent

Proof usesCaterpillar four-gene tree · Clusters of the caterpillar species tree · Degnan–Rosenberg probability of the matching caterpillar gene tree · Degnan–Rosenberg criterion: \(f(x, y) < g(x, y)\) iff \(y < b(x)\) · Degnan–Rosenberg formula g for the gene tree ((A, C), (B, D)) · Probability of the gene tree ((A, C), (B, D)) on the caterpillar · The matching gene tree

DefinitionBalanced gene tree on four genes#✓fully proved

G is one of the three balanced (symmetric) gene trees on four genes.

def IsBalancedGeneTree (G : Finset (Finset (Fin 4))) : Prop :=
  G = balancedTree 0 1 2 3 ∨ G = balancedTree 0 2 1 3 ∨ G = balancedTree 0 3 1 2

Uses 1 · Used by 2

Statement usesBalanced four-gene tree

Used byThe four-species anomaly zone · Only balanced gene trees can be anomalous on the caterpillar

TheoremOnly balanced gene trees can be anomalous on the caterpillar#✓fully proved

On the caterpillar species tree with nonnegative branch lengths, no asymmetric gene tree is more probable than the matching one (Degnan & Rosenberg 2006): only the three balanced gene trees can be anomalous.

theorem caterpillar_le_matching {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (G : Finset (Finset (Fin 4)))
    (hG : ¬ IsBalancedGeneTree G) :
    geneTreeProb (caterpillar x y) (· = G) ≤
      geneTreeProb (caterpillar x y) (· = caterpillarTree 0 1 2 3)

Uses 13 · Used by 1

Statement usesBalanced gene tree on four genes · Caterpillar four-species tree · Caterpillar four-gene tree · The multispecies coalescent

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Balanced four-gene tree · Clusters formed along a ranked history · Expectation under random joining as an average over histories · Lineages after the first coalescence events of a ranked history · Tavaré's probabilities are nonnegative

Used byThe four-species anomaly zone

Theorem\(g(x, y) \le h(x, y)\) for a nonnegative shallower branch#✓fully proved

g(x, y) ≤ h(x, y) for a nonnegative shallower branch (equality at y = 0).

theorem drG_le_drH (x : ℝ) {y : ℝ} (hy : 0 ≤ y) : drG x y ≤ drH x y

Uses 2 · Used by 1

Statement usesDegnan–Rosenberg formula g for the gene tree ((A, C), (B, D)) · Degnan–Rosenberg formula h for the gene tree ((A, B), (C, D))

Used byThe four-species anomaly zone

TheoremThe four-species anomaly zone#✓fully proved

The four-species anomaly zone (Degnan & Rosenberg 2006, Definition 1 and Figure 2): the caterpillar species tree with deeper branch x > 0 and shallower branch y ≥ 0 has an anomalous gene tree, one strictly more probable than the gene tree matching the species tree, if and only if y < a(x).

theorem caterpillar_exists_anomalous_iff {x y : ℝ} (hx : 0 < x) (hy : 0 ≤ y) :
    (∃ G, geneTreeProb (caterpillar x y) (· = (caterpillar x y).clusters) <
        geneTreeProb (caterpillar x y) (· = G)) ↔ y < anomalyA x

Uses 16

Statement usesClusters of a species tree · Boundary of the four-species anomaly zone · Caterpillar four-species tree · The multispecies coalescent

Proof usesBalanced gene tree on four genes · Balanced four-gene tree · Caterpillar four-gene tree · Anomalous gene tree on four species · Only balanced gene trees can be anomalous on the caterpillar · Clusters of the caterpillar species tree · Degnan–Rosenberg formula g for the gene tree ((A, C), (B, D)) · \(g(x, y) \le h(x, y)\) for a nonnegative shallower branch · Degnan–Rosenberg formula h for the gene tree ((A, B), (C, D)) · 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

TheoremNo anomalous gene trees on the balanced four-species tree#✓fully proved

No anomalous gene trees on the balanced four-species tree (Degnan & Rosenberg 2006): for nonnegative branch lengths, no gene tree is more probable than the one matching the species tree ((0, 1), (2, 3)). Given the numbers of lineages entering the root population, the matching tree is already the most probable outcome of random joining.

theorem balanced_no_anomaly {y₁ y₂ : ℝ} (hy₁ : 0 ≤ y₁) (hy₂ : 0 ≤ y₂)
    (G : Finset (Finset (Fin 4))) :
    geneTreeProb (balanced y₁ y₂) (· = G) ≤
      geneTreeProb (balanced y₁ y₂) (· = balancedTree 0 1 2 3)

Uses 13

Statement usesBalanced four-species tree · Balanced four-gene tree · The multispecies coalescent

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Rooted binary species tree with branch lengths · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch · Expectation under random joining as an average over histories · Lineages after the first coalescence events of a ranked history · Tavaré's probabilities are nonnegative

Unrooted quartets

DefinitionGene tree displaying a quartet split#✓fully proved

A rooted gene tree on four genes G (a set of clusters) displays the quartet split ab | cd, where {c, d} is the complement of {a, b}: forgetting the root, the internal edge separates {a, b} from {c, d}; equivalently {a, b} or {c, d} is a cluster.

def DisplaysSplit (a b : Fin 4) (G : Finset (Finset (Fin 4))) : Prop :=
  {a, b} ∈ G ∨ univ \ {a, b} ∈ G

Used by 7

Used byNo 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 · 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 · The species quartet maximizes quartet support

TheoremNo anomalous unrooted quartets, caterpillar species tree#✓fully proved

No anomalous unrooted quartets, caterpillar species tree (Allman, Degnan & Rhodes 2011): the unrooted gene quartet matches the species quartet 01 | 23 with probability 1 - (2/3) e^{-y}, where y is the length of the internal edge of the unrooted species quartet (the shallower internal branch).

theorem geneTreeProb_caterpillar_split_01 (x y : ℝ) :
    geneTreeProb (caterpillar x y) (DisplaysSplit 0 1) = 1 - 2 / 3 * Real.exp (-y)

Uses 18 · Used by 1

Statement usesGene tree displaying a quartet split · Caterpillar four-species tree · The multispecies coalescent

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Rooted binary species tree with branch lengths · Coalescence along one branch of the species tree · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch · Rational-valued expectation under random joining · Lineages after the first coalescence events of a ranked history · Three lineages have one ancestor at time \(t\) · Three lineages remain distinct with probability \(e^{-3t}\) · Three lineages have two ancestors at time \(t\) · Two lineages coalesce with probability \(1 - e^{-t}\) · Two lineages remain distinct with probability \(e^{-t}\)

Used byThe species quartet maximizes quartet support

TheoremProbability of quartet split 02|13 on the caterpillar tree#✓fully proved

On the caterpillar species tree the discordant unrooted gene quartet 02 | 13 has probability (1/3) e^{-y}.

theorem geneTreeProb_caterpillar_split_02 (x y : ℝ) :
    geneTreeProb (caterpillar x y) (DisplaysSplit 0 2) = 1 / 3 * Real.exp (-y)

Uses 18 · Used by 1

Statement usesGene tree displaying a quartet split · Caterpillar four-species tree · The multispecies coalescent

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Rooted binary species tree with branch lengths · Coalescence along one branch of the species tree · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch · Rational-valued expectation under random joining · Lineages after the first coalescence events of a ranked history · Three lineages have one ancestor at time \(t\) · Three lineages remain distinct with probability \(e^{-3t}\) · Three lineages have two ancestors at time \(t\) · Two lineages coalesce with probability \(1 - e^{-t}\) · Two lineages remain distinct with probability \(e^{-t}\)

Used byThe species quartet maximizes quartet support

TheoremProbability of quartet split 03|12 on the caterpillar tree#✓fully proved

On the caterpillar species tree the discordant unrooted gene quartet 03 | 12 has probability (1/3) e^{-y}.

theorem geneTreeProb_caterpillar_split_03 (x y : ℝ) :
    geneTreeProb (caterpillar x y) (DisplaysSplit 0 3) = 1 / 3 * Real.exp (-y)

Uses 18 · Used by 1

Statement usesGene tree displaying a quartet split · Caterpillar four-species tree · The multispecies coalescent

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Rooted binary species tree with branch lengths · Coalescence along one branch of the species tree · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch · Rational-valued expectation under random joining · Lineages after the first coalescence events of a ranked history · Three lineages have one ancestor at time \(t\) · Three lineages remain distinct with probability \(e^{-3t}\) · Three lineages have two ancestors at time \(t\) · Two lineages coalesce with probability \(1 - e^{-t}\) · Two lineages remain distinct with probability \(e^{-t}\)

Used byThe species quartet maximizes quartet support

TheoremNo anomalous unrooted quartets, balanced species tree#✓fully proved

No anomalous unrooted quartets, balanced species tree (Allman, Degnan & Rhodes 2011): on ((0, 1), (2, 3)) the unrooted gene quartet matches 01 | 23 with probability 1 - (2/3) e^{-(y₁ + y₂)}, where y₁ + y₂ is the internal edge of the unrooted species quartet.

theorem geneTreeProb_balanced_split_01 (y₁ y₂ : ℝ) :
    geneTreeProb (balanced y₁ y₂) (DisplaysSplit 0 1) = 1 - 2 / 3 * Real.exp (-(y₁ + y₂))

Uses 14 · Used by 1

Statement usesGene tree displaying a quartet split · Balanced four-species tree · The multispecies coalescent

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Rooted binary species tree with branch lengths · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch · Rational-valued expectation under random joining · Lineages after the first coalescence events of a ranked history · Two lineages coalesce with probability \(1 - e^{-t}\) · Two lineages remain distinct with probability \(e^{-t}\)

Used byThe species quartet maximizes quartet support

TheoremProbability of quartet split 02|13 on the balanced tree#✓fully proved

On the balanced species tree the discordant unrooted gene quartet 02 | 13 has probability (1/3) e^{-(y₁ + y₂)}.

theorem geneTreeProb_balanced_split_02 (y₁ y₂ : ℝ) :
    geneTreeProb (balanced y₁ y₂) (DisplaysSplit 0 2) = 1 / 3 * Real.exp (-(y₁ + y₂))

Uses 13 · Used by 1

Statement usesGene tree displaying a quartet split · Balanced four-species tree · The multispecies coalescent

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Rooted binary species tree with branch lengths · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch · Rational-valued expectation under random joining · Lineages after the first coalescence events of a ranked history · Two lineages remain distinct with probability \(e^{-t}\)

Used byThe species quartet maximizes quartet support

TheoremProbability of quartet split 03|12 on the balanced tree#✓fully proved

On the balanced species tree the discordant unrooted gene quartet 03 | 12 has probability (1/3) e^{-(y₁ + y₂)}.

theorem geneTreeProb_balanced_split_03 (y₁ y₂ : ℝ) :
    geneTreeProb (balanced y₁ y₂) (DisplaysSplit 0 3) = 1 / 3 * Real.exp (-(y₁ + y₂))

Uses 13 · Used by 1

Statement usesGene tree displaying a quartet split · Balanced four-species tree · The multispecies coalescent

Proof usesTavaré's formula for the number of ancestral lineages · Unordered pairs of lineages · Ranked labeled history · Random joining · Rooted binary species tree with branch lengths · Clusters formed along a ranked history · Law of the lineages leaving a species-tree branch · Rational-valued expectation under random joining · Lineages after the first coalescence events of a ranked history · Two lineages remain distinct with probability \(e^{-t}\)

Used byThe species quartet maximizes quartet support

TheoremThe species quartet maximizes quartet support#✓fully proved

The species quartet maximizes quartet support (Allman, Degnan & Rhodes 2011; Mirarab et al. 2014): for a positive internal edge, the unrooted gene quartet matching the species quartet is strictly the most probable of the three, on both four-species shapes. Since the expected quartet support of a candidate four-species tree (one quartet) is the probability of its quartet, the species tree maximizes it.

theorem split_01_most_probable {x y y₁ y₂ : ℝ} (hy : 0 < y) (hy₁₂ : 0 < y₁ + y₂) :
    geneTreeProb (caterpillar x y) (DisplaysSplit 0 2) <
        geneTreeProb (caterpillar x y) (DisplaysSplit 0 1) ∧
      geneTreeProb (caterpillar x y) (DisplaysSplit 0 3) <
        geneTreeProb (caterpillar x y) (DisplaysSplit 0 1) ∧
      geneTreeProb (balanced y₁ y₂) (DisplaysSplit 0 2) <
        geneTreeProb (balanced y₁ y₂) (DisplaysSplit 0 1) ∧
      geneTreeProb (balanced y₁ y₂) (DisplaysSplit 0 3) <
        geneTreeProb (balanced y₁ y₂) (DisplaysSplit 0 1)

Uses 10

Statement usesGene tree displaying a quartet split · Balanced four-species tree · Caterpillar four-species tree · The multispecies coalescent

Proof usesNo 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 · 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

Clade probabilities under random joining

DefinitionClade of a ranked history#✓fully proved

The set S of sampled genes is a clade of the ranked history h: it is a block of one of the ancestral partitions of h, i.e. the set of descendants of some lineage.

def IsClade {m : ℕ} (h : RankedHistory m) (S : Finset (Fin m)) : Prop :=
  ∃ P ∈ partitionsOf h, S ∈ P

Uses 2 · Used by 2

Statement usesRanked labeled history · Ancestral partitions along a history as sets of blocks

Used byClade probability · Clade probability under random joining for at most five genes

TheoremClade probability#✓fully proved

Clade probability (Rosenberg 2003): under random joining, a fixed set of k among m genes, 1 ≤ k < m, is a clade with probability 2m / (k (k + 1) C(m, k)).

theorem randomJoining_isClade {m : ℕ} (S : Finset (Fin m)) (hS : 1 ≤ S.card)
    (hSm : S.card < m) :
    (randomJoining m).real {h | IsClade h S} =
      2 * m / (S.card * (S.card + 1) * (m.choose S.card : ℝ))

Uses 10 · Used by 1

Statement usesUnordered pairs of lineages · Ranked labeled history · Random joining · Clade of a ranked history

Proof usesLineage blocks after the first coalescence events · Number of ranked labeled histories · Merging two lineage blocks · Ancestral partitions along a history as sets of blocks · Lineages after the first coalescence events of a ranked history · Random-joining probability as a fraction of ranked histories

Used byClade probability under random joining for at most five genes

TheoremClade probability under random joining for at most five genes#✓fully proved

The case m ≤ 5 of randomJoining_isClade.

@[deprecated "Use `randomJoining_isClade`." (since := "2026-11-02")]
theorem randomJoining_isClade_of_le_five {m : ℕ} (_hm : m ≤ 5) (S : Finset (Fin m))
    (hS : 1 ≤ S.card) (hSm : S.card < m) :
    (randomJoining m).real {h | IsClade h S} =
      2 * m / (S.card * (S.card + 1) * (m.choose S.card : ℝ))

Uses 5

Statement usesUnordered pairs of lineages · Ranked labeled history · Random joining · Clade of a ranked history

Proof usesClade probability

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.