Pauplin's formula and balanced minimum evolution

14 fully proved

Balanced Minimum Evolution

InductiveRooted binary tree with edge lengths#✓fully proved

A rooted binary tree with leaf labels in X; node a l b r has the child l at the end of an edge of length a and the child r at the end of an edge of length b.

inductive RTree (X : Type u) where
  /-- A leaf with label `x`. -/
  | leaf : X → RTree X
  /-- An internal vertex with children `l` and `r` on edges of lengths `a` and `b`. -/
  | node : ℝ → RTree X → ℝ → RTree X → RTree X

Used by 10

Used byPauplin's formula · Kraft's equality · Kraft equality · Leaf labels of an unrooted binary tree · Leaves of a rooted binary tree with root distances · Total edge length of a rooted binary tree · Total edge length of an unrooted binary tree · Leaf pairs of a rooted binary tree with path lengths · Leaf pairs of an unrooted binary tree with path lengths · Unrooted binary tree with edge lengths

StructureUnrooted binary tree with edge lengths#✓fully proved

An unrooted binary tree, rooted at its edge of length len that joins the roots of the rooted binary trees left and right.

structure UTree (X : Type u) where
  /-- The subtree on one side of the root edge. -/
  left : RTree X
  /-- The length of the root edge. -/
  len : ℝ
  /-- The subtree on the other side of the root edge. -/
  right : RTree X

Uses 1 · Used by 7

Statement usesRooted binary tree with edge lengths

Used byBalanced minimum-evolution length · The balanced minimum-evolution length of a tree metric is the tree length · Pauplin's formula · Kraft equality · Leaf labels of an unrooted binary tree · Total edge length of an unrooted binary tree · Leaf pairs of an unrooted binary tree with path lengths

DefinitionPauplin coefficient of a pair of leaves#✓fully proved

The Pauplin coefficient 2 ^ (1 - τ) of a pair of leaves at topological distance τ.

noncomputable def pauplinCoeff (τ : ℕ) : ℝ :=
  2 / 2 ^ τ

Used by 4

Used byBalanced minimum-evolution length · The balanced minimum-evolution length of a tree metric is the tree length · Pauplin's formula · Kraft equality

Rooted binary trees

DefinitionTotal edge length of a rooted binary tree#✓fully proved

The total length of the edges.

def length : RTree X → ℝ
  | leaf _ => 0
  | node a l b r => a + length l + b + length r

Uses 1 · Used by 2

Statement usesRooted binary tree with edge lengths

Used byPauplin's formula · Total edge length of an unrooted binary tree

DefinitionLeaves of a rooted binary tree with root distances#✓fully proved

The leaves, each with its label, its distance to the root and its number of edges to the root.

def leaves : RTree X → List (X × ℝ × ℕ)
  | leaf x => [(x, 0, 0)]
  | node a l b r =>
    (leaves l).map (fun p => (p.1, p.2.1 + a, p.2.2 + 1)) ++
      (leaves r).map (fun p => (p.1, p.2.1 + b, p.2.2 + 1))

Uses 1 · Used by 6

Statement usesRooted binary tree with edge lengths

Used byPauplin's formula · Kraft's equality · Kraft equality · Leaf labels of an unrooted binary tree · Leaf pairs of a rooted binary tree with path lengths · Leaf pairs of an unrooted binary tree with path lengths

DefinitionLeaf pairs of a rooted binary tree with path lengths#✓fully proved

The unordered pairs of leaves, each with the two labels, the length of the path between the two leaves and its number of edges.

def pairs : RTree X → List (X × X × ℝ × ℕ)
  | leaf _ => []
  | node a l b r =>
    pairs l ++ pairs r ++
      (leaves l).flatMap fun p =>
        (leaves r).map fun q => (p.1, q.1, p.2.1 + a + b + q.2.1, p.2.2 + q.2.2 + 2)

Uses 2 · Used by 3

Statement usesRooted binary tree with edge lengths · Leaves of a rooted binary tree with root distances

Used byPauplin's formula · Kraft equality · Leaf pairs of an unrooted binary tree with path lengths

TheoremKraft's equality#✓fully proved

Kraft's equality for a rooted binary tree: ∑_{leaves} 2^{-depth} = 1.

theorem kraft (t : RTree X) : (t.leaves.map fun p => ((2 : ℝ) ^ p.2.2)⁻¹).sum = 1

Uses 2 · Used by 2

Statement usesRooted binary tree with edge lengths · Leaves of a rooted binary tree with root distances

Used byPauplin's formula · Kraft equality

Unrooted binary trees and Pauplin's formula

DefinitionTotal edge length of an unrooted binary tree#✓fully proved

The total length of the edges.

def length (T : UTree X) : ℝ :=
  T.left.length + T.len + T.right.length

Uses 3 · Used by 2

Statement usesRooted binary tree with edge lengths · Total edge length of a rooted binary tree · Unrooted binary tree with edge lengths

Used byThe balanced minimum-evolution length of a tree metric is the tree length · Pauplin's formula

