Maximum-likelihood ancestral reconstruction

DefinitionNonnegative transition weights on a tree#✓fully proved

All transition weights in the tree are nonnegative.

def NonnegWeights [Zero R] [LE R] : Tree L S R → Prop
  | leaf _ => True
  | node P l Q r => (∀ a b, 0 ≤ P a b) ∧ (∀ a b, 0 ≤ Q a b) ∧ NonnegWeights l ∧ NonnegWeights r

Uses 1 · Used by 5

Statement usesRooted binary tree with transition weights

Used byThe max-product recursion computes the maximal labeling weight · Nonnegativity of max-product pruning · Pupko et al. (2000): joint maximum likelihood · maxPrune bounds the weight of every labeling · Nonnegativity of labeling weights

DefinitionState maximizing a function#✓fully proved

A state maximizing f (ties broken by choice).

noncomputable def argmaxState (f : S → R) : S :=
  (Finite.exists_max f).choose

Used by 6

Used byLikelihood of Pupko's joint reconstruction · Root state of Pupko's reconstruction · The argmax state maximizes the function · Value at the argmax state is the maximum · Pupko's traceback · The traced labeling attains maxPrune

TheoremThe argmax state maximizes the function#✓fully proved

argmaxState f maximizes f.

theorem le_argmaxState (f : S → R) (a : S) : f a ≤ f (argmaxState f)

Uses 1 · Used by 1

Statement usesState maximizing a function

Used byValue at the argmax state is the maximum

TheoremValue at the argmax state is the maximum#✓fully proved

The value at argmaxState f is the maximum univ.sup' of f.

theorem sup'_eq_argmaxState [Fintype S] (f : S → R) :
    univ.sup' univ_nonempty f = f (argmaxState f)

Uses 2 · Used by 2

Statement usesState maximizing a function

Proof usesThe argmax state maximizes the function

Used byLikelihood of Pupko's joint reconstruction · The traced labeling attains maxPrune

DefinitionMax-product pruning recursion#✓fully proved

The max-product (Viterbi) form of Felsenstein's pruning recursion: the largest weight of a labeling of the subtree t given state s at its root.

