Atteson's theorem on neighbor joining

6 fully proved

Split systems

TheoremRobust cherry lemma for split systems#✓fully proved

The selection step of Atteson's theorem (Atteson 1999), with a proof after Mihaescu, Levy & Pachter (2009, Theorem 16). Let A e (e : E) be a compatible binary system of splits with positive weights w, containing every trivial split and closed under complement, on at least four taxa, and let d x y be half the total weight of the indices whose side separates x and y. Let μ be a lower bound on the weight of every internal split (both sides with at least two taxa). If D is symmetric, vanishes on the diagonal, and |D x y - d x y| < μ / 2 for all distinct x, y, then a pair of distinct taxa minimizing the Q-criterion (|X| - 2) D x y - ∑_z D x z - ∑_z D y z is a side of the split system.

Cslib.Bioinformatics.Phylogenetics.NeighborJoining.exists_eq_pair_of_qCriterion_min_of_abs_sub_lt · 16 lines

theorem exists_eq_pair_of_qCriterion_min_of_abs_sub_lt {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)
    {μ : ℝ} (hμ : ∀ e, 2 ≤ (A e).card → 2 ≤ (univ \ A e).card → μ ≤ w e)
    {d 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))
    (hDsymm : ∀ x y, D x y = D y x) (hD0 : ∀ x, D x x = 0)
    (hDd : ∀ x y, x ≠ y → |D x y - d x y| < μ / 2)
    {x y : X} (hxy : x ≠ y)
    (hmin : ∀ x' y', x' ≠ y' →
      ((Fintype.card X : ℝ) - 2) * D x y - ∑ z, D x z - ∑ z, D y z ≤
        ((Fintype.card X : ℝ) - 2) * D x' y' - ∑ z, D x' z - ∑ z, D y' z) :
    ∃ e, A e = {x, y}

Used by 2

Used byRobust cherry lemma for neighbor joining · Atteson's theorem: neighbor joining has ℓ∞ radius 1/2

Binary phylogenetic trees

TheoremRobust cherry lemma for neighbor joining#✓fully proved

The selection step of Atteson's theorem (Atteson 1999), with a proof after Mihaescu, Levy & Pachter (2009, Theorem 16). Let d be the path-length metric of a binary phylogenetic X-tree (G, ι) with positive edge lengths w and at least four taxa, and let μ be a lower bound on the lengths of the internal edges (edges with no taxon at either end). Let D be a symmetric dissimilarity with zero diagonal such that |D x y - d x y| < μ / 2 for all distinct taxa. If the distinct taxa x, y minimize the Q-criterion of D over all pairs of distinct singleton clusters at the start of neighbor joining, then ι x and ι y have a common neighbor: they form a cherry. The bound is sharp: with ≤ μ / 2 a non-cherry can tie (see the tests).

