Splits, compatibility, ultrametrics and UPGMA

57 fully proved

Hierarchies

DefinitionHierarchy on a finite set#✓fully proved

A hierarchy on a finite set S: a family of nonempty subsets of S containing S and every singleton, any two members nested or disjoint. These are the cluster systems of the rooted phylogenetic trees on S (Semple & Steel 2003, Section 3.5).

def IsHierarchy (S : Finset α) (H : Finset (Finset α)) : Prop :=
  S ∈ H ∧ (∀ C ∈ H, C.Nonempty ∧ C ⊆ S) ∧ (∀ x ∈ S, {x} ∈ H) ∧
    ∀ C ∈ H, ∀ D ∈ H, C ⊆ D ∨ D ⊆ C ∨ Disjoint C D

Used by 4

Used byMetric of a dated rooted tree · A binary hierarchy is a hierarchy · Pairwise nested-or-disjoint clusters form a hierarchy · Ultrametrics are dated tree metrics

TheoremA binary hierarchy is a hierarchy#✓fully proved

A binary hierarchy is a hierarchy.

theorem IsBinaryHierarchy.isHierarchy {S : Finset α} {H : Finset (Finset α)}
    (h : IsBinaryHierarchy S H) : IsHierarchy S H

Uses 2

Statement usesHierarchy on a finite set · Binary hierarchy on a finite set

TheoremPairwise nested-or-disjoint clusters form a hierarchy#✓fully proved

Adding S and the singletons to a family of pairwise nested-or-disjoint nonempty subsets of a nonempty S gives a hierarchy.

theorem isHierarchy_completion {S : Finset α} (hS : S.Nonempty) {F : Finset (Finset α)}
    (hF : ∀ C ∈ F, C.Nonempty ∧ C ⊆ S)
    (hlam : ∀ C ∈ F, ∀ D ∈ F, C ⊆ D ∨ D ⊆ C ∨ Disjoint C D) :
    IsHierarchy S (insert S (F ∪ S.image ({·})))

Uses 1

Statement usesHierarchy on a finite set

TheoremHierarchies are refined by binary trees#✓fully proved

Every family of pairwise nested-or-disjoint nonempty subsets of a nonempty S is contained in a binary hierarchy on S, the cluster set of a rooted binary phylogenetic tree on S (Semple & Steel 2003, Proposition 3.5.2 and the refinement of a rooted tree to a binary one).

theorem exists_isBinaryHierarchy_superset {S : Finset α} (hS : S.Nonempty)
    {F : Finset (Finset α)} (hF : ∀ C ∈ F, C.Nonempty ∧ C ⊆ S)
    (hlam : ∀ C ∈ F, ∀ D ∈ F, C ⊆ D ∨ D ⊆ C ∨ Disjoint C D) :
    ∃ H, IsBinaryHierarchy S H ∧ F ⊆ H

Uses 1 · Used by 2

Statement usesBinary hierarchy on a finite set

Used byThe majority-rule consensus tree · Splits-equivalence theorem

TheoremNumber of members of a binary hierarchy#✓fully proved

A binary hierarchy on S has 2 |S| - 1 members: the |S| singletons and |S| - 1 internal clusters (stated without subtraction).

theorem IsBinaryHierarchy.card_add_one {S : Finset α} {H : Finset (Finset α)}
    (h : IsBinaryHierarchy S H) : H.card + 1 = 2 * S.card

Uses 2 · Used by 1

Statement usesBinary hierarchy on a finite set

Proof usesBinary hierarchy restricted below a member is a binary hierarchy

Used byMaximum of the Robinson–Foulds distance

Splits and compatibility

DefinitionCompatible splits#✓fully proved

The splits A | Aᶜ and B | Bᶜ are compatible: one of A ∩ B, A ∩ Bᶜ, Aᶜ ∩ B, Aᶜ ∩ Bᶜ is empty (Semple & Steel 2003, Section 3.1).

def Compatible (A B : Finset X) : Prop :=
  Disjoint A B ∨ Disjoint A Bᶜ ∨ Disjoint Aᶜ B ∨ Disjoint Aᶜ Bᶜ

Used by 9

Used byCompatibility is unchanged by complementing the first split · Compatibility is unchanged by complementing the second split · Compatible clusters are nested or disjoint · The four-gamete test · Edge splits of a tree are pairwise compatible · Splits computed from a leaf are pairwise compatible · Perfect phylogeny and the four-gamete condition · Splits-equivalence theorem · Symmetry of split compatibility

TheoremSymmetry of split compatibility#✓fully proved

Compatibility is symmetric.

theorem Compatible.symm {A B : Finset X} (h : Compatible A B) : Compatible B A

Uses 1 · Used by 1

Statement usesCompatible splits

Used byPerfect phylogeny and the four-gamete condition

TheoremCompatibility is unchanged by complementing the first split#✓fully proved

Compatibility depends only on the split, not on the side used to store it.

theorem compatible_compl_left {A B : Finset X} : Compatible Aᶜ B ↔ Compatible A B

Uses 1 · Used by 2

Statement usesCompatible splits

Used bySplits computed from a leaf are pairwise compatible · Splits-equivalence theorem

