Pulley principle, LogDet distances and Felsenstein zone

41 fully proved

The pulley principle

StructureReversible semigroup of transition matrices#✓fully proved

A family of transition matrices P t, indexed by branch length, is a reversible semigroup for the distribution π: it satisfies the Chapman–Kolmogorov equation and detailed balance π a P t a b = π b P t b a. With rows summing to 1, detailed balance makes π stationary; the pulley principle uses only the two equations below.

structure IsReversibleSemigroup (π : S → ℝ) (P : ℝ → S → S → ℝ) : Prop where
  /-- The Chapman–Kolmogorov equation `P s * P t = P (s + t)`. -/
  chapman_kolmogorov : ∀ s t a c, ∑ b, P s a b * P t b c = P (s + t) a c
  /-- Detailed balance with `π`. -/
  detailed_balance : ∀ t a b, π a * P t a b = π b * P t b a

Used by 4

Used byReversible continuous-time models give reversible semigroups · The root can be pushed to the end of its edge · Pulley principle, rerooting · Pulley principle, sliding

TheoremPartial likelihoods are invariant under swapping subtrees#✓fully proved

Swapping the two subtrees of a node does not change its partial likelihoods; with likelihood_node_comm this lets the rerooting move likelihood_reroot reach either child.

theorem prune_node_comm (obs : L → S → ℝ) (P Q : S → S → ℝ) (l r : Tree L S ℝ) :
    prune obs (node P l Q r) = prune obs (node Q r P l)

Uses 2

Statement usesRooted binary tree with transition weights · Felsenstein's pruning recursion

TheoremLikelihood is invariant under swapping root subtrees#✓fully proved

Swapping the two subtrees of the root does not change the likelihood.

theorem likelihood_node_comm (obs : L → S → ℝ) (P Q : S → S → ℝ) (l r : Tree L S ℝ)
    (π : S → ℝ) : likelihood obs (node P l Q r) π = likelihood obs (node Q r P l) π

Uses 4

Statement usesRooted binary tree with transition weights · Site likelihood of a phylogenetic tree

Proof usesThe site likelihood by pruning · Felsenstein's pruning recursion

TheoremThe root can be pushed to the end of its edge#✓fully proved

With the root on the edge between the subtrees l and r, at distances s and t, the likelihood is that of the root placed at the root of l, with r at distance s + t.

theorem likelihood_node_eq {π : S → ℝ} {P : ℝ → S → S → ℝ} (hP : IsReversibleSemigroup π P)
    (obs : L → S → ℝ) (l r : Tree L S ℝ) (s t : ℝ) :
    likelihood obs (node (P s) l (P t) r) π =
      ∑ b, π b * prune obs l b * ∑ c, P (s + t) b c * prune obs r c

Uses 5 · Used by 2

Statement usesRooted binary tree with transition weights · Site likelihood of a phylogenetic tree · Felsenstein's pruning recursion · Reversible semigroup of transition matrices

Proof usesThe site likelihood by pruning

Used byPulley principle, rerooting · Pulley principle, sliding

TheoremPulley principle, sliding#✓fully proved

Moving the root along its edge does not change the likelihood (Felsenstein 1981).

theorem likelihood_slide {π : S → ℝ} {P : ℝ → S → S → ℝ} (hP : IsReversibleSemigroup π P)
    (obs : L → S → ℝ) (l r : Tree L S ℝ) {s t s' t' : ℝ} (h : s + t = s' + t') :
    likelihood obs (node (P s) l (P t) r) π = likelihood obs (node (P s') l (P t') r) π

Uses 5

Statement usesRooted binary tree with transition weights · Site likelihood of a phylogenetic tree · Reversible semigroup of transition matrices

Proof usesFelsenstein's pruning recursion · The root can be pushed to the end of its edge

TheoremPulley principle, rerooting#✓fully proved

Let the root sit on the edge between an internal vertex x (at distance s₁) and the subtree C (at distance s₂), where x has the subtrees A and B at distances a and b. Moving the root to the edge between x and A, at distance u₁ from A and u₂ from x with u₁ + u₂ = a, gives the same likelihood: the unrooted tree and its edge lengths are unchanged (Felsenstein 1981).

theorem likelihood_reroot {π : S → ℝ} {P : ℝ → S → S → ℝ} (hP : IsReversibleSemigroup π P)
    (obs : L → S → ℝ) (A B C : Tree L S ℝ) {s₁ s₂ a b u₁ u₂ : ℝ} (hu : u₁ + u₂ = a) :
    likelihood obs (node (P s₁) (node (P a) A (P b) B) (P s₂) C) π =
      likelihood obs (node (P u₁) A (P u₂) (node (P b) B (P (s₁ + s₂)) C)) π