theorem exists_adj_adj_of_qCriterion_min_of_abs_sub_lt {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)
    {μ : ℝ} (hμ : ∀ a b, G.Adj a b → a ∉ Set.range ι → b ∉ Set.range ι → μ ≤ w s(a, b))
    {D : X → X → ℝ} (hDsymm : ∀ x y, D x y = D y x) (hD0 : ∀ x, D x x = 0)
    (hDd : ∀ x y, x ≠ y → |D x y - d x y| < μ / 2) (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 13 · 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 · Robust 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

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

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

Under the hypotheses of exists_adj_adj_of_qCriterion_min_of_abs_sub_lt, any pair of clusters that neighbor joining run on D may join from the initial singletons consists of two taxa with a common neighbor.

Cslib.Bioinformatics.Phylogenetics.NeighborJoining.NJRun.exists_adj_adj_of_join_init_of_abs_sub_lt · 15 lines

theorem NJRun.exists_adj_adj_of_join_init_of_abs_sub_lt {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)
    {μ : ℝ} (hμ : ∀ a b, G.Adj a b → a ∉ Set.range ι → b ∉ Set.range ι → μ ≤ w s(a, b))
    {D : X → X → ℝ} (hDsymm : ∀ x y, D x y = D y x) (hD0 : ∀ x, D x x = 0)
    (hDd : ∀ x y, x ≠ y → |D x y - d x y| < μ / 2)
    {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 usesRobust cherry lemma for neighbor joining

The whole run

TheoremNeighbor joining averages up to row shifts#✓fully proved

Along every run of neighbor joining on a symmetric dissimilarity d with zero diagonal there are weights α s (nonnegative, supported on s, summing to 1) and row terms κ s such that the cluster dissimilarity vanishes on the diagonal and D s t = ∑ x, ∑ y, α s x * α t y * d x y - κ s - κ t for distinct current clusters. Joining a, b takes α (a ∪ b) = (α a + α b) / 2 and κ (a ∪ b) = (κ a + κ b + D a b) / 2.

theorem NJRun.exists_avg {d : X → X → ℝ} (hsymm : ∀ x y, d x y = d y x)
    (h0 : ∀ x, d x x = 0) {S : Finset (Finset X)} {D : Finset X → Finset X → ℝ}
    {C : Finset (Finset X)} (hrun : NJRun d S D C) :
    ∃ (α : Finset X → X → ℝ) (κ : Finset X → ℝ),
      (∀ s ∈ S, ∀ x, 0 ≤ α s x) ∧ (∀ s ∈ S, ∀ x, x ∉ s → α s x = 0) ∧
      (∀ s ∈ S, ∑ x, α s x = 1) ∧ (∀ s ∈ S, D s s = 0) ∧
      ∀ s ∈ S, ∀ t ∈ S, s ≠ t → D s t = ∑ x, ∑ y, α s x * α t y * d x y - κ s - κ t

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 byAtteson's theorem: neighbor joining has ℓ∞ radius 1/2

TheoremThe shifting lemma#✓fully proved

The shifting lemma (Mihaescu, Levy & Pachter 2009, Lemma 4): if D' agrees with D on the diagonal of S and D' s t = D s t + f s + f t for distinct s, t ∈ S, then the Q-criterion of every pair of distinct clusters drops by the same amount 2 ∑_{c ∈ S} f c, so both have the same minimizing pairs.

theorem qCriterion_eq_sub_of_shift (S : Finset (Finset X)) {D D' : Finset X → Finset X → ℝ}
    (f : Finset X → ℝ) (hdiag : ∀ s ∈ S, D' s s = D s s)
    (hoff : ∀ s ∈ S, ∀ t ∈ S, s ≠ t → D' s t = D s t + f s + f t) {a b : Finset X}
    (ha : a ∈ S) (hb : b ∈ S) (hab : a ≠ b) :
    qCriterion S D' a b = qCriterion S D a b - 2 * ∑ c ∈ S, f c

Uses 1 · Used by 1

Statement usesNeighbor-joining Q-criterion

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

TheoremAtteson's theorem: neighbor joining has ℓ∞ radius 1/2#✓fully proved

Atteson's theorem: neighbor joining has ℓ∞ radius 1/2 (Atteson 1999). Let d be the path-length metric of a binary phylogenetic X-tree (G, ι) with positive edge lengths w, let μ be a lower bound on the lengths of its internal edges (edges with no taxon at either end), and let D be a symmetric dissimilarity with zero diagonal such that |D x y - d x y| < μ / 2 for all distinct taxa. 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: 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_of_abs_sub_lt {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)
    {μ : ℝ} (hμ : ∀ a b, G.Adj a b → a ∉ Set.range ι → b ∉ Set.range ι → μ ≤ w s(a, b))
    {D : X → X → ℝ} (hDsymm : ∀ x y, D x y = D y x) (hD0 : ∀ x, D x x = 0)
    (hDd : ∀ x y, x ≠ y → |D x y - d x y| < μ / 2)
    {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 ∨ 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

• Atteson (1999); stated as Theorem 2 of Mihaescu, Levy and Pachter (2009). NJRun uses the Studier–Keppler update. The proof was written for this formalization: up to row shifts, which do not change the pairs neighbor joining selects, the cluster dissimilarity of a run is an average of D (NJRun.exists_avg), so its errors against the tree metric of the current clusters stay below μ / 2, and the cherry step exists_eq_pair_of_qCriterion_min_of_abs_sub_lt applies at every join.

Uses 9 · Used by 1

Statement usesBinary phylogenetic tree · Runs of neighbor joining

Proof usesNeighbor joining averages up to row shifts · Robust cherry lemma for split systems · The path metric on a partition into sides · Neighbor joining forms the splits of a tree when every join forms a side · Neighbor-joining Q-criterion · The shifting lemma · Taxa on one side of a tree edge

Used byAtteson's radius for the scaled tree metric

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.