TheoremCompatibility is unchanged by complementing the second split#✓fully proved

Compatibility depends only on the split, not on the side used to store it.

theorem compatible_compl_right {A B : Finset X} : Compatible A Bᶜ ↔ Compatible A B

Uses 1 · Used by 2

Statement usesCompatible splits

Used bySplits computed from a leaf are pairwise compatible · Splits-equivalence theorem

TheoremCompatible clusters are nested or disjoint#✓fully proved

For the sides not containing a fixed taxon a, compatibility is being nested or disjoint: splits seen from a root are clusters.

theorem compatible_iff_nested_or_disjoint {a : X} {A B : Finset X} (hA : a ∉ A) (hB : a ∉ B) :
    Compatible A B ↔ A ⊆ B ∨ B ⊆ A ∨ Disjoint A B

Uses 1 · Used by 2

Statement usesCompatible splits

Used bySplits computed from a leaf are pairwise compatible · Splits-equivalence theorem

DefinitionFour-gamete condition for binary characters#✓fully proved

The binary characters χ and ψ show all four gametes (0,0), (0,1), (1,0), (1,1) on the taxa.

def FourGametes (χ ψ : X → Bool) : Prop :=
  ∀ b c : Bool, ∃ x, χ x = b ∧ ψ x = c

Used by 8

Used byThe sweep yields exactly \(R_m\) distinct breakpoints · Four-gamete condition for two sites · Sweep cuts form a valid breakpoint set · Hudson–Kaplan sweep yields disjoint four-gamete intervals · Intervals kept by the Hudson–Kaplan sweep are distinct · One step of the Hudson–Kaplan sweep · The four-gamete test · Perfect phylogeny and the four-gamete condition

DefinitionSplit of a binary character#✓fully proved

The split of a binary character: the taxa in state true.

def charSplit (χ : X → Bool) : Finset X :=
  Finset.univ.filter fun x => χ x = true

Used by 3

Used byThe four-gamete test · Perfect phylogeny and the four-gamete condition · Perfect phylogeny for a binary character matrix

TheoremThe four-gamete test#✓fully proved

Two binary characters give compatible splits iff they do not show all four gametes (Buneman 1971; Estabrook, Johnson & McMorris 1976).

theorem compatible_iff_not_fourGametes (χ ψ : X → Bool) :
    Compatible (charSplit χ) (charSplit ψ) ↔ ¬ FourGametes χ ψ

Uses 3 · Used by 1

Statement usesCompatible splits · Four-gamete condition for binary characters · Split of a binary character

Used byPerfect phylogeny and the four-gamete condition

Splits of unrooted binary trees

DefinitionSplit set of a tree computed from a leaf#✓fully proved

The split set of T computed from the leaf a: both sides of every cluster of T seen from a. It equals edgeSplits T for every a (splitSet_eq_edgeSplits).

noncomputable def splitSet (T : UnrootedBinaryTree X) (a : X) : Finset (Finset X) :=
  clusterSet T a ∪ (clusterSet T a).image (·ᶜ)

Uses 2 · Used by 9

Statement usesUnrooted binary phylogenetic tree · Cluster set of a tree seen from a leaf

Used byAll species give the whole tree · Edge splits of a tree are pairwise compatible · Splits computed from a leaf are pairwise compatible · An unrooted binary tree is determined by its quartets · Robinson–Foulds distance is independent of the base leaf · Split set from any leaf equals the edge splits · The split set does not depend on the leaf used to compute it · Splits-equivalence theorem · Robinson–Foulds distance as half the split symmetric difference

TheoremClusters seen from a leaf omit that leaf#✓fully proved

The clusters seen from a do not contain a.

theorem notMem_of_mem_clusterSet (T : UnrootedBinaryTree X) (a : X) {C : Finset X}
    (hC : C ∈ clusterSet T a) : a ∉ C

Uses 3 · Used by 4

Statement usesUnrooted binary phylogenetic tree · Cluster set of a tree seen from a leaf

Proof usesClusters of an unrooted tree form a binary hierarchy

Used byAll species give the whole tree · Splits computed from a leaf are pairwise compatible · An unrooted binary tree is determined by its quartets · Robinson–Foulds distance as half the split symmetric difference

DefinitionSide of a tree edge containing a vertex#✓fully proved

The side of the edge p – v containing v: the taxa whose leaf is closer to v than to p.

noncomputable def edgeSide (T : UnrootedBinaryTree X) (p v : T.V) : Finset X :=
  Finset.univ.filter fun x => T.G.dist (T.label x) v < T.G.dist (T.label x) p

Uses 1 · Used by 13

Statement usesUnrooted binary phylogenetic tree

Used byThe Branch Length Score · Branch length score of the empty set is zero · Branch length score is at most the tree length for nonnegative lengths · All species give the whole tree · Monotonicity · Branch length score is nonnegative for nonnegative edge lengths · A single species has BLS 0 · Subadditivity · The side of a pendant edge is the singleton of its leaf · Clusters seen from a leaf are edge sides · The two sides of a tree edge are complementary · Edge splits of a tree · Split set from any leaf equals the edge splits