Uses 5

Statement usesRooted binary tree with transition weights · Site likelihood of a phylogenetic tree · Reversible semigroup of transition matrices

Proof usesFelsenstein's pruning recursion · The root can be pushed to the end of its edge

TheoremReversible continuous-time models give reversible semigroups#✓fully proved

A reversible continuous-time model gives a reversible semigroup: if π is in detailed balance with the generator Q, the transition functions exp (t • Q) form a reversible semigroup for π.

theorem isReversibleSemigroup_ctmcTransition [DecidableEq S] {π : S → ℝ} {Q : Matrix S S ℝ}
    (h : IsDetailedBalance π Q) :
    IsReversibleSemigroup π (fun t => ctmcTransition Q t)

Uses 5

Statement usesReversible semigroup of transition matrices · Detailed balance · Transition semigroup of a continuous-time Markov chain

Proof usesDetailed balance propagates to the transition function · Chapman–Kolmogorov equation for the transition semigroup

LogDet / paralinear distances

DefinitionLogDet (paralinear) distance#✓fully proved

The LogDet (paralinear) distance of a joint distribution matrix F (F i j = ℙ(X = i, Y = j)): -log |det F| + (log det Π_X + log det Π_Y) / 2, where the diagonal marginal matrices have determinants ∏ i, ∑ j, F i j and ∏ j, ∑ i, F i j. It is a distance only when det F ≠ 0 and the marginals are positive; otherwise the value is Lean's totalized logarithm (log 0 = 0).

noncomputable def paralinear (F : Matrix ι ι ℝ) : ℝ :=
  -Real.log |F.det| + (Real.log (∏ i, ∑ j, F i j) + Real.log (∏ j, ∑ i, F i j)) / 2

Used by 4

Used byAdditivity of the LogDet distance along a chain, one step · LogDet distance of a vertex to itself is zero · Additivity of the LogDet distance along a path · Additivity of the LogDet distance at a separating vertex

TheoremLogDet distance of a vertex to itself is zero#✓fully proved

The distance of a vertex to itself is 0: the joint distribution of X with itself is the diagonal matrix of its (positive) marginal.

theorem paralinear_diagonal {p : ι → ℝ} (hp : ∀ i, 0 < p i) : paralinear (diagonal p) = 0

Uses 1 · Used by 1

Statement usesLogDet (paralinear) distance

Used byAdditivity of the LogDet distance along a path

TheoremNonsingular transition matrices preserve positive distributions#✓fully proved

Under a nonnegative, nonsingular transition matrix, a positive distribution stays positive: every column of M has a positive entry. This puts the LogDet logarithms in their domain.

theorem vecMul_pos {p : ι → ℝ} (hp : ∀ i, 0 < p i) {M : Matrix ι ι ℝ} (hM : ∀ i j, 0 ≤ M i j)
    (hdet : M.det ≠ 0) (j : ι) : 0 < (p ᵥ* M) j

Used by 1

Used byAdditivity of the LogDet distance along a chain, one step

TheoremAdditivity of the LogDet distance at a separating vertex#✓fully proved

Additivity of the LogDet distance at a separating vertex (Steel 1994; Lockhart et al. 1994; Lake 1994). Let Y have distribution p (positive) and let X and Z be conditionally independent given Y, with transition matrices M (from Y to X) and N (from Y to Z) whose rows sum to 1 and whose determinants are nonzero. The joint distribution matrices are F_XY = Mᵀ Π_Y, F_YZ = Π_Y N and F_XZ = Mᵀ Π_Y N, and d(X, Z) = d(X, Y) + d(Y, Z). The identity uses no sign condition on M and N; with nonnegative entries all logarithms are of positive numbers (vecMul_pos).

theorem paralinear_threePoint {p : ι → ℝ} (hp : ∀ i, 0 < p i) {M N : Matrix ι ι ℝ}
    (hMrow : ∀ i, ∑ j, M i j = 1) (hNrow : ∀ i, ∑ j, N i j = 1) (hM : M.det ≠ 0)
    (hN : N.det ≠ 0) :
    paralinear (Mᵀ * diagonal p * N) =
      paralinear (Mᵀ * diagonal p) + paralinear (diagonal p * N)

Uses 1

Statement usesLogDet (paralinear) distance

TheoremAdditivity of the LogDet distance along a chain, one step#✓fully proved

For a Markov chain X → Y → Z with X distributed as p (positive), transition matrices A (nonnegative) and B with unit row sums and nonzero determinants, d(X, Z) = d(X, Y) + d(Y, Z), where F_XZ = Π_X A B, F_XY = Π_X A and F_YZ = Π_Y B with Y distributed as p A.

