Neighbor joining and balanced minimum evolution

DefinitionGeneralized Pauplin coefficient of a cherry tree#✓fully proved

The generalized Pauplin coefficient of the pair of clusters u, v in the tree T_ab obtained from the star on S by joining a and b: 1/2 for {a, b}; 1/(2(|S| - 2)) when one of u, v is a or b and the other is not; 1/(|S| - 2) when neither is. Values on the diagonal u = v are never used.

noncomputable def cherryCoeff (S : Finset (Finset X)) (a b u v : Finset X) : ℝ :=
  if (u = a ∧ v = b) ∨ (u = b ∧ v = a) then 1 / 2
  else if u = a ∨ u = b ∨ v = a ∨ v = b then 1 / (2 * ((S.card : ℝ) - 2))
  else 1 / ((S.card : ℝ) - 2)

Used by 3

Used byBalanced minimum-evolution length of a cherry tree · The BME length of a join in terms of the Q-criterion · The coefficients give the tree length

DefinitionBalanced minimum-evolution length of a cherry tree#✓fully proved

The balanced minimum-evolution length of T_ab for the dissimilarity D: half the sum over ordered pairs of distinct clusters of cherryCoeff S a b u v * D u v, which is ∑_{u<v} cherryCoeff S a b u v * D u v when D is symmetric.

noncomputable def cherryLength (S : Finset (Finset X)) (D : Finset X → Finset X → ℝ)
    (a b : Finset X) : ℝ :=
  (∑ p ∈ S.offDiag, cherryCoeff S a b p.1 p.2 * D p.1 p.2) / 2

Uses 1 · Used by 4

Statement usesGeneralized Pauplin coefficient of a cherry tree

Used byThe BME length of a join in terms of the Q-criterion · The coefficients give the tree length · Q-minimality is cherry-length minimality at a run state · Minimizing Q is minimizing the local star BME length of the join

TheoremThe BME length of a join in terms of the Q-criterion#✓fully proved

For D symmetric and zero on the diagonal of S, |S| ≥ 3 and distinct a, b ∈ S: cherryLength S D a b = (∑_{u ≠ v ∈ S} D u v + Q(a, b)) / (2 (|S| - 2)).

theorem cherryLength_eq (S : Finset (Finset X)) (D : Finset X → Finset X → ℝ)
    (hsymm : ∀ u ∈ S, ∀ v ∈ S, D u v = D v u) (hdiag : ∀ u ∈ S, D u u = 0)
    (hS : 3 ≤ S.card) {a b : Finset X} (ha : a ∈ S) (hb : b ∈ S) (hab : a ≠ b) :
    cherryLength S D a b =
      ((∑ p ∈ S.offDiag, D p.1 p.2) + qCriterion S D a b) / (2 * ((S.card : ℝ) - 2))

Uses 3 · Used by 1

Statement usesNeighbor-joining Q-criterion · Balanced minimum-evolution length of a cherry tree

Proof usesGeneralized Pauplin coefficient of a cherry tree

Used byMinimizing Q is minimizing the local star BME length of the join

TheoremMinimizing Q is minimizing the local star BME length of the join#✓fully proved

The BME length of T_ab on the current clusters for the current cluster dissimilarity D. This is the local star identity; it is not the full Gascuel–Steel comparison on all taxa.