DefinitionEdge splits of a tree#✓fully proved

The edge splits of T: the sides of all its edges (both sides of every edge).

noncomputable def edgeSplits (T : UnrootedBinaryTree X) : Finset (Finset X) :=
  ((Finset.univ ×ˢ Finset.univ).filter fun e : T.V × T.V => T.G.Adj e.1 e.2).image
    fun e => edgeSide T e.1 e.2

Uses 2 · Used by 9

Statement usesSide of a tree edge containing a vertex · Unrooted binary phylogenetic tree

Used byAll species give the whole tree · Edge splits of a tree are pairwise compatible · Tree displaying a quartet · Perfect phylogeny and the four-gamete condition · Perfect phylogeny for a binary character matrix · An unrooted binary tree is determined by its quartets · Split set from any leaf equals the edge splits · The split set does not depend on the leaf used to compute it · Splits-equivalence theorem

TheoremThe two sides of a tree edge are complementary#✓fully proved

The two sides of an edge are complementary.

theorem compl_edgeSide (T : UnrootedBinaryTree X) {p v : T.V} (hpv : T.G.Adj p v) :
    (edgeSide T p v)ᶜ = edgeSide T v p

Uses 2 · Used by 2

Statement usesSide of a tree edge containing a vertex · Unrooted binary phylogenetic tree

Used byAll species give the whole tree · Split set from any leaf equals the edge splits

TheoremClusters seen from a leaf are edge sides#✓fully proved

The cluster of a vertex v seen from a is the side of v of the edge from v to its neighbor p toward a.

theorem cluster_eq_edgeSide (T : UnrootedBinaryTree X) (a : X) {p v : T.V} (hpv : T.G.Adj p v)
    (hd : T.G.dist (T.label a) v = T.G.dist (T.label a) p + 1) :
    cluster T a v = edgeSide T p v

Uses 4 · Used by 1

Statement usesSide of a tree edge containing a vertex · Unrooted binary phylogenetic tree · Cluster of a vertex seen from a leaf

Proof usesConcatenation of paths meeting at one endpoint is a path

Used bySplit set from any leaf equals the edge splits

TheoremSplit set from any leaf equals the edge splits#✓fully proved

The split set computed from any leaf is the set of edge splits.

theorem splitSet_eq_edgeSplits (T : UnrootedBinaryTree X) (a : X) :
    splitSet T a = edgeSplits T

Uses 8 · Used by 5

Statement usesEdge splits of a tree · Split set of a tree computed from a leaf · Unrooted binary phylogenetic tree

Proof usesClusters seen from a leaf are edge sides · The two sides of a tree edge are complementary · Side of a tree edge containing a vertex · Cluster of a vertex seen from a leaf · Parent vertex towards a root in a connected graph

Used byAll species give the whole tree · Edge splits of a tree are pairwise compatible · An unrooted binary tree is determined by its quartets · The split set does not depend on the leaf used to compute it · Splits-equivalence theorem

TheoremThe split set does not depend on the leaf used to compute it#✓fully proved

The split set does not depend on the leaf used to compute it.

theorem splitSet_eq_splitSet (T : UnrootedBinaryTree X) (a b : X) :
    splitSet T a = splitSet T b

Uses 4 · Used by 1

Statement usesSplit set of a tree computed from a leaf · Unrooted binary phylogenetic tree

Proof usesEdge splits of a tree · Split set from any leaf equals the edge splits

Used byRobinson–Foulds distance is independent of the base leaf

TheoremSplits computed from a leaf are pairwise compatible#✓fully proved

Any two splits of one tree are compatible.

theorem compatible_of_mem_splitSet {T : UnrootedBinaryTree X} {a : X} {A B : Finset X}
    (hA : A ∈ splitSet T a) (hB : B ∈ splitSet T a) : Compatible A B

Uses 9 · Used by 2

Statement usesCompatible splits · Split set of a tree computed from a leaf · Unrooted binary phylogenetic tree

Proof usesCompatibility is unchanged by complementing the first split · Compatibility is unchanged by complementing the second split · Compatible clusters are nested or disjoint · Clusters seen from a leaf omit that leaf · Cluster set of a tree seen from a leaf · Clusters of an unrooted tree form a binary hierarchy

Used byEdge splits of a tree are pairwise compatible · Splits-equivalence theorem

TheoremEdge splits of a tree are pairwise compatible#✓fully proved

Any two splits of one tree are compatible.

theorem compatible_of_mem_edgeSplits {T : UnrootedBinaryTree X} {A B : Finset X}
    (hA : A ∈ edgeSplits T) (hB : B ∈ edgeSplits T) : Compatible A B

Uses 6 · Used by 1

Statement usesCompatible splits · Edge splits of a tree · Unrooted binary phylogenetic tree

Proof usesSplits computed from a leaf are pairwise compatible · Split set of a tree computed from a leaf · Split set from any leaf equals the edge splits

Used byPerfect phylogeny and the four-gamete condition

TheoremSplits-equivalence theorem#✓fully proved