theorem paralinear_chain_step {p : ι → ℝ} (hp : ∀ i, 0 < p i) {A B : Matrix ι ι ℝ}
    (hA : ∀ i j, 0 ≤ A i j) (hArow : ∀ i, ∑ j, A i j = 1) (hBrow : ∀ i, ∑ j, B i j = 1)
    (hAdet : A.det ≠ 0) (hBdet : B.det ≠ 0) :
    paralinear (diagonal p * (A * B)) =
      paralinear (diagonal p * A) + paralinear (diagonal (p ᵥ* A) * B)

Uses 2 · Used by 1

Statement usesLogDet (paralinear) distance

Proof usesNonsingular transition matrices preserve positive distributions

Used byAdditivity of the LogDet distance along a path

DefinitionProduct of transition matrices along a path#✓fully proved

The product M 0 * M 1 * ⋯ * M (n - 1) of the transition matrices along the first n edges of a path.

def pathProd (M : ℕ → Matrix ι ι ℝ) : ℕ → Matrix ι ι ℝ
  | 0 => 1
  | n + 1 => pathProd M n * M n

Used by 1

Used byAdditivity of the LogDet distance along a path

TheoremAdditivity of the LogDet distance along a path#✓fully proved

Additivity of the LogDet distance along a path (Steel 1994; Lockhart et al. 1994): for a Markov chain v₀ → v₁ → ⋯ → v_n along a path, with positive initial distribution p and nonnegative nonsingular transition matrices M i with unit row sums, the LogDet distance between the ends is the sum of the distances of consecutive vertices. The joint distribution of v₀, v_n is Π_{v₀} M 0 ⋯ M (n - 1), and that of v_i, v_{i+1} is Π_{v_i} M i, where v_i has distribution p M 0 ⋯ M (i - 1). Under the general Markov model on a tree with positive marginals and nonsingular matrices, the states along any path form such a chain once the model is rooted at one end of the path.

theorem paralinear_pathProd {p : ι → ℝ} (hp : ∀ i, 0 < p i) {M : ℕ → Matrix ι ι ℝ}
    (hM : ∀ n i j, 0 ≤ M n i j) (hrow : ∀ n i, ∑ j, M n i j = 1) (hdet : ∀ n, (M n).det ≠ 0)
    (n : ℕ) :
    paralinear (diagonal p * pathProd M n) =
      ∑ i ∈ range n, paralinear (diagonal (p ᵥ* pathProd M i) * M i)

Uses 4

Statement usesLogDet (paralinear) distance · Product of transition matrices along a path

Proof usesAdditivity of the LogDet distance along a chain, one step · LogDet distance of a vertex to itself is zero

The Felsenstein zone

DefinitionSymmetric two-state model on a branch#✓fully proved

The symmetric two-state model on one branch: the state changes with probability p. As a model, 0 ≤ p ≤ 1/2.

def twoState (p : ℝ) (a b : Bool) : ℝ :=
  if a = b then 1 - p else p

Used by 6

Used byNonnegativity of site pattern probabilities · Four-taxon quartet tree model · True split against third split frequency difference · Wrong split against third split frequency difference · Felsenstein (1978), the exact comparison · Site pattern probabilities sum to one

DefinitionFour-taxon quartet tree model#✓fully proved

The quartet ((A, B), (C, D)) on the taxa 0 = A, 1 = B, 2 = C, 3 = D, with change probabilities pA, pB, pC, pD on the pendant edges and pI on the internal edge. The root sits at the AB end of the internal edge (the edge to the AB cherry vertex has change probability 0); by the pulley principle its position does not matter.

def quartet (pA pB pC pD pI : ℝ) : Tree (Fin 4) Bool ℝ :=
  node (twoState 0) (node (twoState pA) (leaf 0) (twoState pB) (leaf 1)) (twoState pI)
    (node (twoState pC) (leaf 2) (twoState pD) (leaf 3))

Uses 2 · Used by 1

Statement usesRooted binary tree with transition weights · Symmetric two-state model on a branch

Used byProbability of a site pattern on a quartet

DefinitionLeaf weights of a site pattern#✓fully proved

The leaf weights of a site pattern σ: the indicator of the observed state.

def siteObs (σ : Fin 4 → Bool) (l : Fin 4) (s : Bool) : ℝ :=
  if s = σ l then 1 else 0

Used by 6

Used byProbability of a site pattern on a quartet · Nonnegativity of site pattern probabilities · True split against third split frequency difference · Wrong split against third split frequency difference · Felsenstein (1978), the exact comparison · Site pattern probabilities sum to one

DefinitionProbability of a site pattern on a quartet#✓fully proved

The probability of the site pattern σ on the quartet, with the uniform root distribution (the stationary distribution of the symmetric model).

