Neighbor joining

23 fully proved

The algorithm

DefinitionInitial cluster dissimilarity in neighbor joining#✓fully proved

The dissimilarity between clusters at the start of neighbor joining: on singletons, initialDist d {x} {y} = d x y (only singleton values are used).

def initialDist (d : X → X → ℝ) (u v : Finset X) : ℝ :=
  ∑ x ∈ u, ∑ y ∈ v, d x y

Used by 10

Used byThe first join of neighbor joining on a perturbed tree metric joins a cherry · Robust cherry lemma for neighbor joining · Neighbor joining averages up to row shifts · Neighbor joining preserves symmetry and zero diagonal · The first join of neighbor joining on a tree metric joins a cherry · On a tree metric, a pair of taxa minimizing the Q-criterion is a cherry · Neighbor joining is exact on tree metrics · Neighbor joining forms the splits of a tree when every join forms a side · Runs of neighbor joining · Q-criterion of two singleton clusters

DefinitionNeighbor-joining Q-criterion#✓fully proved

The Studier–Keppler form of the neighbor-joining criterion on the cluster set S: Q(a, b) = (|S| - 2) D a b - ∑_{c ∈ S} D a c - ∑_{c ∈ S} D b c.

def qCriterion (S : Finset (Finset X)) (D : Finset X → Finset X → ℝ) (a b : Finset X) : ℝ :=
  ((S.card : ℝ) - 2) * D a b - ∑ c ∈ S, D a c - ∑ c ∈ S, D b c

Used by 15

Used byThe first join of neighbor joining on a perturbed tree metric joins a cherry · Robust cherry lemma for neighbor joining · Neighbor joining averages up to row shifts · Atteson's theorem: neighbor joining has ℓ∞ radius 1/2 · The shifting lemma · The BME length of a join in terms of the Q-criterion · Q-minimality is cherry-length minimality at a run state · Minimizing Q is minimizing the local star BME length of the join · Neighbor joining preserves symmetry and zero diagonal · The first join of neighbor joining on a tree metric joins a cherry · On a tree metric, a pair of taxa minimizing the Q-criterion is a cherry · Neighbor joining is exact on tree metrics · Neighbor joining forms the splits of a tree when every join forms a side · Runs of neighbor joining · Q-criterion of two singleton clusters

DefinitionCluster dissimilarity after a neighbor-joining step#✓fully proved

The cluster dissimilarity after joining a and b: the new cluster a ∪ b is at (D a c + D b c - D a b) / 2 from every other cluster c, and at 0 from itself; other values are unchanged.

noncomputable def joinDist (D : Finset X → Finset X → ℝ) (a b : Finset X) (u v : Finset X) : ℝ :=
  if u = a ∪ b then (if v = a ∪ b then 0 else (D a v + D b v - D a b) / 2)
  else if v = a ∪ b then (D a u + D b u - D a b) / 2 else D u v

Used by 5

Used byNeighbor joining averages up to row shifts · Neighbor joining preserves symmetry and zero diagonal · Neighbor joining is exact on tree metrics · Neighbor joining forms the splits of a tree when every join forms a side · Runs of neighbor joining

InductiveRuns of neighbor joining#✓fully proved

NJRun d S D C: some run of neighbor joining on the dissimilarity d reaches the cluster set S with cluster dissimilarity D, having formed the clusters in C. A join is allowed while at least four clusters remain, for any pair of distinct clusters minimizing qCriterion.

inductive NJRun [Fintype X] (d : X → X → ℝ) :
    Finset (Finset X) → (Finset X → Finset X → ℝ) → Finset (Finset X) → Prop
  /-- The run starts from the singletons, with no cluster formed. -/
  | init : NJRun d (Finset.univ.image fun x => {x}) (initialDist d) ∅
  /-- Join a pair of distinct clusters minimizing the Q-criterion. -/
  | join {S : Finset (Finset X)} {D : Finset X → Finset X → ℝ} {C : Finset (Finset X)}
      {a b : Finset X} :
      NJRun d S D C → 4 ≤ S.card → a ∈ S → b ∈ S → a ≠ b →
      (∀ a' ∈ S, ∀ b' ∈ S, a' ≠ b' → qCriterion S D a b ≤ qCriterion S D a' b') →
      NJRun d (insert (a ∪ b) ((S.erase a).erase b)) (joinDist D a b) (insert (a ∪ b) C)

