PhyloCSF coding classifier

DefinitionLeaf data of an alignment column#✓fully proved

The leaf data of an alignment column col : L → S: the indicator of the observed codon at each leaf.

def leafData (col : L → S) (l : L) (s : S) : ℝ := if col l = s then 1 else 0

Used by 2

Used byLikelihood of one alignment column · Site likelihood by Felsenstein's pruning algorithm

DefinitionLikelihood of one alignment column#✓fully proved

The likelihood of one alignment column under the model (t, π).

noncomputable def siteLik (t : Tree L S ℝ) (π : S → ℝ) (col : L → S) : ℝ :=
  likelihood (leafData col) t π

Uses 3 · Used by 5

Statement usesRooted binary tree with transition weights · Site likelihood of a phylogenetic tree · Leaf data of an alignment column

Used byLikelihood of an alignment of independent columns · The PhyloCSF score · The score is the log-likelihood ratio of the alignment · Site likelihood by Felsenstein's pruning algorithm · PhyloCSF's score threshold test is most powerful for unnormalized weights

DefinitionLikelihood of an alignment of independent columns#✓fully proved

The likelihood of an alignment of m independent columns: the product of the site likelihoods.

noncomputable def alignLik (t : Tree L S ℝ) (π : S → ℝ) (A : Fin m → L → S) : ℝ :=
  ∏ k, siteLik t π (A k)

Uses 2 · Used by 2

Statement usesRooted binary tree with transition weights · Likelihood of one alignment column

Used byThe score is the log-likelihood ratio of the alignment · PhyloCSF's score threshold test is most powerful for unnormalized weights

DefinitionThe PhyloCSF score#✓fully proved

The PhyloCSF score (natural-log scale): the sum over the columns of the log-likelihood ratio of the coding model (tC, πC) against the non-coding model (tN, πN). The published PhyloCSF score is reported in decibans; see score_decibans for the conversion. Thresholds for this score are in natural-log units.

noncomputable def score (tC : Tree L S ℝ) (πC : S → ℝ) (tN : Tree L S ℝ) (πN : S → ℝ)
    (A : Fin m → L → S) : ℝ :=
  ∑ k, log (siteLik tC πC (A k) / siteLik tN πN (A k))

Uses 2 · Used by 5

Statement usesRooted binary tree with transition weights · Likelihood of one alignment column

Used byThe published PhyloCSF score in decibans · Deciban score as a rescaled natural-log score · The score is the log-likelihood ratio of the alignment · Score threshold test for calling an alignment coding · PhyloCSF's score threshold test is most powerful for unnormalized weights

DefinitionThe published PhyloCSF score in decibans#✓fully proved

10 * log₁₀(L_C / L_N), i.e. (10 / log 10) * score, since log₁₀ x = log x / log 10.

noncomputable def score_decibans (tC : Tree L S ℝ) (πC : S → ℝ) (tN : Tree L S ℝ) (πN : S → ℝ)
    (A : Fin m → L → S) : ℝ :=
  (10 / log 10) * score tC πC tN πN A

Uses 2 · Used by 1

Statement usesRooted binary tree with transition weights · The PhyloCSF score

Used byDeciban score as a rescaled natural-log score

TheoremDeciban score as a rescaled natural-log score#✓fully proved

Decibans are the natural-log score rescaled by 10 / log 10.

theorem score_decibans_eq (tC : Tree L S ℝ) (πC : S → ℝ) (tN : Tree L S ℝ) (πN : S → ℝ)
    (A : Fin m → L → S) :
    score_decibans tC πC tN πN A = (10 / log 10) * score tC πC tN πN A

Uses 3

Statement usesRooted binary tree with transition weights · The PhyloCSF score · The published PhyloCSF score in decibans

TheoremSite likelihood by Felsenstein's pruning algorithm#✓fully proved

Each site likelihood is computed by Felsenstein's pruning algorithm.

theorem siteLik_eq_sum_prune (t : Tree L S ℝ) (π : S → ℝ) (col : L → S) :
    siteLik t π col = ∑ s, π s * prune (leafData col) t s

Uses 5

Statement usesRooted binary tree with transition weights · Felsenstein's pruning recursion · Leaf data of an alignment column · Likelihood of one alignment column

Proof usesThe site likelihood by pruning

TheoremThe score is the log-likelihood ratio of the alignment#✓fully proved

The score is the log-likelihood ratio of the alignment when all site likelihoods are positive.

theorem score_eq_log_div {tC tN : Tree L S ℝ} {πC πN : S → ℝ} {A : Fin m → L → S}
    (hC : ∀ k, 0 < siteLik tC πC (A k)) (hN : ∀ k, 0 < siteLik tN πN (A k)) :
    score tC πC tN πN A = log (alignLik tC πC A / alignLik tN πN A)

Uses 4 · Used by 1

Statement usesRooted binary tree with transition weights · Likelihood of an alignment of independent columns · The PhyloCSF score · Likelihood of one alignment column

Used byPhyloCSF's score threshold test is most powerful for unnormalized weights

DefinitionScore threshold test for calling an alignment coding#✓fully proved

The threshold test on the score: call the alignment coding (1) iff the score exceeds the cutoff c.

noncomputable def scoreTest (tC : Tree L S ℝ) (πC : S → ℝ) (tN : Tree L S ℝ) (πN : S → ℝ)
    (c : ℝ) (A : Fin m → L → S) : Set.Icc (0 : ℝ) 1 :=
  if c < score tC πC tN πN A then ⟨1, by norm_num, le_rfl⟩ else ⟨0, le_rfl, by norm_num⟩

Uses 2 · Used by 1

Statement usesRooted binary tree with transition weights · The PhyloCSF score

Used byPhyloCSF's score threshold test is most powerful for unnormalized weights

TheoremPhyloCSF's score threshold test is most powerful for unnormalized weights#✓fully proved

With positive site likelihoods under both models, a randomized test φ whose weighted size under the non-coding weights is at most that of scoreTest c has at most its weighted power under the coding weights. This is the dominated Neyman–Pearson inequality for the unnormalized alignment weights alignLik; it becomes a statement about statistical size and power only under additional normalization hypotheses (∑ A, alignLik = 1 for each model).

theorem weighted_power_le_scoreTest {tC tN : Tree L S ℝ} {πC πN : S → ℝ}
    (hC : ∀ col, 0 < siteLik tC πC col) (hN : ∀ col, 0 < siteLik tN πN col) (c : ℝ)
    (φ : (Fin m → L → S) → Set.Icc (0 : ℝ) 1)
    (hsize : ∑ A, (φ A).val * alignLik tN πN A ≤
      ∑ A : Fin m → L → S, (scoreTest tC πC tN πN c A).val * alignLik tN πN A) :
    ∑ A, (φ A).val * alignLik tC πC A ≤
      ∑ A : Fin m → L → S, (scoreTest tC πC tN πN c A).val * alignLik tC πC A

Uses 7

Statement usesRooted binary tree with transition weights · Likelihood of an alignment of independent columns · Score threshold test for calling an alignment coding · Likelihood of one alignment column

Proof usesThe PhyloCSF score · The score is the log-likelihood ratio of the alignment · Neyman–Pearson lemma

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.