noncomputable def patternProb (pA pB pC pD pI : ℝ) (σ : Fin 4 → Bool) : ℝ :=
  likelihood (siteObs σ) (quartet pA pB pC pD pI) (fun _ => 1 / 2)

Uses 3 · Used by 9

Statement usesSite likelihood of a phylogenetic tree · Four-taxon quartet tree model · Leaf weights of a site pattern

Used byParsimony is inconsistent in the Felsenstein zone · Expected Fitch parsimony score on a quartet · The Felsenstein zone · Nonnegativity of site pattern probabilities · Expected frequency of patterns supporting a split · True split against third split frequency difference · Wrong split against third split frequency difference · Felsenstein (1978), the exact comparison · Site pattern probabilities sum to one

TheoremSite pattern probabilities sum to one#✓fully proved

The pattern probabilities sum to 1, for all parameters.

theorem sum_patternProb (pA pB pC pD pI : ℝ) :
    ∑ σ, patternProb pA pB pC pD pI σ = 1

Uses 7

Statement usesProbability of a site pattern on a quartet

Proof usesRooted binary tree with transition weights · Site likelihood of a phylogenetic tree · The site likelihood by pruning · Felsenstein's pruning recursion · Leaf weights of a site pattern · Symmetric two-state model on a branch

TheoremNonnegativity of site pattern probabilities#✓fully proved

The pattern probabilities are nonnegative for change probabilities in [0, 1].

theorem patternProb_nonneg {pA pB pC pD pI : ℝ} (hA : pA ∈ Set.Icc 0 1) (hB : pB ∈ Set.Icc 0 1)
    (hC : pC ∈ Set.Icc 0 1) (hD : pD ∈ Set.Icc 0 1) (hI : pI ∈ Set.Icc 0 1)
    (σ : Fin 4 → Bool) : 0 ≤ patternProb pA pB pC pD pI σ

Uses 7

Statement usesProbability of a site pattern on a quartet

Proof usesRooted binary tree with transition weights · Site likelihood of a phylogenetic tree · The site likelihood by pruning · Felsenstein's pruning recursion · Leaf weights of a site pattern · Symmetric two-state model on a branch

DefinitionSite pattern supporting a split#✓fully proved

The site pattern σ supports the split {a, b} | {c, d}: a, b agree, c, d agree, and the two pairs differ (a parsimony-informative pattern for that split).

def Supports (σ : Fin 4 → Bool) (a b c d : Fin 4) : Prop :=
  σ a = σ b ∧ σ c = σ d ∧ σ a ≠ σ c

Used by 6

Used byThe Felsenstein zone · Difference of parsimony scores of two quartets · Expected frequency of patterns supporting a split · True split against third split frequency difference · Wrong split against third split frequency difference · Felsenstein (1978), the exact comparison

DefinitionExpected frequency of patterns supporting a split#✓fully proved

The expected frequency of the patterns supporting the split {a, b} | {c, d}.

noncomputable def splitFreq (pA pB pC pD pI : ℝ) (a b c d : Fin 4) : ℝ :=
  ∑ σ, if Supports σ a b c d then patternProb pA pB pC pD pI σ else 0

Uses 2 · Used by 4

Statement usesSite pattern supporting a split · Probability of a site pattern on a quartet

Used byThe Felsenstein zone · True split against third split frequency difference · Wrong split against third split frequency difference · Felsenstein (1978), the exact comparison

TheoremFelsenstein (1978), the exact comparison#✓fully proved

With change probability P on the long non-sister branches to A and C and Q on the other three branches, the expected frequency of patterns supporting the wrong split AC | BD exceeds that of the true split AB | CD by (1 - 2 Q) (P ^ 2 - Q (1 - Q)), for all real P, Q. This is Felsenstein's equations (16)–(17) (his four-species model has equal probabilities of change 0 → 1 and reversion 1 → 0).

theorem splitFreq_wrong_sub_true (P Q : ℝ) :
    splitFreq P Q P Q Q 0 2 1 3 - splitFreq P Q P Q Q 0 1 2 3 =
      (1 - 2 * Q) * (P ^ 2 - Q * (1 - Q))

Uses 9 · Used by 1

Statement usesExpected frequency of patterns supporting a split

Proof usesRooted binary tree with transition weights · Site likelihood of a phylogenetic tree · The site likelihood by pruning · Felsenstein's pruning recursion · Site pattern supporting a split · Probability of a site pattern on a quartet · Leaf weights of a site pattern · Symmetric two-state model on a branch

Used byThe Felsenstein zone

TheoremWrong split against third split frequency difference#✓fully proved

The wrong split AC | BD against the third split AD | BC: the difference of expected frequencies is (1 - 2 Q) (P - Q) ^ 2.