Uses 3 · Used by 10

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

Used byNeighbor joining averages up to row shifts · Atteson's theorem: neighbor joining has ℓ∞ radius 1/2 · Q-minimality is cherry-length minimality at a run state · Neighbor joining preserves symmetry and zero diagonal · Neighbor joining is exact on tree metrics · Neighbor joining forms the splits of a tree when every join forms a side · Statistical consistency of neighbor joining under Jukes–Cantor · Statistical consistency of neighbor joining under Jukes–Cantor · Atteson's radius for the scaled tree metric · Neighbor joining recovers a tree within a radius

Binary phylogenetic trees and their splits

DefinitionBinary phylogenetic tree#✓fully proved

G with the taxon placement ι is a binary phylogenetic X-tree: G is a tree, ι is injective, the leaves (degree-one vertices) are exactly the taxa, and every other vertex has degree three.

def IsBinaryPhylogeneticTree {X : Type*} {V : Type*} [Fintype V] (G : SimpleGraph V)
    [DecidableRel G.Adj] (ι : X → V) : Prop :=
  G.IsTree ∧ Function.Injective ι ∧ (∀ v, G.degree v = 1 ↔ v ∈ Set.range ι) ∧
    ∀ v, v ∉ Set.range ι → G.degree v = 3

Used by 16

Used byThe first join of neighbor joining on a perturbed tree metric joins a cherry · Robust cherry lemma for neighbor joining · Atteson's theorem: neighbor joining has ℓ∞ radius 1/2 · A two-taxon side forms a cherry · A singleton side is a pendant leaf side · The first join of neighbor joining on a tree metric joins a cherry · On a tree metric, a pair of taxa minimizing the Q-criterion is a cherry · The path metric on a partition into sides · Neighbor joining is exact on tree metrics · Neighbor joining forms the splits of a tree when every join forms a side · Edge side at an internal vertex as a disjoint union · Leaf side of a pendant edge · Every edge side of a binary phylogenetic tree is nonempty · Statistical consistency of neighbor joining under Jukes–Cantor · Statistical consistency of neighbor joining under Jukes–Cantor · Atteson's radius for the scaled tree metric

DefinitionTaxa on one side of a tree edge#✓fully proved

The taxa on the a-side of the edge {a, b}: those whose vertex is still joined to a once the edge {a, b} is deleted.

noncomputable def side {X : Type*} [Fintype X] {V : Type*} (G : SimpleGraph V) (ι : X → V)
    (a b : V) : Finset X :=
  univ.filter fun z => (G.deleteEdges {s(a, b)}).Reachable (ι z) a

Used by 14

Used byRobust cherry lemma for neighbor joining · Atteson's theorem: neighbor joining has ℓ∞ radius 1/2 · A two-taxon side forms a cherry · Split decomposition of a tree metric · A singleton side is a pendant leaf side · On a tree metric, a pair of taxa minimizing the Q-criterion is a cherry · The path metric on a partition into sides · Neighbor joining is exact on tree metrics · Neighbor joining forms the splits of a tree when every join forms a side · Splits of two tree edges are compatible · Edge side at an internal vertex as a disjoint union · Leaf side of a pendant edge · Every edge side of a binary phylogenetic tree is nonempty · Two sides of a tree edge partition the taxa

DefinitionContribution of a split to the neighbor-joining score#✓fully proved

The contribution of one split {A, Aᶜ} to the neighbor-joining score of the pair x, y: the number of taxa on the far side of the split when x, y lie on the same side, and 1 when the split separates them.

def splitGain {X : Type*} [Fintype X] [DecidableEq X] (A : Finset X) (x y : X) : ℝ :=
  if x ∈ A then (if y ∈ A then ((univ \ A).card : ℝ) else 1)
  else (if y ∈ A then 1 else (A.card : ℝ))

Used by 4