theorem qCriterion_le_iff_cherryLength_le (S : Finset (Finset X))
    (D : Finset X → Finset X → ℝ)
    (hsymm : ∀ u ∈ S, ∀ v ∈ S, D u v = D v u) (hdiag : ∀ u ∈ S, D u u = 0)
    (hS : 3 ≤ S.card) {a b a' b' : Finset X} (ha : a ∈ S) (hb : b ∈ S) (hab : a ≠ b)
    (ha' : a' ∈ S) (hb' : b' ∈ S) (hab' : a' ≠ b') :
    qCriterion S D a b ≤ qCriterion S D a' b' ↔ cherryLength S D a b ≤ cherryLength S D a' b'

Uses 3 · Used by 1

Statement usesNeighbor-joining Q-criterion · Balanced minimum-evolution length of a cherry tree

Proof usesThe BME length of a join in terms of the Q-criterion

Used byQ-minimality is cherry-length minimality at a run state

TheoremNeighbor joining preserves symmetry and zero diagonal#✓fully proved

Along a run of neighbor joining on a symmetric d with zero diagonal, the cluster dissimilarity stays symmetric and vanishes on every current cluster.

theorem NJRun.symm_diag [Fintype X] {d : X → X → ℝ} (hsymm : ∀ x y, d x y = d y x)
    (hdiag : ∀ x, d x x = 0) {S : Finset (Finset X)} {D : Finset X → Finset X → ℝ}
    {C : Finset (Finset X)} (hrun : NJRun d S D C) :
    (∀ u v, D u v = D v u) ∧ ∀ u ∈ S, D u u = 0

Uses 4 · Used by 1

Statement usesRuns of neighbor joining

Proof usesInitial cluster dissimilarity in neighbor joining · Cluster dissimilarity after a neighbor-joining step · Neighbor-joining Q-criterion

Used byQ-minimality is cherry-length minimality at a run state

TheoremQ-minimality is cherry-length minimality at a run state#✓fully proved

At every state of a run on a symmetric dissimilarity with zero diagonal and at least three clusters, a pair of distinct clusters minimizes the Q-criterion (the pairs NJ may join) if and only if joining it gives the smallest cherryLength, the BME length of the join tree T_ab on the current clusters for the current cluster dissimilarity D. This is the local star identity only: it does not compare partially resolved trees on all taxa under the original dissimilarity d.

theorem NJRun.isMin_qCriterion_iff_cherryLength [Fintype X] {d : X → X → ℝ} (hsymm : ∀ x y, d x y = d y x)
    (hdiag : ∀ x, d x x = 0) {S : Finset (Finset X)} {D : Finset X → Finset X → ℝ}
    {C : Finset (Finset X)} (hrun : NJRun d S D C) (hS : 3 ≤ S.card) {a b : Finset X}
    (ha : a ∈ S) (hb : b ∈ S) (hab : a ≠ b) :
    (∀ a' ∈ S, ∀ b' ∈ S, a' ≠ b' → qCriterion S D a b ≤ qCriterion S D a' b') ↔
      ∀ a' ∈ S, ∀ b' ∈ S, a' ≠ b' → cherryLength S D a b ≤ cherryLength S D a' b'

Uses 5

Statement usesRuns of neighbor joining · Neighbor-joining Q-criterion · Balanced minimum-evolution length of a cherry tree

Proof usesNeighbor joining preserves symmetry and zero diagonal · Minimizing Q is minimizing the local star BME length of the join

TheoremThe coefficients give the tree length#✓fully proved

Let T_ab carry real edge lengths: ℓ c on the pendant edge of each cluster c ∈ S and m on the edge between u and the center. If D is its path-length dissimilarity (D a b = ℓ a + ℓ b, D x c = ℓ x + m + ℓ c for x ∈ {a, b} and c another cluster, D c c' = ℓ c + ℓ c' for two other distinct clusters), then cherryLength S D a b = ∑_{c ∈ S} ℓ c + m.

theorem cherryLength_eq_length (S : Finset (Finset X)) (hS : 3 ≤ S.card) {a b : Finset X}
    (ha : a ∈ S) (hb : b ∈ S) (hab : a ≠ b) (ℓ : Finset X → ℝ) (m : ℝ)
    (D : Finset X → Finset X → ℝ)
    (hD : ∀ u ∈ S, ∀ v ∈ S, u ≠ v → D u v =
      if (u = a ∨ u = b) ∧ (v = a ∨ v = b) then ℓ u + ℓ v
      else if u = a ∨ u = b ∨ v = a ∨ v = b then ℓ u + m + ℓ v
      else ℓ u + ℓ v) :
    cherryLength S D a b = ∑ c ∈ S, ℓ c + m

Uses 2

Statement usesBalanced minimum-evolution length of a cherry tree

Proof usesGeneralized Pauplin coefficient of a cherry tree

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.