theorem splitFreq_wrong_sub_third (P Q : ℝ) :
    splitFreq P Q P Q Q 0 2 1 3 - splitFreq P Q P Q Q 0 3 1 2 = (1 - 2 * Q) * (P - Q) ^ 2

Uses 9 · Used by 1

Statement usesExpected frequency of patterns supporting a split

Proof usesRooted binary tree with transition weights · Site likelihood of a phylogenetic tree · The site likelihood by pruning · Felsenstein's pruning recursion · Site pattern supporting a split · Probability of a site pattern on a quartet · Leaf weights of a site pattern · Symmetric two-state model on a branch

Used byThe Felsenstein zone

TheoremTrue split against third split frequency difference#✓fully proved

The true split AB | CD against the third split AD | BC: the difference of expected frequencies is Q (1 - 2 Q) (1 - 2 P).

theorem splitFreq_true_sub_third (P Q : ℝ) :
    splitFreq P Q P Q Q 0 1 2 3 - splitFreq P Q P Q Q 0 3 1 2 =
      Q * (1 - 2 * Q) * (1 - 2 * P)

Uses 9

Statement usesExpected frequency of patterns supporting a split

Proof usesRooted binary tree with transition weights · Site likelihood of a phylogenetic tree · The site likelihood by pruning · Felsenstein's pruning recursion · Site pattern supporting a split · Probability of a site pattern on a quartet · Leaf weights of a site pattern · Symmetric two-state model on a branch

DefinitionRooted quartet with unit costs#✓fully proved

The rooted quartet ((a, b), (c, d)) with unit costs, for Fitch's algorithm.

def quartetShape (a b c d : Fin 4) : Tree (Fin 4) Bool Parsimony.Cost :=
  node unitCost (node unitCost (leaf a) unitCost (leaf b)) unitCost
    (node unitCost (leaf c) unitCost (leaf d))

Uses 3 · Used by 1

Statement usesRooted binary tree with transition weights · Min-plus cost semiring · Unit substitution cost

Used byFitch parsimony score on a quartet

DefinitionFitch parsimony score on a quartet#✓fully proved

The Fitch parsimony score of the site pattern σ on the quartet ((a, b), (c, d)); it is the small-parsimony score by Parsimony.fitch_score_eq.

def parsimonyScore (a b c d : Fin 4) (σ : Fin 4 → Bool) : ℕ :=
  (fitch σ (quartetShape a b c d)).2

Uses 3 · Used by 4

Statement usesRooted quartet with unit costs · Min-plus cost semiring · Fitch's algorithm

Used byParsimony is inconsistent in the Felsenstein zone · Expected Fitch parsimony score on a quartet · The Felsenstein zone · Difference of parsimony scores of two quartets

TheoremDifference of parsimony scores of two quartets#✓fully proved

On four taxa, the parsimony scores of two quartets differ only on informative patterns: the score on AB | CD minus the score on AC | BD is 1 on patterns supporting AC | BD, -1 on patterns supporting AB | CD, and 0 otherwise; likewise for AD | BC.

theorem parsimonyScore_sub (σ : Fin 4 → Bool) :
    ((parsimonyScore 0 1 2 3 σ : ℤ) - parsimonyScore 0 2 1 3 σ =
        (if Supports σ 0 2 1 3 then 1 else 0) - (if Supports σ 0 1 2 3 then 1 else 0)) ∧
      ((parsimonyScore 0 3 1 2 σ : ℤ) - parsimonyScore 0 2 1 3 σ =
        (if Supports σ 0 2 1 3 then 1 else 0) - (if Supports σ 0 3 1 2 then 1 else 0))

Uses 2 · Used by 1

Statement usesSite pattern supporting a split · Fitch parsimony score on a quartet

Used byThe Felsenstein zone

DefinitionExpected Fitch parsimony score on a quartet#✓fully proved

The expected Fitch parsimony score of one site on the quartet ((a, b), (c, d)).

noncomputable def expectedScore (pA pB pC pD pI : ℝ) (a b c d : Fin 4) : ℝ :=
  ∑ σ, patternProb pA pB pC pD pI σ * parsimonyScore a b c d σ

Uses 2 · Used by 2

Statement usesFitch parsimony score on a quartet · Probability of a site pattern on a quartet

Used byParsimony is inconsistent in the Felsenstein zone · The Felsenstein zone

TheoremThe Felsenstein zone#✓fully proved

The Felsenstein zone (Felsenstein 1978): if 0 ≤ Q < 1/2 and P ^ 2 > Q (1 - Q), the wrong quartet AC | BD has strictly smaller expected parsimony score per site than both the true quartet AB | CD and the third quartet AD | BC. The statement is algebraic in P; the model has 0 ≤ P ≤ 1/2.