Used byOn a tree metric, a pair of taxa minimizing the Q-criterion is a cherry · Cherry lemma for split systems · Neighbor joining is exact on tree metrics · The Q-criterion of a split-decomposed dissimilarity

TheoremTwo sides of a tree edge partition the taxa#✓fully proved

In a tree, the two sides of an edge partition the taxa.

theorem side_swap {X : Type*} [Fintype X] [DecidableEq X] {V : Type*} {G : SimpleGraph V}
    {ι : X → V} (hG : G.IsTree) {a b : V} (hab : G.Adj a b) :
    side G ι b a = univ \ side G ι a b

Uses 1 · Used by 6

Statement usesTaxa on one side of a tree edge

Used byRobust cherry lemma for neighbor joining · On a tree metric, a pair of taxa minimizing the Q-criterion is a cherry · The path metric on a partition into sides · Neighbor joining is exact on tree metrics · Neighbor joining forms the splits of a tree when every join forms a side · Edge side at an internal vertex as a disjoint union

TheoremSplits of two tree edges are compatible#✓fully proved

In a tree, the splits of any two edges are compatible: one side of the first edge lies inside one side of the second.

theorem side_compat {X : Type*} [Fintype X] {V : Type*} {G : SimpleGraph V} {ι : X → V}
    (hG : G.IsTree) {a b c e : V} (hab : G.Adj a b) (hce : G.Adj c e) :
    side G ι b a ⊆ side G ι c e ∨ side G ι b a ⊆ side G ι e c ∨
      side G ι a b ⊆ side G ι c e ∨ side G ι a b ⊆ side G ι e c

Uses 1 · Used by 5

Statement usesTaxa on one side of a tree edge

Used byRobust cherry lemma for neighbor joining · On a tree metric, a pair of taxa minimizing the Q-criterion is a cherry · The path metric on a partition into sides · Neighbor joining is exact on tree metrics · Neighbor joining forms the splits of a tree when every join forms a side

TheoremLeaf side of a pendant edge#✓fully proved

The leaf side of a pendant edge holds only the leaf's taxon.

theorem side_leaf {X : Type*} [Fintype X] {V : Type*} [Fintype V] {G : SimpleGraph V}
    [DecidableRel G.Adj] {ι : X → V} (hT : IsBinaryPhylogeneticTree G ι) {z : X} {b : V}
    (hb : G.Adj (ι z) b) : side G ι (ι z) b = {z}

Uses 2 · Used by 7

Statement usesBinary phylogenetic tree · Taxa on one side of a tree edge

Used byRobust cherry lemma for neighbor joining · A two-taxon side forms a cherry · A singleton side is a pendant leaf side · On a tree metric, a pair of taxa minimizing the Q-criterion is a cherry · The path metric on a partition into sides · Neighbor joining is exact on tree metrics · Neighbor joining forms the splits of a tree when every join forms a side

TheoremEvery edge side of a binary phylogenetic tree is nonempty#✓fully proved

Every side of every edge of a binary phylogenetic tree holds a taxon.

theorem side_nonempty {X : Type*} [Fintype X] {V : Type*} [Fintype V] {G : SimpleGraph V}
    [DecidableRel G.Adj] {ι : X → V} (hT : IsBinaryPhylogeneticTree G ι) {a b : V}
    (hab : G.Adj a b) : (side G ι a b).Nonempty

Uses 2 · Used by 7

Statement usesBinary phylogenetic tree · Taxa on one side of a tree edge

Used byRobust cherry lemma for neighbor joining · A two-taxon side forms a cherry · A singleton side is a pendant leaf side · On a tree metric, a pair of taxa minimizing the Q-criterion is a cherry · The path metric on a partition into sides · Neighbor joining is exact on tree metrics · Neighbor joining forms the splits of a tree when every join forms a side

TheoremEdge side at an internal vertex as a disjoint union#✓fully proved

At an internal vertex a with neighbor b, the a-side of {a, b} is the disjoint union of the far sides of the other two edges at a.