def maxPrune : Tree L S R → S → R
  | leaf l, s => obs l s
  | node P l Q r, s =>
    (univ.sup' univ_nonempty fun a => P s a * maxPrune l a) *
      (univ.sup' univ_nonempty fun b => Q s b * maxPrune r b)

Uses 1 · Used by 8

Statement usesRooted binary tree with transition weights

Used byLikelihood of Pupko's joint reconstruction · Root state of Pupko's reconstruction · The max-product recursion computes the maximal labeling weight · Nonnegativity of max-product pruning · Pupko et al. (2000): joint maximum likelihood · Pupko's traceback · maxPrune bounds the weight of every labeling · The traced labeling attains maxPrune

DefinitionPupko's traceback#✓fully proved

Pupko's traceback: given the state s of the root of t, label each child with a state maximizing the transition weight times the child's maxPrune, and recurse.

noncomputable def traceback : (t : Tree L S R) → S → Labeling t
  | leaf _, _ => PUnit.unit
  | node P l Q r, s =>
    let a := argmaxState fun a => P s a * maxPrune obs l a
    let b := argmaxState fun b => Q s b * maxPrune obs r b
    ((a, traceback l a), (b, traceback r b))

Uses 4 · Used by 3

Statement usesState maximizing a function · Max-product pruning recursion · Labeling of the non-root nodes of a tree · Rooted binary tree with transition weights

Used byThe max-product recursion computes the maximal labeling weight · Pupko's joint reconstruction · The traced labeling attains maxPrune

TheoremNonnegativity of max-product pruning#✓fully proved

With nonnegative weights, maxPrune is nonnegative.

theorem maxPrune_nonneg (hobs : ∀ l s, 0 ≤ obs l s) :
    ∀ (t : Tree L S R), NonnegWeights t → ∀ s, 0 ≤ maxPrune obs t s

Uses 3 · Used by 1

Statement usesNonnegative transition weights on a tree · Max-product pruning recursion · Rooted binary tree with transition weights

Used bymaxPrune bounds the weight of every labeling

TheoremThe traced labeling attains maxPrune#✓fully proved

No sign condition is needed.

theorem weight_traceback :
    ∀ (t : Tree L S R) (s : S), weight obs t s (traceback obs t s) = maxPrune obs t s

Uses 7 · Used by 2

Statement usesMax-product pruning recursion · Pupko's traceback · Rooted binary tree with transition weights · Weight of a tree labeling

Proof usesState maximizing a function · Value at the argmax state is the maximum · Labeling of the non-root nodes of a tree

Used byLikelihood of Pupko's joint reconstruction · The max-product recursion computes the maximal labeling weight

TheoremNonnegativity of labeling weights#✓fully proved

With nonnegative weights, every labeling has nonnegative weight.

theorem weight_nonneg (hobs : ∀ l s, 0 ≤ obs l s) :
    ∀ (t : Tree L S R), NonnegWeights t → ∀ (s : S) (z : Labeling t), 0 ≤ weight obs t s z

Uses 4 · Used by 1

Statement usesNonnegative transition weights on a tree · Labeling of the non-root nodes of a tree · Rooted binary tree with transition weights · Weight of a tree labeling

Used bymaxPrune bounds the weight of every labeling

TheoremmaxPrune bounds the weight of every labeling#✓fully proved

maxPrune bounds the weight of every labeling (nonnegative weights).

theorem weight_le_maxPrune (hobs : ∀ l s, 0 ≤ obs l s) :
    ∀ (t : Tree L S R), NonnegWeights t → ∀ (s : S) (z : Labeling t),
      weight obs t s z ≤ maxPrune obs t s

Uses 7 · Used by 2

Statement usesNonnegative transition weights on a tree · Max-product pruning recursion · Labeling of the non-root nodes of a tree · Rooted binary tree with transition weights · Weight of a tree labeling

Proof usesNonnegativity of max-product pruning · Nonnegativity of labeling weights

Used byThe max-product recursion computes the maximal labeling weight · Pupko et al. (2000): joint maximum likelihood

TheoremThe max-product recursion computes the maximal labeling weight#✓fully proved

maxPrune obs t s is the maximum over all labelings z of the non-root nodes of weight obs t s z.

theorem maxPrune_eq_sup' (hobs : ∀ l s, 0 ≤ obs l s) (t : Tree L S R) (ht : NonnegWeights t)
    (s : S) :
    maxPrune obs t s = univ.sup' ⟨traceback obs t s, mem_univ _⟩ (weight obs t s)

Uses 8

Statement usesNonnegative transition weights on a tree · Max-product pruning recursion · Pupko's traceback · Labeling of the non-root nodes of a tree · Rooted binary tree with transition weights · Weight of a tree labeling

Proof usesmaxPrune bounds the weight of every labeling · The traced labeling attains maxPrune

DefinitionRoot state of Pupko's reconstruction#✓fully proved

The root state of Pupko's reconstruction: it maximizes π s * maxPrune obs t s.

noncomputable def jointRoot (t : Tree L S R) (π : S → R) : S :=
  argmaxState fun s => π s * maxPrune obs t s

Uses 3 · Used by 1

Statement usesState maximizing a function · Max-product pruning recursion · Rooted binary tree with transition weights

Used byPupko's joint reconstruction

DefinitionPupko's joint reconstruction#✓fully proved

The root state jointRoot and the traced labeling.

noncomputable def pupko (t : Tree L S R) (π : S → R) : S × Labeling t :=
  (jointRoot obs t π, traceback obs t (jointRoot obs t π))

Uses 4 · Used by 2

Statement usesRoot state of Pupko's reconstruction · Pupko's traceback · Labeling of the non-root nodes of a tree · Rooted binary tree with transition weights

Used byLikelihood of Pupko's joint reconstruction · Pupko et al. (2000): joint maximum likelihood

TheoremLikelihood of Pupko's joint reconstruction#✓fully proved

The likelihood of Pupko's reconstruction is max_s π s * maxPrune obs t s.

theorem jointLik_pupko (t : Tree L S R) (π : S → R) :
    π (pupko obs t π).1 * weight obs t (pupko obs t π).1 (pupko obs t π).2 =
      univ.sup' univ_nonempty fun s => π s * maxPrune obs t s

Uses 8 · Used by 1

Statement usesMax-product pruning recursion · Pupko's joint reconstruction · Labeling of the non-root nodes of a tree · Rooted binary tree with transition weights · Weight of a tree labeling

Proof usesState maximizing a function · Value at the argmax state is the maximum · The traced labeling attains maxPrune

Used byPupko et al. (2000): joint maximum likelihood

TheoremPupko et al. (2000): joint maximum likelihood#✓fully proved

With nonnegative root, transition and leaf weights, no root state s and labeling z of the non-root nodes has larger joint likelihood π s * weight obs t s z than Pupko's reconstruction.

theorem pupko_isJointML (hobs : ∀ l s, 0 ≤ obs l s) (t : Tree L S R) (ht : NonnegWeights t)
    (π : S → R) (hπ : ∀ s, 0 ≤ π s) (s : S) (z : Labeling t) :
    π s * weight obs t s z ≤
      π (pupko obs t π).1 * weight obs t (pupko obs t π).1 (pupko obs t π).2

Uses 8

Statement usesNonnegative transition weights on a tree · Pupko's joint reconstruction · Labeling of the non-root nodes of a tree · Rooted binary tree with transition weights · Weight of a tree labeling

Proof usesLikelihood of Pupko's joint reconstruction · Max-product pruning recursion · maxPrune bounds the weight of every labeling

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.