theorem expectedScore_wrong_lt {P Q : ℝ} (hQ0 : 0 ≤ Q) (hQ : Q < 1 / 2)
    (hPQ : Q * (1 - Q) < P ^ 2) :
    expectedScore P Q P Q Q 0 2 1 3 < expectedScore P Q P Q Q 0 1 2 3 ∧
      expectedScore P Q P Q Q 0 2 1 3 < expectedScore P Q P Q Q 0 3 1 2

Uses 8 · Used by 1

Statement usesExpected Fitch parsimony score on a quartet

Proof usesSite pattern supporting a split · Fitch parsimony score on a quartet · Difference of parsimony scores of two quartets · Probability of a site pattern on a quartet · Expected frequency of patterns supporting a split · Wrong split against third split frequency difference · Felsenstein (1978), the exact comparison

Used byParsimony is inconsistent in the Felsenstein zone

TheoremParsimony is inconsistent in the Felsenstein zone#✓fully proved

Parsimony is inconsistent in the Felsenstein zone (Felsenstein 1978): if the sites σ i are pairwise independent and identically distributed with the pattern distribution of the quartet, and 0 ≤ Q < 1/2, P ^ 2 > Q (1 - Q), then almost surely, for all long enough alignments, the wrong quartet AC | BD has a strictly smaller total Fitch score than the true quartet AB | CD and the third quartet AD | BC.