theorem side_eq_union {X : Type*} [Fintype X] [DecidableEq X] {V : Type*} [Fintype V]
    {G : SimpleGraph V} [DecidableRel G.Adj] {ι : X → V} (hT : IsBinaryPhylogeneticTree G ι)
    {a b : V} (ha : a ∉ Set.range ι) (hab : G.Adj a b) :
    ∃ c e, G.Adj a c ∧ G.Adj a e ∧ c ≠ b ∧ e ≠ b ∧ c ≠ e ∧
      Disjoint (side G ι c a) (side G ι e a) ∧ side G ι a b = side G ι c a ∪ side G ι e a

Uses 3 · Used by 7

Statement usesBinary phylogenetic tree · Taxa on one side of a tree edge

Proof usesTwo sides of a tree edge partition the taxa

Used byRobust cherry lemma for neighbor joining · A two-taxon side forms a cherry · A singleton side is a pendant leaf side · On a tree metric, a pair of taxa minimizing the Q-criterion is a cherry · The path metric on a partition into sides · Neighbor joining is exact on tree metrics · Neighbor joining forms the splits of a tree when every join forms a side

TheoremSplit decomposition of a tree metric#✓fully proved

The path length between two taxa is half the sum, over the darts (oriented edges) of the tree, of the lengths of the edges whose split separates them.

theorem dist_eq_sum_darts {X : Type*} [Fintype X] [DecidableEq X] {V : Type*} [Fintype V]
    {G : SimpleGraph V} [DecidableRel G.Adj] {ι : X → V} (hG : G.IsTree) {w : Sym2 V → ℝ}
    {d : X → X → ℝ}
    (hd : ∀ x y (p : G.Walk (ι x) (ι y)), p.IsPath → d x y = (p.edges.map w).sum) (x y : X) :
    d x y = (1 / 2) * ∑ t : G.Dart,
      w t.edge * (if (x ∈ side G ι t.fst t.snd ↔ y ∈ side G ι t.fst t.snd) then 0 else 1)

Uses 1 · Used by 4

Statement usesTaxa on one side of a tree edge

Used byRobust cherry lemma for neighbor joining · On a tree metric, a pair of taxa minimizing the Q-criterion is a cherry · The path metric on a partition into sides · Neighbor joining is exact on tree metrics

The cherry lemma for compatible binary split systems

TheoremCherry lemma for split systems#✓fully proved

For a compatible system of splits with positive weights, containing every trivial split and binary (every side with at least two taxa is the disjoint union of two sides), on at least four taxa, a pair maximizing the total splitGain is a side of some split.

theorem exists_eq_pair_of_isMax {X : Type*} [Fintype X] [DecidableEq X] {E : Type*} [Fintype E]
    (A : E → Finset X) (w : E → ℝ) (hw : ∀ e, 0 < w e) (hne : ∀ e, (A e).Nonempty)
    (hcompl : ∀ e, ∃ e', A e' = univ \ A e)
    (hcompat : ∀ e e', Disjoint (A e) (A e') ∨ A e ⊆ A e' ∨ A e' ⊆ A e ∨ A e ∪ A e' = univ)
    (hbin : ∀ e, 2 ≤ (A e).card → ∃ e₁ e₂, Disjoint (A e₁) (A e₂) ∧ A e₁ ∪ A e₂ = A e)
    (hsingle : ∀ z, ∃ e, A e = {z}) (hX : 4 ≤ Fintype.card X) {x y : X} (hxy : x ≠ y)
    (hmax : ∀ x' y', x' ≠ y' →
      ∑ e, w e * splitGain (A e) x' y' ≤ ∑ e, w e * splitGain (A e) x y) :
    ∃ e, A e = {x, y}

Uses 1 · Used by 2

Statement usesContribution of a split to the neighbor-joining score

Used byOn a tree metric, a pair of taxa minimizing the Q-criterion is a cherry · Neighbor joining is exact on tree metrics

The Q-criterion as a sum over splits

TheoremQ-criterion of two singleton clusters#✓fully proved

The Q-criterion of two singleton clusters at the start of neighbor joining: Q({x}, {y}) = (|X| - 2) d x y - ∑_z d x z - ∑_z d y z.

