Evolutionary conservation scores

• Upper tail of the binomial distribution
• Binomial upper tail at zero equals one
• Binomial upper tail vanishes beyond \(n\)
• The tail is nonincreasing in k
• Derivative of the binomial upper tail
• The binomial upper tail is nondecreasing in p on (0, 1)
• The binomial upper tail is strictly increasing in p on (0, 1)

DefinitionBinomial z-score approximation to the motif conservation score#✓fully proved

The conserved count k of a motif with N occurrences, standardized under Bin(N, p): (k - N p) / √(N p (1 - p)). This is an approximation to Xie et al.'s MCS, not their exact score.

noncomputable def mcsApprox (N : ℕ) (k p : ℝ) : ℝ := (k - N * p) / Real.sqrt (N * p * (1 - p))

Used by 3

Used byMotif conservation score approximation is strictly increasing · Motif conservation score approximation as a de Moivre–Laplace sum · De Moivre–Laplace for the MCS approximation

TheoremMotif conservation score approximation is strictly increasing#✓fully proved

The MCS approximation is strictly increasing in the conserved count, for N ≥ 1 and p ∈ (0, 1).

theorem mcsApprox_strictMono {N : ℕ} (hN : 0 < N) {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1) :
    StrictMono fun k => mcsApprox N k p

Uses 1

Statement usesBinomial z-score approximation to the motif conservation score

TheoremMotif conservation score approximation as a de Moivre–Laplace sum#✓fully proved

The MCS approximation of the number of conserved occurrences among the first n is the de Moivre–Laplace standardized sum.

theorem mcsApprox_sum_eq {Ω : Type*} (X : ℕ → Ω → ℝ) (p : ℝ) (n : ℕ) (ω : Ω) :
    mcsApprox n (∑ i ∈ range n, X i ω) p = deMoivreLaplaceStandardized X p n ω

Uses 2

Statement usesBinomial z-score approximation to the motif conservation score · Standardized partial sums

TheoremDe Moivre–Laplace for the MCS approximation#✓fully proved

If the conservation indicators of the occurrences are i.i.d. Bernoulli(p) with 0 < p < 1, then for every z, P(z ≤ MCS approximation of the first n occurrences) tends to the standard normal mass of [z, ∞).

