Tree metrics and the four-point condition

DefinitionTree metric#✓fully proved

d is a tree metric: there are a finite tree G on a vertex type V, positive edge lengths w, and a placement ι of the taxa on vertices such that d x y is the total length of the (unique) path from ι x to ι y.

def IsTreeMetric {X : Type*} (d : X → X → ℝ) : Prop :=
  ∃ (V : Type) (_ : Fintype V) (G : SimpleGraph V) (_ : G.IsTree) (w : Sym2 V → ℝ)
    (ι : X → V), (∀ e ∈ G.edgeSet, 0 < w e) ∧
      ∀ x y (p : G.Walk (ι x) (ι y)), p.IsPath → d x y = (p.edges.map w).sum

Used by 4

Used byEvery ultrametric is a tree metric · Tree metrics satisfy the four-point condition · Buneman's four-point theorem · Buneman's theorem, converse direction

DefinitionFour-point condition#✓fully proved

The four-point condition: d x y + d z t ≤ max (d x z + d y t) (d x t + d y z).

def FourPointCondition {X : Type*} (d : X → X → ℝ) : Prop :=
  ∀ x y z t, d x y + d z t ≤ max (d x z + d y t) (d x t + d y z)

Used by 4

Used byUltrametrics satisfy the four-point condition · Tree metrics satisfy the four-point condition · Buneman's four-point theorem · Buneman's theorem, converse direction

TheoremTree metrics satisfy the four-point condition#✓fully proved

Tree metrics satisfy the four-point condition (the easy direction of Buneman's theorem).

theorem IsTreeMetric.fourPointCondition {X : Type*} {d : X → X → ℝ} (h : IsTreeMetric d) :
    FourPointCondition d

Sources

• Buneman (1974); Semple & Steel (2003), Theorem 7.2.6.

Uses 3 · Used by 1

Statement usesFour-point condition · Tree metric

Proof usesConcatenation of paths meeting at one endpoint is a path

Used byBuneman's four-point theorem

TheoremBuneman's theorem, converse direction#✓fully proved

A symmetric dissimilarity on a finite set that vanishes on the diagonal and satisfies the four-point condition is a tree metric.

theorem isTreeMetric_of_fourPointCondition {X : Type*} [Finite X] (d : X → X → ℝ)
    (hdiag : ∀ x, d x x = 0) (hsymm : ∀ x y, d x y = d y x) (h : FourPointCondition d) :
    IsTreeMetric d

Sources

• Buneman (1974); Semple & Steel (2003), Theorem 7.2.6.

Uses 2 · Used by 2

Statement usesFour-point condition · Tree metric

Used byEvery ultrametric is a tree metric · Buneman's four-point theorem

TheoremBuneman's four-point theorem#✓fully proved

A symmetric dissimilarity on a finite set that vanishes on the diagonal is a tree metric if and only if it satisfies the four-point condition.

theorem isTreeMetric_iff_fourPointCondition {X : Type*} [Finite X] (d : X → X → ℝ)
    (hdiag : ∀ x, d x x = 0) (hsymm : ∀ x y, d x y = d y x) :
    IsTreeMetric d ↔ FourPointCondition d

Sources

• Buneman (1974); Semple & Steel (2003), Theorem 7.2.6.

Uses 4

Statement usesFour-point condition · Tree metric

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

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.