theorem qCriterion_singleton {X : Type*} [Fintype X] [DecidableEq X] (d : X → X → ℝ)
    (x y : X) :
    qCriterion (univ.image fun x => ({x} : Finset X)) (initialDist d) {x} {y} =
      ((Fintype.card X : ℝ) - 2) * d x y - ∑ z, d x z - ∑ z, d y z

Uses 2 · Used by 2

Statement usesInitial cluster dissimilarity in neighbor joining · Neighbor-joining Q-criterion

Used byRobust cherry lemma for neighbor joining · On a tree metric, a pair of taxa minimizing the Q-criterion is a cherry

TheoremThe Q-criterion of a split-decomposed dissimilarity#✓fully proved

If d x y is half the total weight of the splits A e separating x and y, then (|X| - 2) d x y - ∑_z d x z - ∑_z d y z = -∑ e, w e * splitGain (A e) x y.

theorem sub_sum_sub_sum_eq_neg_sum_splitGain {X : Type*} [Fintype X] [DecidableEq X] {E : Type*}
    [Fintype E] (A : E → Finset X) (w : E → ℝ) {d : X → X → ℝ}
    (hd : ∀ x y, d x y = (1 / 2) * ∑ e, w e * (if (x ∈ A e ↔ y ∈ A e) then 0 else 1))
    (x y : X) :
    ((Fintype.card X : ℝ) - 2) * d x y - ∑ z, d x z - ∑ z, d y z =
      -∑ e, w e * splitGain (A e) x y

Uses 1 · Used by 2

Statement usesContribution of a split to the neighbor-joining score

Used byOn a tree metric, a pair of taxa minimizing the Q-criterion is a cherry · Neighbor joining is exact on tree metrics

Assembly

TheoremA singleton side is a pendant leaf side#✓fully proved

A side holding a single taxon z is the leaf side of z's pendant edge.