theorem tendsto_prob_le_mcsApprox {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
    [IsProbabilityMeasure P] (X : ℕ → Ω → ℝ) {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1)
    (h01 : ∀ i, ∀ᵐ ω ∂P, X i ω = 0 ∨ X i ω = 1) (hmean : ∀ i, ∫ ω, X i ω ∂P = p)
    (hindep : iIndepFun X P) (hident : ∀ i, IdentDistrib (X i) (X 0) P P) (z : ℝ) :
    Tendsto (fun n : ℕ => P.real {ω | z ≤ mcsApprox n (∑ i ∈ range n, X i ω) p}) atTop
      (𝓝 ((gaussianReal 0 1).real (Set.Ici z)))

Uses 3

Statement usesBinomial z-score approximation to the motif conservation score

Proof usesStandardized partial sums · De Moivre–Laplace limit theorem, convergence in distribution

DefinitionThe SiPhy rate matrix#✓fully proved

The SiPhy rate matrix Q a b = ω R a b π b for a ≠ b (Garber et al. 2009, Eq. 10), with rows summing to zero: ω times the GTR matrix with exchangeabilities R and base frequencies π.

noncomputable def siphyRate (ω : ℝ) (R : Matrix ι ι ℝ) (π : ι → ℝ) : Matrix ι ι ℝ :=
  ω • gtrRate π R

Uses 1 · Used by 6

Statement usesGeneral time-reversible (GTR) rate matrix

Used byThe rate update maximizes Eq. 6 over ω > 0 · The rate update is the unique maximizer · The constraint-vector update is the unique maximizer of Eq. 6 · Eq. 6 for the SiPhy matrix · π is the equilibrium of the SiPhy matrix · SiPhy matrix is a rate matrix

TheoremSiPhy matrix is a rate matrix#✓fully proved

With ω ≥ 0, nonnegative R and nonnegative π, the SiPhy matrix is a rate matrix.

theorem isRateMatrix_siphyRate {ω : ℝ} {R : Matrix ι ι ℝ} {π : ι → ℝ} (hω : 0 ≤ ω)
    (hR : ∀ a b, 0 ≤ R a b) (hπ : ∀ b, 0 ≤ π b) : IsRateMatrix (siphyRate ω R π)

Uses 4

Statement usesThe SiPhy rate matrix · Rate matrix

Proof usesGeneral time-reversible (GTR) rate matrix · GTR matrix is a rate matrix

Theoremπ is the equilibrium of the SiPhy matrix#✓fully proved

For symmetric R it is in detailed balance with π, for every ω.

theorem isDetailedBalance_siphyRate (ω : ℝ) {R : Matrix ι ι ℝ} (hR : ∀ a b, R a b = R b a)
    (π : ι → ℝ) : IsDetailedBalance π (siphyRate ω R π)

Uses 4

Statement usesThe SiPhy rate matrix · Detailed balance

Proof usesGeneral time-reversible (GTR) rate matrix · GTR is reversible

DefinitionThe expected complete-data log-likelihood#✓fully proved

The expected complete-data log-likelihood of a rate matrix Q and root distribution π (Garber et al. 2009, Eq. 6): ∑_{a ≠ b} n a b log Q a b + ∑ a, τ a Q a a + ∑ b, r b log π b, for expected substitution counts n, expected state durations τ and the root posterior r.

noncomputable def expectedLogLik (n : Matrix ι ι ℝ) (τ r : ι → ℝ) (Q : Matrix ι ι ℝ)
    (π : ι → ℝ) : ℝ :=
  ∑ a, ∑ b, (if a = b then 0 else n a b * log (Q a b)) + ∑ a, τ a * Q a a +
    ∑ b, r b * log (π b)

Used by 4

Used byThe rate update maximizes Eq. 6 over ω > 0 · The rate update is the unique maximizer · The constraint-vector update is the unique maximizer of Eq. 6 · Eq. 6 for the SiPhy matrix

DefinitionExpected total number of substitutions#✓fully proved

The expected total number of substitutions N = ∑_{a ≠ b} n a b.

def totalCount (n : Matrix ι ι ℝ) : ℝ := ∑ a, ∑ b, if a = b then 0 else n a b

Used by 5

Used byThe rate update maximizes Eq. 6 over ω > 0 · The rate update is the unique maximizer · The constraint-vector update is the unique maximizer of Eq. 6 · Eq. 6 for the SiPhy matrix · The SiPhy rate update

DefinitionWeight of a state: substitutions into it plus root posterior#✓fully proved

The weight c b = ∑_{a ≠ b} n a b + r b of state b: substitutions into b plus the root posterior of b.

def inCount (n : Matrix ι ι ℝ) (r : ι → ℝ) (b : ι) : ℝ :=
  ∑ a, (if a = b then 0 else n a b) + r b

Used by 5

Used byThe rate update maximizes Eq. 6 over ω > 0 · The rate update is the unique maximizer · The constraint-vector update is the unique maximizer of Eq. 6 · Eq. 6 for the SiPhy matrix · The SiPhy constraint-vector update

DefinitionTime-weighted exchange rate into a state#✓fully proved

The time-weighted exchange rate into b, e b = ∑_{a ≠ b} τ a R a b.

def exitWeight (τ : ι → ℝ) (R : Matrix ι ι ℝ) (b : ι) : ℝ :=
  ∑ a, if a = b then 0 else τ a * R a b

Used by 6

Used byThe rate update maximizes Eq. 6 over ω > 0 · The rate update is the unique maximizer · The constraint-vector update is the unique maximizer of Eq. 6 · Eq. 6 for the SiPhy matrix · The SiPhy rate update · The SiPhy constraint-vector update

DefinitionPart of the SiPhy objective depending on the constraint vector#✓fully proved

The part of Eq. 6 that depends on π (for fixed ω): ∑ b, (c b * log (π b) - d b * π b).

noncomputable def piObjective (c d π : ι → ℝ) : ℝ := ∑ b, (c b * log (π b) - d b * π b)

Used by 5

Used byThe rate update maximizes Eq. 6 over ω > 0 · The rate update is the unique maximizer · The constraint-vector update is the unique maximizer of Eq. 6 · Eq. 6 for the SiPhy matrix · The π update is the unique maximizer

DefinitionConstant \(n \log R\) term of the SiPhy objective#✓fully proved

The n log R constant of Eq. 6.

noncomputable def exchangeTerm (n R : Matrix ι ι ℝ) : ℝ :=
  ∑ a, ∑ b, if a = b then 0 else n a b * log (R a b)

Used by 4

Used byThe rate update maximizes Eq. 6 over ω > 0 · The rate update is the unique maximizer · The constraint-vector update is the unique maximizer of Eq. 6 · Eq. 6 for the SiPhy matrix

TheoremEq. 6 for the SiPhy matrix#✓fully proved

For ω > 0, positive off-diagonal R and positive π, expectedLogLik = N log ω + ∑_{a ≠ b} n a b log R a b + piObjective c (ω e) π.

theorem expectedLogLik_siphyRate (n : Matrix ι ι ℝ) (τ r : ι → ℝ) {ω : ℝ}
    {R : Matrix ι ι ℝ} {π : ι → ℝ} (hω : 0 < ω) (hR : ∀ a b, a ≠ b → 0 < R a b)
    (hπ : ∀ b, 0 < π b) :
    expectedLogLik n τ r (siphyRate ω R π) π =
      totalCount n * log ω + exchangeTerm n R +
        piObjective (inCount n r) (fun b => ω * exitWeight τ R b) π

Uses 8 · Used by 3

Statement usesConstant \(n \log R\) term of the SiPhy objective · Time-weighted exchange rate into a state · The expected complete-data log-likelihood · Weight of a state: substitutions into it plus root posterior · Part of the SiPhy objective depending on the constraint vector · The SiPhy rate matrix · Expected total number of substitutions

Proof usesGeneral time-reversible (GTR) rate matrix

Used byThe rate update maximizes Eq. 6 over ω > 0 · The rate update is the unique maximizer · The constraint-vector update is the unique maximizer of Eq. 6

DefinitionThe SiPhy rate update#✓fully proved

The SiPhy rate update (Eq. 7, for fixed π): ω = N / ∑ b, e b π b.

noncomputable def omegaUpdate (n : Matrix ι ι ℝ) (τ : ι → ℝ) (R : Matrix ι ι ℝ)
    (π : ι → ℝ) : ℝ :=
  totalCount n / ∑ b, exitWeight τ R b * π b

Uses 2 · Used by 2

Statement usesTime-weighted exchange rate into a state · Expected total number of substitutions

Used byThe rate update maximizes Eq. 6 over ω > 0 · The rate update is the unique maximizer

TheoremThe rate update maximizes Eq. 6 over ω > 0#✓fully proved

The rate update maximizes Eq. 6 over ω > 0 for a fixed positive π, when the expected number of substitutions N and the time-weighted rate ∑ b, e b π b are positive.

theorem expectedLogLik_le_omegaUpdate (n : Matrix ι ι ℝ) (τ r : ι → ℝ) {R : Matrix ι ι ℝ}
    {π : ι → ℝ} (hR : ∀ a b, a ≠ b → 0 < R a b) (hπ : ∀ b, 0 < π b) (hN : 0 < totalCount n)
    (hD : 0 < ∑ b, exitWeight τ R b * π b) {ω : ℝ} (hω : 0 < ω) :
    expectedLogLik n τ r (siphyRate ω R π) π ≤
      expectedLogLik n τ r (siphyRate (omegaUpdate n τ R π) R π) π

Uses 9

Statement usesTime-weighted exchange rate into a state · The expected complete-data log-likelihood · The SiPhy rate update · The SiPhy rate matrix · Expected total number of substitutions

Proof usesConstant \(n \log R\) term of the SiPhy objective · Eq. 6 for the SiPhy matrix · Weight of a state: substitutions into it plus root posterior · Part of the SiPhy objective depending on the constraint vector

TheoremThe rate update is the unique maximizer#✓fully proved

Any other ω > 0 gives a strictly smaller value of Eq. 6.

theorem expectedLogLik_lt_omegaUpdate (n : Matrix ι ι ℝ) (τ r : ι → ℝ) {R : Matrix ι ι ℝ}
    {π : ι → ℝ} (hR : ∀ a b, a ≠ b → 0 < R a b) (hπ : ∀ b, 0 < π b) (hN : 0 < totalCount n)
    (hD : 0 < ∑ b, exitWeight τ R b * π b) {ω : ℝ} (hω : 0 < ω)
    (hne : ω ≠ omegaUpdate n τ R π) :
    expectedLogLik n τ r (siphyRate ω R π) π <
      expectedLogLik n τ r (siphyRate (omegaUpdate n τ R π) R π) π

Uses 9

Statement usesTime-weighted exchange rate into a state · The expected complete-data log-likelihood · The SiPhy rate update · The SiPhy rate matrix · Expected total number of substitutions

Proof usesConstant \(n \log R\) term of the SiPhy objective · Eq. 6 for the SiPhy matrix · Weight of a state: substitutions into it plus root posterior · Part of the SiPhy objective depending on the constraint vector

TheoremThe Lagrange multiplier of the π update exists and is unique#✓fully proved

For positive c and nonnegative d on a nonempty finite alphabet there is exactly one γ with d b + γ > 0 for all b and ∑ b, c b / (d b + γ) = 1.

theorem existsUnique_lagrange [Nonempty ι] {c d : ι → ℝ} (hc : ∀ b, 0 < c b)
    (hd : ∀ b, 0 ≤ d b) :
    ∃! γ : ℝ, (∀ b, 0 < d b + γ) ∧ ∑ b, c b / (d b + γ) = 1

Used by 2

Used byThe constraint-vector update is the unique maximizer of Eq. 6 · The SiPhy constraint-vector update

TheoremThe π update is the unique maximizer#✓fully proved

The π update is the unique maximizer of piObjective c d over the positive probability vectors: with γ as in existsUnique_lagrange, every other positive π summing to one has a strictly smaller objective than b ↦ c b / (d b + γ).

theorem piObjective_lt {c d : ι → ℝ} {γ : ℝ} (hc : ∀ b, 0 < c b) (hγ : ∀ b, 0 < d b + γ)
    (hsum : ∑ b, c b / (d b + γ) = 1) {π : ι → ℝ} (hπ : ∀ b, 0 < π b) (hπs : ∑ b, π b = 1)
    (hne : π ≠ fun b => c b / (d b + γ)) :
    piObjective c d π < piObjective c d (fun b => c b / (d b + γ))

Uses 1 · Used by 1

Statement usesPart of the SiPhy objective depending on the constraint vector

Used byThe constraint-vector update is the unique maximizer of Eq. 6

DefinitionThe SiPhy constraint-vector update#✓fully proved

The SiPhy constraint-vector update (Eq. 8, for fixed ω): π b = c b / (ω e b + γ), with γ the Lagrange multiplier of existsUnique_lagrange.

noncomputable def piUpdate [Nonempty ι] (n : Matrix ι ι ℝ) (τ r : ι → ℝ) (ω : ℝ)
    (R : Matrix ι ι ℝ) (hc : ∀ b, 0 < inCount n r b) (hd : ∀ b, 0 ≤ ω * exitWeight τ R b)
    (b : ι) : ℝ :=
  inCount n r b / (ω * exitWeight τ R b + (existsUnique_lagrange hc hd).exists.choose)

Uses 3 · Used by 1

Statement usesThe Lagrange multiplier of the π update exists and is unique · Time-weighted exchange rate into a state · Weight of a state: substitutions into it plus root posterior

Used byThe constraint-vector update is the unique maximizer of Eq. 6

TheoremThe constraint-vector update is the unique maximizer of Eq. 6#✓fully proved

The constraint-vector update is the unique maximizer of Eq. 6 over the positive probability vectors π (the rate matrix ω R π and the root distribution both use π), for fixed ω > 0, positive off-diagonal R and positive weights c.

theorem expectedLogLik_lt_piUpdate [Nonempty ι] (n : Matrix ι ι ℝ) (τ r : ι → ℝ) {ω : ℝ}
    {R : Matrix ι ι ℝ} (hω : 0 < ω) (hR : ∀ a b, a ≠ b → 0 < R a b)
    (hc : ∀ b, 0 < inCount n r b) (hd : ∀ b, 0 ≤ ω * exitWeight τ R b) {π : ι → ℝ}
    (hπ : ∀ b, 0 < π b) (hπs : ∑ b, π b = 1) (hne : π ≠ piUpdate n τ r ω R hc hd) :
    expectedLogLik n τ r (siphyRate ω R π) π <
      expectedLogLik n τ r (siphyRate ω R (piUpdate n τ r ω R hc hd))
        (piUpdate n τ r ω R hc hd)

Uses 11

Statement usesTime-weighted exchange rate into a state · The expected complete-data log-likelihood · Weight of a state: substitutions into it plus root posterior · The SiPhy constraint-vector update · The SiPhy rate matrix

Proof usesConstant \(n \log R\) term of the SiPhy objective · The Lagrange multiplier of the π update exists and is unique · Eq. 6 for the SiPhy matrix · Part of the SiPhy objective depending on the constraint vector · The π update is the unique maximizer · Expected total number of substitutions

DefinitionLeaf set meeting both sides of a tree edge#✓fully proved

Whether the leaf set S meets both sides of an edge with leaf set B below it, inside a tree with leaf set U: S ∩ B and S ∩ (U \ B) are nonempty.

def Separates (U S B : Finset L) : Prop := (S ∩ B).Nonempty ∧ (S ∩ (U \ B)).Nonempty

Used by 8

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

DefinitionNonnegative edge lengths of a tree#✓fully proved

Edge lengths are nonnegative: every dart's undirected edge has nonnegative length.

def NonnegWeights (T : UnrootedBinaryTree X) (w : Sym2 T.V → ℝ) : Prop :=
  ∀ t : T.G.Dart, 0 ≤ w t.edge

Uses 1 · Used by 6

Statement usesUnrooted binary phylogenetic tree

Used byNormalized branch length score is at most one for nonnegative lengths · Normalized branch length score is nonnegative for nonnegative lengths · Branch length score is at most the tree length for nonnegative lengths · Monotonicity · Branch length score is nonnegative for nonnegative edge lengths · Subadditivity

DefinitionTotal branch length of a tree#✓fully proved

The total branch length: half the sum of the edge lengths over the darts, since each undirected edge is traversed once in each direction.

noncomputable def totalLength (T : UnrootedBinaryTree X) (w : Sym2 T.V → ℝ) : ℝ :=
  (1 / 2) * ∑ t : T.G.Dart, w t.edge

Uses 1 · Used by 5

Statement usesUnrooted binary phylogenetic tree

Used byNormalized branch length score · Normalized branch length score is at most one for nonnegative lengths · Normalized branch length score is nonnegative for nonnegative lengths · Branch length score is at most the tree length for nonnegative lengths · All species give the whole tree

DefinitionThe Branch Length Score#✓fully proved

The Branch Length Score (unnormalized): the total branch length of the smallest subtree of T connecting the leaves S, as half the sum over the darts of the edge length times the indicator that S meets both sides (edgeSide) of the dart's edge.

noncomputable def bls (S : Finset X) (T : UnrootedBinaryTree X) (w : Sym2 T.V → ℝ) : ℝ :=
  (1 / 2) * ∑ t : T.G.Dart, w t.edge *
    if Separates Finset.univ S (edgeSide T t.fst t.snd) then 1 else 0

Uses 3 · Used by 10

Statement usesLeaf set meeting both sides of a tree edge · Side of a tree edge containing a vertex · Unrooted binary phylogenetic tree

Used byBranch length score of the empty set is zero · Normalized branch length score · Normalized branch length score is at most one for nonnegative lengths · Normalized branch length score is nonnegative for nonnegative lengths · 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

DefinitionNormalized branch length score#✓fully proved

The normalized Branch Length Score, bls S T w / totalLength T w, as reported by Kheradpour et al. (a fraction of the total branch length).

noncomputable def blsFrac (S : Finset X) (T : UnrootedBinaryTree X) (w : Sym2 T.V → ℝ) : ℝ :=
  bls S T w / totalLength T w

Uses 3 · Used by 2

Statement usesThe Branch Length Score · Total branch length of a tree · Unrooted binary phylogenetic tree

Used byNormalized branch length score is at most one for nonnegative lengths · Normalized branch length score is nonnegative for nonnegative lengths

TheoremBranch length score is nonnegative for nonnegative edge lengths#✓fully proved

The BLS is nonnegative for nonnegative edge lengths.

theorem bls_nonneg (S : Finset X) (T : UnrootedBinaryTree X) (w : Sym2 T.V → ℝ)
    (hw : NonnegWeights T w) : 0 ≤ bls S T w

Uses 5 · Used by 1

Statement usesNonnegative edge lengths of a tree · The Branch Length Score · Unrooted binary phylogenetic tree

Proof usesLeaf set meeting both sides of a tree edge · Side of a tree edge containing a vertex

Used byNormalized branch length score is nonnegative for nonnegative lengths

TheoremBranch length score is at most the tree length for nonnegative lengths#✓fully proved

The BLS is at most the total branch length.

theorem bls_le_totalLength (S : Finset X) (T : UnrootedBinaryTree X) (w : Sym2 T.V → ℝ)
    (hw : NonnegWeights T w) : bls S T w ≤ totalLength T w

Uses 6 · Used by 1

Statement usesNonnegative edge lengths of a tree · The Branch Length Score · Total branch length of a tree · Unrooted binary phylogenetic tree

Proof usesLeaf set meeting both sides of a tree edge · Side of a tree edge containing a vertex

Used byNormalized branch length score is at most one for nonnegative lengths

TheoremMonotonicity#✓fully proved

With nonnegative edge lengths, more conserving species never lower the BLS.

theorem bls_mono {S S' : Finset X} (h : S ⊆ S') (T : UnrootedBinaryTree X)
    (w : Sym2 T.V → ℝ) (hw : NonnegWeights T w) : bls S T w ≤ bls S' T w

Uses 5

Statement usesNonnegative edge lengths of a tree · The Branch Length Score · Unrooted binary phylogenetic tree

Proof usesLeaf set meeting both sides of a tree edge · Side of a tree edge containing a vertex

TheoremBranch length score of the empty set is zero#✓fully proved

The BLS of the empty set is 0.

theorem bls_empty (T : UnrootedBinaryTree X) (w : Sym2 T.V → ℝ) : bls ∅ T w = 0

Uses 4

Statement usesThe Branch Length Score · Unrooted binary phylogenetic tree

Proof usesLeaf set meeting both sides of a tree edge · Side of a tree edge containing a vertex

TheoremA single species has BLS 0#✓fully proved

A single species has BLS 0 (a motif present in one genome is not conserved).

theorem bls_singleton (x : X) (T : UnrootedBinaryTree X) (w : Sym2 T.V → ℝ) :
    bls {x} T w = 0

Uses 4

Statement usesThe Branch Length Score · Unrooted binary phylogenetic tree

Proof usesLeaf set meeting both sides of a tree edge · Side of a tree edge containing a vertex

TheoremAll species give the whole tree#✓fully proved

The BLS of the set of all leaves is the total branch length.

theorem bls_leaves (a : X) (T : UnrootedBinaryTree X) (w : Sym2 T.V → ℝ) :
    bls Finset.univ T w = totalLength T w

Uses 12

Statement usesThe Branch Length Score · Total branch length of a tree · Unrooted binary phylogenetic tree

Proof usesLeaf set meeting both sides of a tree edge · The two sides of a tree edge are complementary · Side of a tree edge containing a vertex · Edge splits of a tree · 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

TheoremSubadditivity#✓fully proved

For sets of species S, S' that share a species, the subtree connecting S ∪ S' is at most as long as the two subtrees together.

theorem bls_union_le {S S' : Finset X} (hSS : (S ∩ S').Nonempty) (T : UnrootedBinaryTree X)
    (w : Sym2 T.V → ℝ) (hw : NonnegWeights T w) :
    bls (S ∪ S') T w ≤ bls S T w + bls S' T w

Uses 5

Statement usesNonnegative edge lengths of a tree · The Branch Length Score · Unrooted binary phylogenetic tree

Proof usesLeaf set meeting both sides of a tree edge · Side of a tree edge containing a vertex

TheoremNormalized branch length score is nonnegative for nonnegative lengths#✓fully proved

The normalized BLS is nonnegative.

theorem blsFrac_nonneg (S : Finset X) (T : UnrootedBinaryTree X) (w : Sym2 T.V → ℝ)
    (hw : NonnegWeights T w) : 0 ≤ blsFrac S T w

Uses 6

Statement usesNonnegative edge lengths of a tree · Normalized branch length score · Unrooted binary phylogenetic tree

Proof usesThe Branch Length Score · Branch length score is nonnegative for nonnegative edge lengths · Total branch length of a tree

TheoremNormalized branch length score is at most one for nonnegative lengths#✓fully proved

The normalized BLS is at most 1 when the tree has positive total length.

theorem blsFrac_le_one (S : Finset X) (T : UnrootedBinaryTree X) (w : Sym2 T.V → ℝ)
    (hw : NonnegWeights T w) (hpos : 0 < totalLength T w) : blsFrac S T w ≤ 1

Uses 6

Statement usesNonnegative edge lengths of a tree · Normalized branch length score · Total branch length of a tree · Unrooted binary phylogenetic tree

Proof usesThe Branch Length Score · Branch length score is at most the tree length for nonnegative lengths

TheoremThe side of a pendant edge is the singleton of its leaf#✓fully proved

The taxa whose leaf is closer to the leaf vertex than to its neighbor are exactly that leaf's taxon.

theorem edgeSide_of_leaf (T : UnrootedBinaryTree X) {x : X} {p : T.V}
    (hp : T.G.Adj p (T.label x)) : edgeSide T p (T.label x) = {x}

Uses 2

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

TheoremSum over darts is twice the sum over edges#✓fully proved

A sum over darts of a function of the undirected edge is twice the sum over the edges: the two darts of each edge contribute equally.

theorem dart_sum_edge (T : UnrootedBinaryTree X) (f : Sym2 T.V → ℝ) :
    ∑ t : T.G.Dart, f t.edge = ∑ e ∈ T.G.edgeFinset, 2 * f e

Uses 1

Statement usesUnrooted binary phylogenetic tree

37 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.