DefinitionLeaf labels of an unrooted binary tree#✓fully proved

The leaf labels (with multiplicity).

def labels (T : UTree X) : List X :=
  T.left.leaves.map Prod.fst ++ T.right.leaves.map Prod.fst

Uses 3 · Used by 1

Statement usesRooted binary tree with edge lengths · Leaves of a rooted binary tree with root distances · Unrooted binary tree with edge lengths

Used byKraft equality

DefinitionLeaf pairs of an unrooted binary tree with path lengths#✓fully proved

The unordered pairs of leaves, each with the two labels, the length d_T(i, j) of the path between the two leaves and its number of edges τ_ij.

def pairs (T : UTree X) : List (X × X × ℝ × ℕ) :=
  T.left.pairs ++ T.right.pairs ++
    T.left.leaves.flatMap fun p =>
      T.right.leaves.map fun q => (p.1, q.1, p.2.1 + T.len + q.2.1, p.2.2 + q.2.2 + 1)

Uses 4 · Used by 4

Statement usesRooted binary tree with edge lengths · Leaves of a rooted binary tree with root distances · Leaf pairs of a rooted binary tree with path lengths · Unrooted binary tree with edge lengths

Used byBalanced minimum-evolution length · The balanced minimum-evolution length of a tree metric is the tree length · Pauplin's formula · Kraft equality

DefinitionBalanced minimum-evolution length#✓fully proved

The balanced minimum-evolution length of the topology of T for a dissimilarity d (Desper and Gascuel 2002): ∑_{i<j} 2^{1-τ_ij} (d(i, j) + d(j, i)) / 2. It depends on T only through the topological distances τ_ij. Each term is symmetrized, so the value does not depend on the orientation T.pairs happens to assign to a pair: swapping the children of a node, or the two sides of the root edge, leaves bmeLength unchanged.

noncomputable def bmeLength (T : UTree X) (d : X → X → ℝ) : ℝ :=
  (T.pairs.map fun p => pauplinCoeff p.2.2.2 * (d p.1 p.2.1 + d p.2.1 p.1) / 2).sum

Uses 3 · Used by 1

Statement usesUnrooted binary tree with edge lengths · Leaf pairs of an unrooted binary tree with path lengths · Pauplin coefficient of a pair of leaves

Used byThe balanced minimum-evolution length of a tree metric is the tree length

TheoremPauplin's formula#✓fully proved

Pauplin's formula (Pauplin 2000): the total edge length of a binary tree with real edge lengths is ∑_{i<j} 2^{1-τ_ij} d_T(i, j), the sum over pairs of leaves of the path length weighted by 2 to the power one minus the number of edges on the path.

theorem bmeLength_pathLength (T : UTree X) :
    (T.pairs.map fun p => pauplinCoeff p.2.2.2 * p.2.2.1).sum = T.length

Uses 9 · Used by 1

Statement usesUnrooted binary tree with edge lengths · Total edge length of an unrooted binary tree · Leaf pairs of an unrooted binary tree with path lengths · Pauplin coefficient of a pair of leaves

Proof usesRooted binary tree with edge lengths · Kraft's equality · Leaves of a rooted binary tree with root distances · Total edge length of a rooted binary tree · Leaf pairs of a rooted binary tree with path lengths

Used byThe balanced minimum-evolution length of a tree metric is the tree length

TheoremThe balanced minimum-evolution length of a tree metric is the tree length#✓fully proved

If d is the path-length dissimilarity of T on its leaves and d is symmetric, bmeLength T d = length T. Symmetry is needed because bmeLength averages the two orientations of each pair.

theorem bmeLength_eq_length (T : UTree X) (d : X → X → ℝ)
    (hd : ∀ p ∈ T.pairs, d p.1 p.2.1 = p.2.2.1)
    (hsym : ∀ x y, d x y = d y x) : T.bmeLength d = T.length

Uses 6

Statement usesUnrooted binary tree with edge lengths · Balanced minimum-evolution length · Total edge length of an unrooted binary tree · Leaf pairs of an unrooted binary tree with path lengths

Proof usesPauplin's formula · Pauplin coefficient of a pair of leaves

TheoremKraft equality#✓fully proved

Kraft equality for unrooted binary trees: for every leaf i of a tree with distinct leaf labels, ∑_{j ≠ i} 2^{1-τ_ij} = 1.

theorem kraft_leaf [DecidableEq X] (T : UTree X) (hT : T.labels.Nodup) (x : X) (hx : x ∈ T.labels) :
    (T.pairs.map fun p => if p.1 = x ∨ p.2.1 = x then pauplinCoeff p.2.2.2 else 0).sum = 1

Uses 8

Statement usesUnrooted binary tree with edge lengths · Leaf labels of an unrooted binary tree · Leaf pairs of an unrooted binary tree with path lengths · Pauplin coefficient of a pair of leaves

Proof usesRooted binary tree with edge lengths · Kraft's equality · Leaves of a rooted binary tree with root distances · Leaf pairs of a rooted binary tree with path lengths

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.