theorem eq_of_side_eq_singleton {X : Type*} [Fintype X] {V : Type*}
    [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {ι : X → V}
    (hT : IsBinaryPhylogeneticTree G ι) {c a : V} (hca : G.Adj c a) {z : X}
    (h : side G ι c a = {z}) : c = ι z

Uses 5 · Used by 1

Statement usesBinary phylogenetic tree · Taxa on one side of a tree edge

Proof usesEdge side at an internal vertex as a disjoint union · Leaf side of a pendant edge · Every edge side of a binary phylogenetic tree is nonempty

Used byA two-taxon side forms a cherry

TheoremA two-taxon side forms a cherry#✓fully proved

If a side of the edge {a, b} is the pair {x, y}, then a is a common neighbor of the leaves ι x and ι y: they form a cherry.

theorem adj_adj_of_side_eq_pair {X : Type*} [Fintype X] [DecidableEq X] {V : Type*}
    [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {ι : X → V}
    (hT : IsBinaryPhylogeneticTree G ι) {a b : V} (hab : G.Adj a b) {x y : X} (hxy : x ≠ y)
    (h : side G ι a b = {x, y}) : G.Adj (ι x) a ∧ G.Adj (ι y) a

Uses 6 · Used by 2

Statement usesBinary phylogenetic tree · Taxa on one side of a tree edge

Proof usesA singleton side is a pendant leaf side · Edge side at an internal vertex as a disjoint union · Leaf side of a pendant edge · Every edge side of a binary phylogenetic tree is nonempty

Used byRobust cherry lemma for neighbor joining · On a tree metric, a pair of taxa minimizing the Q-criterion is a cherry

TheoremOn a tree metric, a pair of taxa minimizing the Q-criterion is a cherry#✓fully proved

(Saitou & Nei 1987; Studier & Keppler 1988; Bryant 2005). Let d be the path-length metric of a binary phylogenetic X-tree (G, ι) with positive edge lengths w and at least four taxa. If the distinct taxa x, y minimize the Q-criterion over all pairs of distinct singleton clusters at the start of neighbor joining, then ι x and ι y have a common neighbor.

theorem exists_adj_adj_of_qCriterion_min {X : Type*} [Fintype X] [DecidableEq X] {V : Type*}
    [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {ι : X → V}
    (hT : IsBinaryPhylogeneticTree G ι) {w : Sym2 V → ℝ} (hw : ∀ e ∈ G.edgeSet, 0 < w e)
    {d : X → X → ℝ}
    (hd : ∀ x y (p : G.Walk (ι x) (ι y)), p.IsPath → d x y = (p.edges.map w).sum)
    (hX : 4 ≤ Fintype.card X) {x y : X} (hxy : x ≠ y)
    (hmin : ∀ a' ∈ univ.image (fun x => ({x} : Finset X)),
      ∀ b' ∈ univ.image (fun x => ({x} : Finset X)), a' ≠ b' →
        qCriterion (univ.image fun x => ({x} : Finset X)) (initialDist d) {x} {y} ≤
          qCriterion (univ.image fun x => ({x} : Finset X)) (initialDist d) a' b') :
    ∃ u, G.Adj (ι x) u ∧ G.Adj (ι y) u

Uses 15 · Used by 1

Statement usesBinary phylogenetic tree · Initial cluster dissimilarity in neighbor joining · Neighbor-joining Q-criterion

Proof usesA two-taxon side forms a cherry · Split decomposition of a tree metric · Cherry lemma for split systems · Q-criterion of two singleton clusters · Taxa on one side of a tree edge · Splits of two tree edges are compatible · Edge side at an internal vertex as a disjoint union · Leaf side of a pendant edge · Every edge side of a binary phylogenetic tree is nonempty · Two sides of a tree edge partition the taxa · Contribution of a split to the neighbor-joining score · The Q-criterion of a split-decomposed dissimilarity

Used byThe first join of neighbor joining on a tree metric joins a cherry

TheoremThe first join of neighbor joining on a tree metric joins a cherry#✓fully proved

On the path-length metric of a binary phylogenetic X-tree with positive edge lengths and at least four taxa, any pair of clusters that neighbor joining may join from the initial singletons consists of two taxa with a common neighbor.

theorem NJRun.exists_adj_adj_of_join_init {X : Type*} [Fintype X] [DecidableEq X] {V : Type*}
    [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {ι : X → V}
    (hT : IsBinaryPhylogeneticTree G ι) {w : Sym2 V → ℝ} (hw : ∀ e ∈ G.edgeSet, 0 < w e)
    {d : X → X → ℝ}
    (hd : ∀ x y (p : G.Walk (ι x) (ι y)), p.IsPath → d x y = (p.edges.map w).sum)
    {a b : Finset X} (ha : a ∈ univ.image fun x => ({x} : Finset X))
    (hb : b ∈ univ.image fun x => ({x} : Finset X)) (hab : a ≠ b)
    (h4 : 4 ≤ (univ.image fun x => ({x} : Finset X)).card)
    (hmin : ∀ a' ∈ univ.image (fun x => ({x} : Finset X)),
      ∀ b' ∈ univ.image (fun x => ({x} : Finset X)), a' ≠ b' →
        qCriterion (univ.image fun x => ({x} : Finset X)) (initialDist d) a b ≤
          qCriterion (univ.image fun x => ({x} : Finset X)) (initialDist d) a' b') :
    ∃ x y u, a = {x} ∧ b = {y} ∧ x ≠ y ∧ G.Adj (ι x) u ∧ G.Adj (ι y) u

Uses 4

Statement usesBinary phylogenetic tree · Initial cluster dissimilarity in neighbor joining · Neighbor-joining Q-criterion

Proof usesOn a tree metric, a pair of taxa minimizing the Q-criterion is a cherry

TheoremThe path metric on a partition into sides#✓fully proved

Let S partition the taxa of a binary phylogenetic X-tree (G, ι) with positive edge lengths w and path-length metric d into sides of edges. Then there is a system of splits A e (e : E) of the set of clusters with positive weights w' e, closed under complement, pairwise compatible, binary, and containing every trivial split, such that * the weight of every internal split (both sides with at least two clusters) is the length of an edge with both endpoints internal; * a split whose side is {s, t} comes from an edge with side s ∪ t; * for taxa x ∈ s and y ∈ t of distinct clusters, d x y is half the total weight of the splits separating s from t, plus a term ρ s x depending only on s and x and a term ρ t y. In the construction, the splits are those of the edges that cut no cluster.

Cslib.Bioinformatics.Phylogenetics.NeighborJoining.exists_splitSystem_of_partition · 19 lines

theorem exists_splitSystem_of_partition {X : Type*} [Fintype X] [DecidableEq X] {V : Type u}
    [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {ι : X → V}
    (hT : IsBinaryPhylogeneticTree G ι) {w : Sym2 V → ℝ} (hw : ∀ e ∈ G.edgeSet, 0 < w e)
    {d : X → X → ℝ}
    (hd : ∀ x y (p : G.Walk (ι x) (ι y)), p.IsPath → d x y = (p.edges.map w).sum)
    {S : Finset (Finset X)} (hside : ∀ s ∈ S, ∃ u v, G.Adj u v ∧ side G ι u v = s)
    (hdisj : ∀ s ∈ S, ∀ t ∈ S, s ≠ t → Disjoint s t) (hcover : ∀ x, ∃ s ∈ S, x ∈ s) :
    ∃ (E : Type u) (_ : Fintype E) (A : E → Finset {s // s ∈ S}) (w' : E → ℝ)
      (ρ : {s // s ∈ S} → X → ℝ),
      (∀ e, 0 < w' e) ∧ (∀ e, (A e).Nonempty) ∧ (∀ e, ∃ e', A e' = univ \ A e) ∧
      (∀ e e', Disjoint (A e) (A e') ∨ A e ⊆ A e' ∨ A e' ⊆ A e ∨ A e ∪ A e' = univ) ∧
      (∀ e, 2 ≤ (A e).card → ∃ e₁ e₂, Disjoint (A e₁) (A e₂) ∧ A e₁ ∪ A e₂ = A e) ∧
      (∀ s, ∃ e, A e = {s}) ∧
      (∀ e, 2 ≤ (A e).card → 2 ≤ (univ \ A e).card →
        ∃ u v, G.Adj u v ∧ u ∉ Set.range ι ∧ v ∉ Set.range ι ∧ w' e = w s(u, v)) ∧
      (∀ e s t, A e = {s, t} → ∃ u v, G.Adj u v ∧ side G ι u v = (s : Finset X) ∪ t) ∧
      ∀ s t : {s // s ∈ S}, s ≠ t → ∀ x ∈ (s : Finset X), ∀ y ∈ (t : Finset X),
        d x y = (1 / 2) * ∑ e, w' e * (if (s ∈ A e ↔ t ∈ A e) then 0 else 1) +
          ρ s x + ρ t y

Uses 8 · Used by 1

Statement usesBinary phylogenetic tree · Taxa on one side of a tree edge

Proof usesSplit decomposition of a tree metric · Splits of two tree edges are compatible · Edge side at an internal vertex as a disjoint union · Leaf side of a pendant edge · Every edge side of a binary phylogenetic tree is nonempty · Two sides of a tree edge partition the taxa

Used byAtteson's theorem: neighbor joining has ℓ∞ radius 1/2

TheoremNeighbor joining is exact on tree metrics#✓fully proved

Let d be the path-length metric of a binary phylogenetic X-tree (G, ι) with positive edge lengths w. Then every complete run of neighbor joining (stopped with at most three clusters) forms exactly the splits of the internal edges of the tree: a set of taxa A or its complement is a formed cluster if and only if A is the set of taxa on the a-side of an edge {a, b} with both endpoints internal.

theorem njRun_splits {X : Type*} [DecidableEq X] [Fintype X] {V : Type*} [Fintype V]
    {G : SimpleGraph V} [DecidableRel G.Adj] {ι : X → V} (hT : IsBinaryPhylogeneticTree G ι)
    {w : Sym2 V → ℝ} (hw : ∀ e ∈ G.edgeSet, 0 < w e) {d : X → X → ℝ}
    (hd : ∀ x y (p : G.Walk (ι x) (ι y)), p.IsPath → d x y = (p.edges.map w).sum)
    {S : Finset (Finset X)} {D : Finset X → Finset X → ℝ} {C : Finset (Finset X)}
    (hrun : NJRun d S D C) (hS : S.card ≤ 3) (A : Finset X) :
    (A ∈ C ∨ Finset.univ \ A ∈ C) ↔
      ∃ a b, G.Adj a b ∧ a ∉ Set.range ι ∧ b ∉ Set.range ι ∧
        ∀ x, x ∈ A ↔ (G.deleteEdges {s(a, b)}).Reachable (ι x) a

Sources

• Saitou & Nei (1987); Studier & Keppler (1988); Gascuel (1994); Bryant (2005). Proves the deferred entry njRun_splits.

Uses 15

Statement usesBinary phylogenetic tree · Runs of neighbor joining

Proof usesSplit decomposition of a tree metric · Cherry lemma for split systems · Initial cluster dissimilarity in neighbor joining · Cluster dissimilarity after a neighbor-joining step · Neighbor-joining Q-criterion · Taxa on one side of a tree edge · Splits of two tree edges are compatible · Edge side at an internal vertex as a disjoint union · Leaf side of a pendant edge · Every edge side of a binary phylogenetic tree is nonempty · Two sides of a tree edge partition the taxa · Contribution of a split to the neighbor-joining score · The Q-criterion of a split-decomposed dissimilarity

TheoremNeighbor joining forms the splits of a tree when every join forms a side#✓fully proved

Let (G, ι) be a binary phylogenetic X-tree and D any dissimilarity. Suppose that whenever a run of neighbor joining on D has reached a partition S of the taxa into sides of edges of the tree (with at least four clusters) and joins two of its clusters, their union is again a side of an edge. Then every complete run of neighbor joining on D (stopped with at most three clusters) forms exactly the splits of the internal edges of the tree. This reduces the correctness of neighbor joining on D to its selection step.

theorem njRun_splits_of_join {X : Type*} [DecidableEq X] [Fintype X] {V : Type*} [Fintype V]
    {G : SimpleGraph V} [DecidableRel G.Adj] {ι : X → V} (hT : IsBinaryPhylogeneticTree G ι)
    {D : X → X → ℝ}
    (hjoin : ∀ {S : Finset (Finset X)} {Dc : Finset X → Finset X → ℝ} {C : Finset (Finset X)}
      {a b : Finset X}, NJRun D S Dc C → (∀ s ∈ S, ∃ u v, G.Adj u v ∧ side G ι u v = s) →
      (∀ s ∈ S, ∀ t ∈ S, s ≠ t → Disjoint s t) → (∀ x, ∃ s ∈ S, x ∈ s) → 4 ≤ S.card →
      a ∈ S → b ∈ S → a ≠ b →
      (∀ a' ∈ S, ∀ b' ∈ S, a' ≠ b' → qCriterion S Dc a b ≤ qCriterion S Dc a' b') →
      ∃ u v, G.Adj u v ∧ side G ι u v = a ∪ b)
    {S : Finset (Finset X)} {Dc : Finset X → Finset X → ℝ} {C : Finset (Finset X)}
    (hrun : NJRun D S Dc C) (hS : S.card ≤ 3) (A : Finset X) :
    (A ∈ C ∨ Finset.univ \ A ∈ C) ↔
      ∃ a b, G.Adj a b ∧ a ∉ Set.range ι ∧ b ∉ Set.range ι ∧
        ∀ x, x ∈ A ↔ (G.deleteEdges {s(a, b)}).Reachable (ι x) a

Uses 11 · Used by 1

Statement usesBinary phylogenetic tree · Runs of neighbor joining · Neighbor-joining Q-criterion · Taxa on one side of a tree edge

Proof usesInitial cluster dissimilarity in neighbor joining · Cluster dissimilarity after a neighbor-joining step · Splits of two tree edges are compatible · Edge side at an internal vertex as a disjoint union · Leaf side of a pendant edge · Every edge side of a binary phylogenetic tree is nonempty · Two sides of a tree edge partition the taxa

Used byAtteson's theorem: neighbor joining has ℓ∞ radius 1/2

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.