theorem ae_eventually_parsimony_wrong {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
    [IsProbabilityMeasure μ] {P Q : ℝ} (hQ0 : 0 ≤ Q) (hQ : Q < 1 / 2)
    (hPQ : Q * (1 - Q) < P ^ 2) (σ : ℕ → Ω → Fin 4 → Bool) (hmeas : ∀ i, Measurable (σ i))
    (hident : ∀ i, IdentDistrib (σ i) (σ 0) μ μ)
    (hindep : Pairwise fun i j => IndepFun (σ i) (σ j) μ)
    (hlaw : ∀ τ, μ.real (σ 0 ⁻¹' {τ}) = patternProb P Q P Q Q τ) :
    ∀ᵐ ω ∂μ, ∀ᶠ n in atTop,
      ∑ i ∈ range n, parsimonyScore 0 2 1 3 (σ i ω) <
          ∑ i ∈ range n, parsimonyScore 0 1 2 3 (σ i ω) ∧
        ∑ i ∈ range n, parsimonyScore 0 2 1 3 (σ i ω) <
          ∑ i ∈ range n, parsimonyScore 0 3 1 2 (σ i ω)

Uses 5

Statement usesFitch parsimony score on a quartet · Probability of a site pattern on a quartet

Proof usesExpected Fitch parsimony score on a quartet · The Felsenstein zone · The Monte Carlo estimator is consistent

Jukes–Cantor distances and the consistency of neighbor joining

DefinitionJukes–Cantor transition matrix along a path#✓fully proved

The JC transition matrix along a path whose branch lengths are listed in ts: the product of the branch transition matrices jcProb μ t.

noncomputable def jcPath (μ : ℝ) : List ℝ → Matrix (Fin 4) (Fin 4) ℝ
  | [] => 1
  | t :: ts => Matrix.of (jcProb μ t) * jcPath μ ts

Uses 1 · Used by 4

Statement usesJukes–Cantor transition probability

Used byStatistical consistency of neighbor joining under Jukes–Cantor · Statistical consistency of neighbor joining under Jukes–Cantor · JC-corrected distances are path lengths · Chapman–Kolmogorov along a path

TheoremChapman–Kolmogorov along a path#✓fully proved

The JC transition matrix along a path is the transition matrix of the total length.

theorem jcPath_eq (μ : ℝ) (ts : List ℝ) : jcPath μ ts = Matrix.of (jcProb μ ts.sum)

Uses 4 · Used by 2

Statement usesJukes–Cantor transition matrix along a path · Jukes–Cantor transition probability

Proof usesJukes–Cantor transition matrix at time zero is the identity · Chapman–Kolmogorov equation

Used byStatistical consistency of neighbor joining under Jukes–Cantor · JC-corrected distances are path lengths

TheoremJC-corrected distances are path lengths#✓fully proved

JC-corrected distances are path lengths (Jukes & Cantor 1969): the JC distance of the probability that the two ends of a path differ is μ times the total branch length.

theorem jcDistance_jcPath (μ : ℝ) (ts : List ℝ) (i : Fin 4) :
    jcDistance (∑ j ∈ univ.erase i, jcPath μ ts i j) = μ * ts.sum

Uses 5

Statement usesJukes–Cantor transition matrix along a path · Jukes–Cantor distance

Proof usesChapman–Kolmogorov along a path · The Jukes–Cantor distance correction · Jukes–Cantor transition probability

DefinitionEmpirical p-distance#✓fully proved

The empirical p-distance of the taxa x, y over the first n sites of the alignment seq (seq i x is the base of taxon x at site i): the proportion of sites where they differ.

noncomputable def pHat {X : Type*} (seq : ℕ → X → Fin 4) (n : ℕ) (x y : X) : ℝ :=
  (n : ℝ)⁻¹ * ∑ i ∈ range n, if seq i x = seq i y then 0 else 1

Used by 3

Used byStatistical consistency of neighbor joining under Jukes–Cantor · Strong law for the p-distances · Jukes–Cantor corrected empirical distance

DefinitionJukes–Cantor corrected empirical distance#✓fully proved

The JC-corrected empirical distance jcDistance (pHat seq n x y).

noncomputable def jcHat {X : Type*} (seq : ℕ → X → Fin 4) (n : ℕ) (x y : X) : ℝ :=
  jcDistance (pHat seq n x y)

Uses 2 · Used by 2

Statement usesEmpirical p-distance · Jukes–Cantor distance

Used byStatistical consistency of neighbor joining under Jukes–Cantor · Statistical consistency of neighbor joining under Jukes–Cantor

DefinitionNeighbor joining recovers a tree within a radius#✓fully proved

Neighbor joining recovers the tree within radius r of the dissimilarity d: every complete run of neighbor joining on a symmetric dissimilarity D with zero diagonal and |D x y - d x y| < r for distinct taxa forms exactly the splits of the internal edges of (G, ι). Atteson's theorem gives this for the path-length metric of a binary phylogenetic tree with r half the shortest internal edge length (njRecoversWithin_of_le).

def NJRecoversWithin {X : Type*} [DecidableEq X] [Fintype X] {V : Type*} (G : SimpleGraph V)
    (ι : X → V) (d : X → X → ℝ) (r : ℝ) : Prop :=
  ∀ D : X → X → ℝ, (∀ x y, D x y = D y x) → (∀ x, D x x = 0) →
    (∀ x y, x ≠ y → |D x y - d x y| < r) →
    ∀ S Dc C, NJRun D S Dc C → 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)

Uses 1 · Used by 2

Statement usesRuns of neighbor joining

Used byStatistical consistency of neighbor joining under Jukes–Cantor · Atteson's radius for the scaled tree metric

TheoremStrong law for the p-distances#✓fully proved

For pairwise independent, identically distributed sites, the empirical p-distance of every pair of taxa converges almost surely to the probability that the two taxa differ at a site.

theorem ae_tendsto_pHat {X : Type*} [Finite X] {Ω : Type*} [MeasurableSpace Ω]
    {P : Measure Ω} [IsProbabilityMeasure P] (site : ℕ → Ω → X → Fin 4)
    (hmeas : ∀ i, Measurable (site i)) (hident : ∀ i, IdentDistrib (site i) (site 0) P P)
    (hindep : Pairwise fun i j => IndepFun (site i) (site j) P) :
    ∀ᵐ ω ∂P, ∀ x y, Tendsto (fun n => pHat (fun i => site i ω) n x y) atTop
      (𝓝 (P.real {ω | site 0 ω x ≠ site 0 ω y}))

Uses 2 · Used by 1

Statement usesEmpirical p-distance

Proof usesThe Monte Carlo estimator is consistent

Used byStatistical consistency of neighbor joining under Jukes–Cantor

TheoremStatistical consistency of neighbor joining under Jukes–Cantor#✓fully proved

Statistical consistency of neighbor joining under Jukes–Cantor (Saitou & Nei 1987; Atteson 1999). Let (G, ι) be a binary phylogenetic X-tree with path-length metric d for edge lengths w, and let the sites be pairwise independent and identically distributed, with the two-leaf marginals of the JC model with rate μ and uniform root: for every path p from x to y, ℙ(site x = i, site y = j) = jcPath μ (lengths of p) i j / 4. If neighbor joining recovers the tree within some radius r > 0 of the scaled metric μ d (for μ > 0, Atteson's theorem gives r = μ m / 2, m the shortest internal edge length), then almost surely, for all long enough alignments, every complete run of neighbor joining on the JC-corrected empirical distances returns exactly the splits of the internal edges of the tree.

Cslib.Bioinformatics.Phylogenetics.FelsensteinZone.ae_eventually_njRun_splits_jcHat · 16 lines

theorem ae_eventually_njRun_splits_jcHat {X : Type*} [DecidableEq X] [Fintype X] {V : Type*}
    [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {ι : X → V}
    (hT : IsBinaryPhylogeneticTree G ι) {w : Sym2 V → ℝ} {d : X → X → ℝ}
    (hd : ∀ x y (p : G.Walk (ι x) (ι y)), p.IsPath → d x y = (p.edges.map w).sum)
    {μ r : ℝ} (hr : 0 < r) (hNJ : NJRecoversWithin G ι (fun x y => μ * d x y) r)
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    (site : ℕ → Ω → X → Fin 4) (hmeas : ∀ i, Measurable (site i))
    (hident : ∀ i, IdentDistrib (site i) (site 0) P P)
    (hindep : Pairwise fun i j => IndepFun (site i) (site j) P)
    (hpair : ∀ x y (p : G.Walk (ι x) (ι y)), p.IsPath → ∀ i j,
      P.real {ω | site 0 ω x = i ∧ site 0 ω y = j} = jcPath μ (p.edges.map w) i j / 4) :
    ∀ᵐ ω ∂P, ∀ᶠ n in atTop, ∀ S Dc C, NJRun (jcHat (fun i => site i ω) n) S Dc C →
      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)

Uses 14 · Used by 1

Statement usesNeighbor joining recovers a tree within a radius · Jukes–Cantor corrected empirical distance · Jukes–Cantor transition matrix along a path · Binary phylogenetic tree · Runs of neighbor joining

Proof usesStrong law for the p-distances · Chapman–Kolmogorov along a path · Empirical p-distance · Jukes–Cantor distance · The Jukes–Cantor distance correction · Jukes–Cantor transition probability · Probability that the ends of a branch differ · Closed form of the Jukes–Cantor difference probability · Jukes–Cantor difference probability is below 3/4

Used byStatistical consistency of neighbor joining under Jukes–Cantor

TheoremAtteson's radius for the scaled tree metric#✓fully proved

Let d be the path-length metric of a binary phylogenetic X-tree (G, ι) with positive edge lengths w whose internal edges (no taxon at either end) have length at least m. For μ > 0, neighbor joining recovers the tree within radius μ m / 2 of the scaled metric μ d. This is njRun_splits_of_abs_sub_lt (Atteson 1999) for the edge lengths μ w.

theorem njRecoversWithin_of_le {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)
    {μ m : ℝ} (hμ : 0 < μ)
    (hm : ∀ a b, G.Adj a b → a ∉ Set.range ι → b ∉ Set.range ι → m ≤ w s(a, b)) :
    NJRecoversWithin G ι (fun x y => μ * d x y) (μ * m / 2)

Uses 4 · Used by 1

Statement usesNeighbor joining recovers a tree within a radius · Binary phylogenetic tree

Proof usesRuns of neighbor joining · Atteson's theorem: neighbor joining has ℓ∞ radius 1/2

Used byStatistical consistency of neighbor joining under Jukes–Cantor

TheoremStatistical consistency of neighbor joining under Jukes–Cantor#✓fully proved

Statistical consistency of neighbor joining under Jukes–Cantor (Saitou & Nei 1987; Atteson 1999), without a robustness hypothesis. Let (G, ι) be a binary phylogenetic X-tree with path-length metric d for positive edge lengths w, whose internal edges have length at least m > 0, and let the sites be pairwise independent and identically distributed, with the two-leaf marginals of the JC model with rate μ > 0 and uniform root. Then almost surely, for all long enough alignments, every complete run of neighbor joining on the JC-corrected empirical distances returns exactly the splits of the internal edges of the tree.

Cslib.Bioinformatics.Phylogenetics.FelsensteinZone.ae_eventually_njRun_splits_jcHat_of_le · 18 lines

theorem ae_eventually_njRun_splits_jcHat_of_le {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)
    {μ m : ℝ} (hμ : 0 < μ) (hm0 : 0 < m)
    (hm : ∀ a b, G.Adj a b → a ∉ Set.range ι → b ∉ Set.range ι → m ≤ w s(a, b))
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    (site : ℕ → Ω → X → Fin 4) (hmeas : ∀ i, Measurable (site i))
    (hident : ∀ i, IdentDistrib (site i) (site 0) P P)
    (hindep : Pairwise fun i j => IndepFun (site i) (site j) P)
    (hpair : ∀ x y (p : G.Walk (ι x) (ι y)), p.IsPath → ∀ i j,
      P.real {ω | site 0 ω x = i ∧ site 0 ω y = j} = jcPath μ (p.edges.map w) i j / 4) :
    ∀ᵐ ω ∂P, ∀ᶠ n in atTop, ∀ S Dc C, NJRun (jcHat (fun i => site i ω) n) S Dc C →
      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)

Uses 6

Statement usesJukes–Cantor corrected empirical distance · Jukes–Cantor transition matrix along a path · Binary phylogenetic tree · Runs of neighbor joining

Proof usesStatistical consistency of neighbor joining under Jukes–Cantor · Atteson's radius for the scaled tree metric

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.