Splits-equivalence theorem, binary form (Buneman 1971; Semple & Steel 2003, Theorem 3.1.4): on at least two taxa, a family F of proper splits (both sides nonempty) is contained in the split set of some unrooted binary phylogenetic tree iff its members are pairwise compatible. The tree is a binary refinement of the tree whose splits are exactly F and the trivial ones.

theorem splits_equivalence (hX : 1 < Fintype.card X) (F : Finset (Finset X))
    (hne : ∀ A ∈ F, A.Nonempty ∧ Aᶜ.Nonempty) :
    (∃ T : UnrootedBinaryTree X, F ⊆ edgeSplits T) ↔
      ∀ A ∈ F, ∀ B ∈ F, Compatible A B

Uses 13 · Used by 1

Statement usesCompatible splits · Edge splits of a tree · Unrooted binary phylogenetic tree

Proof usesCompatibility is unchanged by complementing the first split · Compatibility is unchanged by complementing the second split · Compatible clusters are nested or disjoint · Splits computed from a leaf are pairwise compatible · Hierarchies are refined by binary trees · Split set of a tree computed from a leaf · Split set from any leaf equals the edge splits · Binary hierarchy on a finite set · Cluster set of a tree seen from a leaf · Every binary hierarchy is a cluster set of a tree

Used byPerfect phylogeny and the four-gamete condition

DefinitionPerfect phylogeny for a binary character matrix#✓fully proved

T is a perfect phylogeny for the binary character matrix M (taxa by characters): the split of every non-constant column is a split of T, i.e. every character changes state on exactly one edge.

def IsPerfectPhylogeny {ι : Type} (T : UnrootedBinaryTree X) (M : X → ι → Bool) : Prop :=
  ∀ j, charSplit (M · j) = ∅ ∨ charSplit (M · j) = Finset.univ ∨
    charSplit (M · j) ∈ edgeSplits T

Uses 3 · Used by 1

Statement usesSplit of a binary character · Edge splits of a tree · Unrooted binary phylogenetic tree

Used byPerfect phylogeny and the four-gamete condition

TheoremPerfect phylogeny and the four-gamete condition#✓fully proved

Perfect phylogeny and the four-gamete condition (Estabrook, Johnson & McMorris 1976; Gusfield 1991): a binary character matrix on at least two taxa has a perfect phylogeny iff no two of its columns show all four gametes.

theorem exists_perfectPhylogeny_iff {ι : Type} (hX : 1 < Fintype.card X) (M : X → ι → Bool) :
    (∃ T : UnrootedBinaryTree X, IsPerfectPhylogeny T M) ↔
      ∀ j k, ¬ FourGametes (M · j) (M · k)

Uses 10

Statement usesFour-gamete condition for binary characters · Perfect phylogeny for a binary character matrix · Unrooted binary phylogenetic tree

Proof usesCompatible splits · Symmetry of split compatibility · Split of a binary character · The four-gamete test · Edge splits of a tree are pairwise compatible · Edge splits of a tree · Splits-equivalence theorem

The Robinson–Foulds distance

DefinitionRobinson–Foulds distance#✓fully proved

The Robinson–Foulds distance: the number of splits in exactly one of the two trees. Each split is counted once, by its side away from the leaf a (its cluster seen from a); trivial splits are common to all trees and cancel. The value does not depend on a (rfDist_eq_rfDist).

noncomputable def rfDist (a : X) (T T' : UnrootedBinaryTree X) : ℕ :=
  (clusterSet T a ∆ clusterSet T' a).card

Uses 2 · Used by 8

Statement usesUnrooted binary phylogenetic tree · Cluster set of a tree seen from a leaf

Used bySymmetry of the Robinson–Foulds distance · Isomorphism invariance of the Robinson–Foulds distance · Robinson–Foulds distance is independent of the base leaf · Robinson–Foulds distance vanishes exactly on isomorphic trees · Maximum of the Robinson–Foulds distance · Robinson–Foulds distance from a tree to itself is zero · Triangle inequality for the Robinson–Foulds distance · Robinson–Foulds distance as half the split symmetric difference

TheoremRobinson–Foulds distance as half the split symmetric difference#✓fully proved

Each split is counted twice in the symmetric difference of the split sets (once per side), so the Robinson–Foulds distance is half of it.

theorem two_mul_rfDist (a : X) (T T' : UnrootedBinaryTree X) :
    2 * rfDist a T T' = (splitSet T a ∆ splitSet T' a).card

Uses 5 · Used by 1

Statement usesRobinson–Foulds distance · Split set of a tree computed from a leaf · Unrooted binary phylogenetic tree

Proof usesClusters seen from a leaf omit that leaf · Cluster set of a tree seen from a leaf

Used byRobinson–Foulds distance is independent of the base leaf

TheoremRobinson–Foulds distance is independent of the base leaf#✓fully proved

The Robinson–Foulds distance does not depend on the leaf used to compute it.

theorem rfDist_eq_rfDist (a b : X) (T T' : UnrootedBinaryTree X) :
    rfDist a T T' = rfDist b T T'

Uses 5

Statement usesRobinson–Foulds distance · Unrooted binary phylogenetic tree

Proof usesSplit set of a tree computed from a leaf · The split set does not depend on the leaf used to compute it · Robinson–Foulds distance as half the split symmetric difference

TheoremRobinson–Foulds distance from a tree to itself is zero#✓fully proved

The Robinson–Foulds distance from a tree to itself is zero.

theorem rfDist_self (a : X) (T : UnrootedBinaryTree X) : rfDist a T T = 0

Uses 3

Statement usesRobinson–Foulds distance · Unrooted binary phylogenetic tree

Proof usesCluster set of a tree seen from a leaf

TheoremSymmetry of the Robinson–Foulds distance#✓fully proved

The Robinson–Foulds distance is symmetric.

theorem rfDist_comm (a : X) (T T' : UnrootedBinaryTree X) : rfDist a T T' = rfDist a T' T

Uses 3

Statement usesRobinson–Foulds distance · Unrooted binary phylogenetic tree

Proof usesCluster set of a tree seen from a leaf

TheoremTriangle inequality for the Robinson–Foulds distance#✓fully proved

The Robinson–Foulds distance satisfies the triangle inequality.

theorem rfDist_triangle (a : X) (T₁ T₂ T₃ : UnrootedBinaryTree X) :
    rfDist a T₁ T₃ ≤ rfDist a T₁ T₂ + rfDist a T₂ T₃

Uses 3

Statement usesRobinson–Foulds distance · Unrooted binary phylogenetic tree

Proof usesCluster set of a tree seen from a leaf

TheoremRobinson–Foulds distance vanishes exactly on isomorphic trees#✓fully proved

The Robinson–Foulds distance vanishes exactly on isomorphic trees (Robinson & Foulds 1981).

theorem rfDist_eq_zero_iff (a : X) (T T' : UnrootedBinaryTree X) :
    rfDist a T T' = 0 ↔ T.Iso T'

Uses 6

Statement usesRobinson–Foulds distance · Unrooted binary phylogenetic tree · Isomorphism of unrooted binary phylogenetic trees

Proof usesCluster set of a tree seen from a leaf · Isomorphic trees have the same clusters · Clusters determine an unrooted binary tree

TheoremIsomorphism invariance of the Robinson–Foulds distance#✓fully proved

The Robinson–Foulds distance is invariant under isomorphism, so it is a metric on the trees up to isomorphism.

theorem rfDist_congr {a : X} {T₁ T₂ T' : UnrootedBinaryTree X} (h : T₁.Iso T₂) :
    rfDist a T₁ T' = rfDist a T₂ T'

Uses 5

Statement usesRobinson–Foulds distance · Unrooted binary phylogenetic tree · Isomorphism of unrooted binary phylogenetic trees

Proof usesCluster set of a tree seen from a leaf · Isomorphic trees have the same clusters

TheoremMaximum of the Robinson–Foulds distance#✓fully proved

On n ≥ 3 taxa it is at most 2 (n - 3), the number of nontrivial splits of two binary trees (Robinson & Foulds 1981).

theorem rfDist_le (a : X) (hn : 3 ≤ Fintype.card X) (T T' : UnrootedBinaryTree X) :
    rfDist a T T' ≤ 2 * (Fintype.card X - 3)

Uses 6

Statement usesRobinson–Foulds distance · Unrooted binary phylogenetic tree

Proof usesNumber of members of a binary hierarchy · Binary hierarchy on a finite set · Cluster set of a tree seen from a leaf · Clusters of an unrooted tree form a binary hierarchy

Majority-rule consensus and bootstrap support

DefinitionMajority splits of a family of trees#✓fully proved

The majority splits of a finite family of trees T i: the clusters, seen from a, of more than half of the trees (repetitions in the family count).

noncomputable def majoritySplits {ι : Type} [Fintype ι] (T : ι → UnrootedBinaryTree X) (a : X) :
    Finset (Finset X) :=
  Finset.univ.filter fun A =>
    Fintype.card ι < 2 * (Finset.univ.filter fun i => A ∈ clusterSet (T i) a).card

Uses 2 · Used by 3

Statement usesUnrooted binary phylogenetic tree · Cluster set of a tree seen from a leaf

Used byThe majority-rule consensus tree · Majority splits are compatible · Bootstrap support above one half means a majority split

TheoremMajority splits are compatible#✓fully proved

Majority splits are compatible (Margush & McMorris 1981): two clusters each in more than half of the trees are both clusters of a common tree (pigeonhole), hence nested or disjoint.

theorem nested_or_disjoint_of_mem_majoritySplits {ι : Type} [Fintype ι]
    {T : ι → UnrootedBinaryTree X} {a : X} {A B : Finset X} (hA : A ∈ majoritySplits T a)
    (hB : B ∈ majoritySplits T a) : A ⊆ B ∨ B ⊆ A ∨ Disjoint A B

Uses 4 · Used by 1

Statement usesMajority splits of a family of trees · Unrooted binary phylogenetic tree

Proof usesCluster set of a tree seen from a leaf · Clusters of an unrooted tree form a binary hierarchy

Used byThe majority-rule consensus tree

TheoremThe majority-rule consensus tree#✓fully proved

The majority splits are clusters of one unrooted binary phylogenetic tree (a binary refinement of the majority-rule consensus tree).

theorem exists_tree_majoritySplits_subset {ι : Type} [Fintype ι]
    (T : ι → UnrootedBinaryTree X) (a : X) (hX : (Finset.univ.erase a).Nonempty) :
    ∃ T₀ : UnrootedBinaryTree X, majoritySplits T a ⊆ clusterSet T₀ a

Uses 8

Statement usesMajority splits of a family of trees · Unrooted binary phylogenetic tree · Cluster set of a tree seen from a leaf

Proof usesHierarchies are refined by binary trees · Majority splits are compatible · Binary hierarchy on a finite set · Every binary hierarchy is a cluster set of a tree · Clusters of an unrooted tree form a binary hierarchy

DefinitionBootstrap support#✓fully proved

Bootstrap support (Felsenstein 1985) of the split with side A away from a, for a tree estimator est and an alignment M of m sites: the fraction of the m ^ m site resamplings with replacement w : Fin m → Fin m (uniform draws, whose site counts are multinomial) for which the tree estimated from the resampled alignment M ∘ w has the cluster A. This is the exact bootstrap proportion; Felsenstein's procedure estimates it from a sample of resamplings.

noncomputable def bootstrapSupport {σ : Type} {m : ℕ}
    (est : (Fin m → X → σ) → UnrootedBinaryTree X) (a : X) (M : Fin m → X → σ)
    (A : Finset X) : ℝ :=
  ((Finset.univ.filter fun w : Fin m → Fin m => A ∈ clusterSet (est (M ∘ w)) a).card : ℝ) /
    ((m ^ m : ℕ) : ℝ)

Uses 2 · Used by 2

Statement usesUnrooted binary phylogenetic tree · Cluster set of a tree seen from a leaf

Used byBootstrap support lies in the unit interval · Bootstrap support above one half means a majority split

TheoremBootstrap support lies in the unit interval#✓fully proved

Bootstrap support is a frequency: it lies in [0, 1].

theorem bootstrapSupport_mem_Icc {σ : Type} {m : ℕ}
    (est : (Fin m → X → σ) → UnrootedBinaryTree X) (a : X) (M : Fin m → X → σ)
    (A : Finset X) : bootstrapSupport est a M A ∈ Set.Icc 0 1

Uses 3

Statement usesBootstrap support · Unrooted binary phylogenetic tree

Proof usesCluster set of a tree seen from a leaf

TheoremBootstrap support above one half means a majority split#✓fully proved

A split has bootstrap support above one half iff it is a majority split of the bootstrap replicate trees; so the splits with support above one half are pairwise compatible and form one tree (exists_tree_majoritySplits_subset).

theorem one_half_lt_bootstrapSupport_iff {σ : Type} {m : ℕ}
    (est : (Fin m → X → σ) → UnrootedBinaryTree X) (a : X) (M : Fin m → X → σ)
    (A : Finset X) :
    1 / 2 < bootstrapSupport est a M A ↔ A ∈ majoritySplits (fun w => est (M ∘ w)) a

Uses 4

Statement usesBootstrap support · Majority splits of a family of trees · Unrooted binary phylogenetic tree

Proof usesCluster set of a tree seen from a leaf

Ultrametrics and UPGMA

StructureUltrametric on taxa#✓fully proved

d is an ultrametric on the taxa: symmetric, zero exactly on the diagonal, and satisfying the three-point condition d x z ≤ max (d x y) (d y z) (equivalently, of the three distances among any three taxa the two largest are equal).

structure IsUltrametric (d : X → X → ℝ) : Prop where
  /-- Symmetry. -/
  symm : ∀ x y, d x y = d y x
  /-- Zero on the diagonal. -/
  self : ∀ x, d x x = 0
  /-- Positive off the diagonal. -/
  pos : ∀ x y, x ≠ y → 0 < d x y
  /-- The three-point condition. -/
  three_point : ∀ x y z, d x z ≤ max (d x y) (d y z)

Used by 4

Used byUltrametrics satisfy the four-point condition · Every ultrametric is a tree metric · Ultrametrics are dated tree metrics · UPGMA is exact on ultrametrics

DefinitionMetric of a dated rooted tree#✓fully proved

d is the metric of a dated rooted tree, encoded by its clusters: a hierarchy H on the taxa with dates h (0 at the leaves, strictly increasing from a cluster to any cluster strictly containing it) such that d x y is the date of the smallest cluster containing x and y (their most recent common ancestor). With edge lengths (h D - h C) / 2 from each cluster C to its parent D, d x y is the path length from x to y and all leaves are equidistant from the root (Semple & Steel 2003, Section 7.2).

def IsDatedTreeMetric (d : X → X → ℝ) : Prop :=
  ∃ (H : Finset (Finset X)) (h : Finset X → ℝ), IsHierarchy Finset.univ H ∧
    (∀ x, h {x} = 0) ∧ (∀ C ∈ H, ∀ D ∈ H, C ⊂ D → h C < h D) ∧
    ∀ x y, ∃ C ∈ H, x ∈ C ∧ y ∈ C ∧ d x y = h C ∧ ∀ D ∈ H, x ∈ D → y ∈ D → C ⊆ D

Uses 1 · Used by 1

Statement usesHierarchy on a finite set

Used byUltrametrics are dated tree metrics

TheoremUltrametrics satisfy the four-point condition#✓fully proved

Ultrametrics satisfy the four-point condition (Semple & Steel 2003, Section 7.2), so every ultrametric on a finite set is a tree metric (IsUltrametric.isTreeMetric).

theorem IsUltrametric.fourPointCondition {d : X → X → ℝ} (hd : IsUltrametric d) :
    MathlibExt.Biology.Phylogenetics.Buneman.FourPointCondition d

Uses 2 · Used by 1

Statement usesUltrametric on taxa · Four-point condition

Used byEvery ultrametric is a tree metric

TheoremEvery ultrametric is a tree metric#✓fully proved

Every ultrametric on a finite set is a tree metric (via Buneman's four-point theorem).

theorem IsUltrametric.isTreeMetric [Finite X] {d : X → X → ℝ} (hd : IsUltrametric d) :
    MathlibExt.Biology.Phylogenetics.Buneman.IsTreeMetric d

Uses 4

Statement usesUltrametric on taxa · Tree metric

Proof usesUltrametrics satisfy the four-point condition · Buneman's theorem, converse direction

TheoremUltrametrics are dated tree metrics#✓fully proved

Ultrametrics are dated tree metrics (Semple & Steel 2003, Theorem 7.2.5): on a nonempty finite set of taxa, a dissimilarity satisfies the three-point condition (and is a metric) iff it is the metric of a dated rooted tree.

theorem isUltrametric_iff_isDatedTreeMetric [Nonempty X] (d : X → X → ℝ) :
    IsUltrametric d ↔ IsDatedTreeMetric d

Uses 3

Statement usesMetric of a dated rooted tree · Ultrametric on taxa

Proof usesHierarchy on a finite set

DefinitionAverage linkage between clusters#✓fully proved

The average linkage between two clusters: the mean of d x y over x ∈ C, y ∈ D.

noncomputable def avgDist (d : X → X → ℝ) (C D : Finset X) : ℝ :=
  (∑ x ∈ C, ∑ y ∈ D, d x y) / (C.card * D.card : ℝ)

Used by 3

Used byUPGMA always completes · UPGMA is exact on ultrametrics · States reachable by UPGMA

InductiveStates reachable by UPGMA#✓fully proved

The states reachable by UPGMA (Sokal & Michener 1958) on d: a partition P of the taxa into blocks and the heights c x y recorded so far. It starts from the singletons; each step merges two distinct blocks C, D of least average linkage (ties broken arbitrarily) and records avgDist d C D as the height at which every x ∈ C and y ∈ D are joined (the distance between them in the output tree; their common ancestor sits at half of it).

inductive UpgmaReaches (d : X → X → ℝ) : Finset (Finset X) → (X → X → ℝ) → Prop
  | init : UpgmaReaches d (Finset.univ.image ({·})) fun _ _ => 0
  | step {P : Finset (Finset X)} {c : X → X → ℝ} {C D : Finset X} :
      UpgmaReaches d P c → C ∈ P → D ∈ P → C ≠ D →
      (∀ E ∈ P, ∀ F ∈ P, E ≠ F → avgDist d C D ≤ avgDist d E F) →
      UpgmaReaches d (insert (C ∪ D) ((P.erase C).erase D))
        fun x y => if (x ∈ C ∧ y ∈ D) ∨ (x ∈ D ∧ y ∈ C) then avgDist d C D else c x y

Uses 1 · Used by 2

Statement usesAverage linkage between clusters

Used byUPGMA always completes · UPGMA is exact on ultrametrics

TheoremUPGMA is exact on ultrametrics#✓fully proved

In every UPGMA run on an ultrametric, the recorded height of two taxa in the same block is their distance. In particular a completed run (one block) reconstructs d, i.e. the dated tree, exactly (Semple & Steel 2003, Section 7.2).

theorem upgma_exact {d : X → X → ℝ} (hd : IsUltrametric d) {P : Finset (Finset X)}
    {c : X → X → ℝ} (h : UpgmaReaches d P c) {B : Finset X} (hB : B ∈ P) {x y : X}
    (hx : x ∈ B) (hy : y ∈ B) : c x y = d x y

Uses 3

Statement usesUltrametric on taxa · States reachable by UPGMA

Proof usesAverage linkage between clusters

TheoremUPGMA always completes#✓fully proved

UPGMA always completes: from the singletons it reaches the single block univ.

theorem exists_upgmaReaches_univ [Nonempty X] (d : X → X → ℝ) :
    ∃ c, UpgmaReaches d {Finset.univ} c

Uses 2

Statement usesStates reachable by UPGMA

Proof usesAverage linkage between clusters

Rooted triplets, quartets and BUILD

StructureRooted triplet#✓fully proved

A rooted triplet xy|z: x and y are closer to each other than to z.

structure Triplet (α : Type*) where
  /-- The first taxon of the cherry. -/
  x : α
  /-- The second taxon of the cherry. -/
  y : α
  /-- The outgroup. -/
  z : α

Used by 5

Used byCorrectness of BUILD · Cluster system displaying a triplet · A rooted binary tree is determined by its triplets · Cut in the Aho graph · An unrooted binary tree is determined by its quartets

DefinitionCluster system displaying a triplet#✓fully proved

The cluster system H displays the triplet xy|z: some cluster contains x and y but not z.

def DisplaysTriplet (H : Finset (Finset α)) (t : Triplet α) : Prop :=
  ∃ C ∈ H, t.x ∈ C ∧ t.y ∈ C ∧ t.z ∉ C

Uses 1 · Used by 3

Statement usesRooted triplet

Used byCorrectness of BUILD · A rooted binary tree is determined by its triplets · An unrooted binary tree is determined by its quartets

DefinitionCut in the Aho graph#✓fully proved

The Aho graph of the triplets R on S' (vertices S', an edge x y for each xy|z ∈ R with x, y, z ∈ S') has a cut: a partition of S' into two nonempty parts with no edge across, i.e. the graph is disconnected.

def HasAhoCut (R : Finset (Triplet α)) (S' : Finset α) : Prop :=
  ∃ K ⊆ S', K.Nonempty ∧ (S' \ K).Nonempty ∧
    ∀ t ∈ R, t.x ∈ S' → t.y ∈ S' → t.z ∈ S' → (t.x ∈ K ↔ t.y ∈ K)

Uses 1 · Used by 1

Statement usesRooted triplet

Used byCorrectness of BUILD

TheoremA rooted binary tree is determined by its triplets#✓fully proved

A rooted binary tree is determined by its triplets (Semple & Steel 2003, Theorem 6.4.1): two binary hierarchies on S displaying the same triplets are equal.

theorem eq_of_displaysTriplet_iff {S : Finset α} {H H' : Finset (Finset α)}
    (hH : IsBinaryHierarchy S H) (hH' : IsBinaryHierarchy S H')
    (h : ∀ t : Triplet α, DisplaysTriplet H t ↔ DisplaysTriplet H' t) : H = H'

Uses 3 · Used by 1

Statement usesCluster system displaying a triplet · Rooted triplet · Binary hierarchy on a finite set

Used byAn unrooted binary tree is determined by its quartets

TheoremCorrectness of BUILD#✓fully proved

Correctness of BUILD (Aho, Sagiv, Szymanski & Ullman 1981; Semple & Steel 2003, Section 6.4): a set R of triplets on a nonempty S, none of the degenerate form xx|x (which no tree displays and no cut detects), is displayed by a rooted binary phylogenetic tree on S iff for every subset S' of at least two taxa the Aho graph of R on S' is disconnected. BUILD splits along the components and recurses; the converse direction builds the tree this way, splitting along any cut.

theorem build_spec {S : Finset α} (hS : S.Nonempty) (R : Finset (Triplet α))
    (hR : ∀ t ∈ R, t.x ∈ S ∧ t.y ∈ S ∧ t.z ∈ S ∧ (t.z ≠ t.x ∨ t.z ≠ t.y)) :
    (∃ H, IsBinaryHierarchy S H ∧ ∀ t ∈ R, DisplaysTriplet H t) ↔
      ∀ S' ⊆ S, 2 ≤ S'.card → HasAhoCut R S'

Uses 4

Statement usesCluster system displaying a triplet · Cut in the Aho graph · Rooted triplet · Binary hierarchy on a finite set

DefinitionTree displaying a quartet#✓fully proved

T displays the quartet xy|zw: some edge split of T has x, y on one side and z, w on the other.

def DisplaysQuartet (T : UnrootedBinaryTree X) (x y z w : X) : Prop :=
  ∃ A ∈ edgeSplits T, x ∈ A ∧ y ∈ A ∧ z ∉ A ∧ w ∉ A

Uses 2 · Used by 1

Statement usesEdge splits of a tree · Unrooted binary phylogenetic tree

Used byAn unrooted binary tree is determined by its quartets

TheoremAn unrooted binary tree is determined by its quartets#✓fully proved

An unrooted binary tree is determined by its quartets (Semple & Steel 2003, Corollary 6.3.8): two trees displaying the same quartets are isomorphic. Already the quartets containing the taxon a suffice; they are the rooted triplets seen from a.

theorem iso_of_displaysQuartet_iff {T T' : UnrootedBinaryTree X} (a : X)
    (h : ∀ x y z, DisplaysQuartet T x y z a ↔ DisplaysQuartet T' x y z a) : T.Iso T'

Uses 13

Statement usesTree displaying a quartet · Unrooted binary phylogenetic tree · Isomorphism of unrooted binary phylogenetic trees

Proof usesCluster system displaying a triplet · Rooted triplet · Edge splits of a tree · A rooted binary tree is determined by its triplets · Clusters seen from a leaf omit that leaf · Split set of a tree computed from a leaf · Split set from any leaf equals the edge splits · Cluster set of a tree seen from a leaf · Clusters of an unrooted tree form a binary hierarchy · Clusters determine an unrooted binary tree

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.