ChromHMM chromatin-state model

27 fully proved

The factored emission update

DefinitionWeight of binary vectors with a mark present#✓fully proved

The weight ∑ o with o j = true, c o of the binary vectors with mark j present.

noncomputable def onesCount (c : (Fin d → Bool) → ℝ) (j : Fin d) : ℝ :=
  ∑ o, if o j then c o else 0

Used by 8

Used byThe ChromHMM update maximizes Q(· | θ) · Factored per-mark update · Factored update is below one · Positivity of the factored update · The ChromHMM update is a valid parameter · Expected number of bins in a state with a mark present · Expected product-Bernoulli log-likelihood splits over marks · The factored update maximizes the expected log-likelihood

DefinitionWeight of binary vectors with a mark absent#✓fully proved

The weight ∑ o with o j = false, c o of the binary vectors with mark j absent.

noncomputable def zerosCount (c : (Fin d → Bool) → ℝ) (j : Fin d) : ℝ :=
  ∑ o, if o j then 0 else c o

Used by 8

Used byThe ChromHMM update maximizes Q(· | θ) · Factored per-mark update · Factored update is below one · Positivity of the factored update · The ChromHMM update is a valid parameter · Expected number of bins in a state with a mark absent · Expected product-Bernoulli log-likelihood splits over marks · The factored update maximizes the expected log-likelihood

DefinitionFactored per-mark update#✓fully proved

The factored (per-mark) update ones j / (ones j + zeros j).

noncomputable def factoredUpdate (c : (Fin d → Bool) → ℝ) (j : Fin d) : ℝ :=
  onesCount c j / (onesCount c j + zerosCount c j)

Uses 2 · Used by 4

Statement usesWeight of binary vectors with a mark present · Weight of binary vectors with a mark absent

Used byFactored update is below one · Positivity of the factored update · The ChromHMM M-step · The factored update maximizes the expected log-likelihood

TheoremProduct of Bernoulli distributions sums to one#✓fully proved

A product of Bernoulli distributions sums to one over the binary vectors, for every parameter vector p (the identity is algebraic: ∏ j, (p j + (1 - p j)) = 1).

theorem sum_bernPMF (p : Fin d → ℝ) : ∑ x, bernPMF p x = 1

Uses 1 · Used by 1

Statement usesProduct Bernoulli probability mass function

Used byValid ChromHMM parameters give a valid HMM

TheoremExpected product-Bernoulli log-likelihood splits over marks#✓fully proved

The expected log-likelihood of weighted binary vectors under a product of Bernoulli distributions with parameters in (0, 1) splits over the marks.

theorem sum_mul_log_bernPMF (c : (Fin d → Bool) → ℝ) {p : Fin d → ℝ} (hp0 : ∀ j, 0 < p j)
    (hp1 : ∀ j, p j < 1) :
    ∑ o, c o * log (bernPMF p o) =
      ∑ j, (onesCount c j * log (p j) + zerosCount c j * log (1 - p j))

Uses 3 · Used by 1

Statement usesWeight of binary vectors with a mark present · Weight of binary vectors with a mark absent · Product Bernoulli probability mass function

Used byThe factored update maximizes the expected log-likelihood

TheoremThe factored update maximizes the expected log-likelihood#✓fully proved

The factored update maximizes the expected log-likelihood over all products of Bernoulli distributions with parameters in (0, 1), for nonnegative weights c in which every mark is both present and absent with positive weight.

theorem sum_mul_log_bernPMF_le_factoredUpdate {c : (Fin d → Bool) → ℝ} (hc : ∀ o, 0 ≤ c o)
    (h1 : ∀ j, 0 < onesCount c j) (h0 : ∀ j, 0 < zerosCount c j) {p : Fin d → ℝ}
    (hp0 : ∀ j, 0 < p j) (hp1 : ∀ j, p j < 1) :
    ∑ o, c o * log (bernPMF p o) ≤ ∑ o, c o * log (bernPMF (factoredUpdate c) o)

Uses 5 · Used by 1

Statement usesFactored per-mark update · Weight of binary vectors with a mark present · Weight of binary vectors with a mark absent · Product Bernoulli probability mass function

Proof usesExpected product-Bernoulli log-likelihood splits over marks

Used byThe ChromHMM update maximizes Q(· | θ)

TheoremPositivity of the factored update#✓fully proved

The factored update is positive when both counts are.

theorem factoredUpdate_pos {c : (Fin d → Bool) → ℝ} (h1 : ∀ j, 0 < onesCount c j)
    (h0 : ∀ j, 0 < zerosCount c j) (j : Fin d) : 0 < factoredUpdate c j

Uses 3 · Used by 1

Statement usesFactored per-mark update · Weight of binary vectors with a mark present · Weight of binary vectors with a mark absent

Used byThe ChromHMM update is a valid parameter

TheoremFactored update is below one#✓fully proved

The factored update is below one when both counts are positive.

theorem factoredUpdate_lt_one {c : (Fin d → Bool) → ℝ} (h1 : ∀ j, 0 < onesCount c j)
    (h0 : ∀ j, 0 < zerosCount c j) (j : Fin d) : factoredUpdate c j < 1

Uses 3 · Used by 1

Statement usesFactored per-mark update · Weight of binary vectors with a mark present · Weight of binary vectors with a mark absent

Used byThe ChromHMM update is a valid parameter

The model

StructureChromHMM parameters#✓fully proved

ChromHMM parameters: initial and transition weights, and the presence probability of each mark in each state.

structure Params (S : Type*) (d : ℕ) where
  /-- The initial weight of each state. -/
  init : S → ℝ
  /-- The transition weights. -/
  trans : S → S → ℝ
  /-- The probability that mark `j` is present in state `s`. -/
  prob : S → Fin d → ℝ

Used by 10

Used byThe ChromHMM update maximizes Q(· | θ) · One ChromHMM step on rich data · EM log-likelihood as a sum of HMM log-likelihoods · The ChromHMM M-step · The ChromHMM update is a valid parameter · HMM of ChromHMM parameters · Valid ChromHMM parameters give a valid HMM · Valid HMM built from a valid ChromHMM parameter · Valid ChromHMM parameters · Parameter space of ChromHMM

DefinitionHMM of ChromHMM parameters#✓fully proved

The HMM of ChromHMM parameters: emissions are products of Bernoulli distributions.

noncomputable def Params.toHMM (θ : Params S d) : HMM S (Fin d → Bool) ℝ where
  init := θ.init
  trans := θ.trans
  emit s o := bernPMF (θ.prob s) o

Uses 3 · Used by 3

Statement usesChromHMM parameters · Product Bernoulli probability mass function · Hidden Markov model

Used byEM log-likelihood as a sum of HMM log-likelihoods · Valid ChromHMM parameters give a valid HMM · Valid HMM built from a valid ChromHMM parameter

StructureValid ChromHMM parameters#✓fully proved

Valid parameters: positive initial and transition distributions, mark probabilities in (0, 1).

structure Params.Valid (θ : Params S d) : Prop where
  init_pos : ∀ s, 0 < θ.init s
  init_sum : ∑ s, θ.init s = 1
  trans_pos : ∀ s s', 0 < θ.trans s s'
  trans_sum : ∀ s, ∑ s', θ.trans s s' = 1
  prob_pos : ∀ s j, 0 < θ.prob s j
  prob_lt_one : ∀ s j, θ.prob s j < 1

Uses 1 · Used by 7

Statement usesChromHMM parameters

Used byThe ChromHMM update maximizes Q(· | θ) · One ChromHMM step on rich data · EM log-likelihood as a sum of HMM log-likelihoods · The ChromHMM update is a valid parameter · Valid ChromHMM parameters give a valid HMM · Valid HMM built from a valid ChromHMM parameter · Parameter space of ChromHMM

AbbreviationParameter space of ChromHMM#✓fully proved

The parameter space of ChromHMM.

abbrev ValidParams (S : Type*) [Fintype S] (d : ℕ) := {θ : Params S d // θ.Valid}

Uses 2 · Used by 13

Statement usesChromHMM parameters · Valid ChromHMM parameters

Used byThe ChromHMM update maximizes Q(· | θ) · One ChromHMM step on rich data · ChromHMM joint weight of a state path and mark vectors · Positivity of the ChromHMM joint weight · EM log-likelihood as a sum of HMM log-likelihoods · The log-likelihood is monotone along the ChromHMM iterates · Each ChromHMM step does not decrease the log-likelihood · The ChromHMM M-step · The ChromHMM update is a valid parameter · Expected number of bins in a state with a mark present · The factored update in posterior form · Expected number of bins in a state with a mark absent · Valid HMM built from a valid ChromHMM parameter

TheoremValid ChromHMM parameters give a valid HMM#✓fully proved

A valid ChromHMM parameter is a valid HMM.

theorem Params.Valid.toHMM {θ : Params S d} (h : θ.Valid) : BaumWelch.Valid θ.toHMM

Uses 7 · Used by 1

Statement usesChromHMM parameters · Valid ChromHMM parameters · HMM of ChromHMM parameters · Valid hidden Markov model parameters

Proof usesProduct of Bernoulli distributions sums to one · Product Bernoulli probability mass function · Hidden Markov model

Used byValid HMM built from a valid ChromHMM parameter

DefinitionValid HMM built from a valid ChromHMM parameter#✓fully proved

The valid HMM of a valid ChromHMM parameter.

noncomputable def toValidHMM (θ : ValidParams S d) : ValidHMM S (Fin d → Bool) :=
  ⟨θ.1.toHMM, θ.2.toHMM⟩

Uses 8 · Used by 10

Statement usesChromHMM parameters · Valid ChromHMM parameters · Valid ChromHMM parameters give a valid HMM · HMM of ChromHMM parameters · Parameter space of ChromHMM · Valid hidden Markov model parameters · Valid HMMs · Hidden Markov model

Used byThe ChromHMM update maximizes Q(· | θ) · ChromHMM joint weight of a state path and mark vectors · Positivity of the ChromHMM joint weight · The log-likelihood is monotone along the ChromHMM iterates · Each ChromHMM step does not decrease the log-likelihood · The ChromHMM M-step · The ChromHMM update is a valid parameter · Expected number of bins in a state with a mark present · The factored update in posterior form · Expected number of bins in a state with a mark absent

DefinitionChromHMM joint weight of a state path and mark vectors#✓fully proved

The EM model of ChromHMM: the joint weight of a state path and a sequence of mark vectors.

noncomputable def joint (θ : ValidParams S d) (x : ℕ → Fin d → Bool) (z : Fin (T + 1) → S) :
    ℝ :=
  BaumWelch.joint T (toValidHMM θ) x z

Uses 3 · Used by 5

Statement usesParameter space of ChromHMM · Valid HMM built from a valid ChromHMM parameter · The EM model of a hidden Markov model

Used byThe ChromHMM update maximizes Q(· | θ) · Positivity of the ChromHMM joint weight · EM log-likelihood as a sum of HMM log-likelihoods · The log-likelihood is monotone along the ChromHMM iterates · Each ChromHMM step does not decrease the log-likelihood

DefinitionExpected number of bins in a state with a mark present#✓fully proved

The expected number of bins in state s with mark j present.

noncomputable def markOnes (θ : ValidParams S d) (s : S) (j : Fin d) : ℝ :=
  onesCount (emitCount T xs (toValidHMM θ) s) j

Uses 4 · Used by 1

Statement usesParameter space of ChromHMM · Weight of binary vectors with a mark present · Valid HMM built from a valid ChromHMM parameter · Expected emission counts

Used byThe factored update in posterior form

DefinitionExpected number of bins in a state with a mark absent#✓fully proved

The expected number of bins in state s with mark j absent.

noncomputable def markZeros (θ : ValidParams S d) (s : S) (j : Fin d) : ℝ :=
  zerosCount (emitCount T xs (toValidHMM θ) s) j

Uses 4

Statement usesParameter space of ChromHMM · Valid HMM built from a valid ChromHMM parameter · Weight of binary vectors with a mark absent · Expected emission counts

DefinitionThe ChromHMM M-step#✓fully proved

The Baum-Welch initial and transition updates, and the factored emission update prob s j = markOnes / (markOnes + markZeros).

noncomputable def mStep (θ : ValidParams S d) : Params S d where
  init := (BaumWelch.mStep T xs (toValidHMM θ)).init
  trans := (BaumWelch.mStep T xs (toValidHMM θ)).trans
  prob s := factoredUpdate (emitCount T xs (toValidHMM θ) s)

Uses 7 · Used by 2

Statement usesChromHMM parameters · Parameter space of ChromHMM · Factored per-mark update · Valid HMM built from a valid ChromHMM parameter · Expected emission counts · The Baum-Welch M-step · Hidden Markov model

Used byOne ChromHMM step on rich data · The ChromHMM update is a valid parameter

TheoremThe factored update in posterior form#✓fully proved

markOnes s j is the posterior expected number of bins in state s at which mark j is present.

theorem markOnes_eq (θ : ValidParams S d) (s : S) (j : Fin d) :
    markOnes T xs θ s j = ∑ n, ∑ z, post T xs (toValidHMM θ) n z *
      ∑ t : Fin (T + 1), if z t = s ∧ xs n t j = true then 1 else 0

Uses 6

Statement usesParameter space of ChromHMM · Expected number of bins in a state with a mark present · Valid HMM built from a valid ChromHMM parameter · Posterior weight of a state path

Proof usesExpected emission counts · Emission count of a state path

StructureRich data for the ChromHMM M-step#✓fully proved

Data on which the ChromHMM M-step is valid: a sequence, a transition, and every mark both present and absent somewhere.

structure Rich (xs : Fin N → ℕ → Fin d → Bool) : Prop where
  pos : 0 < N
  len : 0 < T
  marks : ∀ j b, ∃ n, ∃ t : Fin (T + 1), xs n t j = b

Used by 5

Used byThe ChromHMM update maximizes Q(· | θ) · One ChromHMM step on rich data · The log-likelihood is monotone along the ChromHMM iterates · Each ChromHMM step does not decrease the log-likelihood · The ChromHMM update is a valid parameter

TheoremThe ChromHMM update is a valid parameter#✓fully proved

The ChromHMM update is a valid parameter on rich data.

theorem mStep_valid (hx : Rich T xs) (θ : ValidParams S d) : (mStep T xs θ).Valid

Uses 26 · Used by 1

Statement usesValid ChromHMM parameters · Rich data for the ChromHMM M-step · Parameter space of ChromHMM · The ChromHMM M-step

Proof usesChromHMM parameters · Factored update is below one · Positivity of the factored update · Weight of binary vectors with a mark present · Valid HMM built from a valid ChromHMM parameter · Weight of binary vectors with a mark absent · Posteriors are probability distributions · Marginal of a latent-variable model · Posterior of a latent-variable model · Valid hidden Markov model parameters · Valid HMMs · Expected emission counts · Expected initial-state counts · The EM model of a hidden Markov model · Emission count of a state path · Initial-state indicator of a state path · Transition count of a state path · Path weight as a product · Posterior weight of a state path · Expected transition count · Hidden Markov model · Joint weight of a state path and the observations

Used byOne ChromHMM step on rich data

DefinitionOne ChromHMM step on rich data#✓fully proved

One ChromHMM step, on rich data.

noncomputable def emStep (hx : Rich T xs) (θ : ValidParams S d) : ValidParams S d :=
  ⟨mStep T xs θ, mStep_valid hx θ⟩

Uses 6 · Used by 3

Statement usesChromHMM parameters · Valid ChromHMM parameters · Rich data for the ChromHMM M-step · Parameter space of ChromHMM · The ChromHMM M-step · The ChromHMM update is a valid parameter

Used byThe ChromHMM update maximizes Q(· | θ) · The log-likelihood is monotone along the ChromHMM iterates · Each ChromHMM step does not decrease the log-likelihood

TheoremPositivity of the ChromHMM joint weight#✓fully proved

The ChromHMM joint weight is positive.

theorem joint_pos (θ : ValidParams S d) (x : ℕ → Fin d → Bool) (z : Fin (T + 1) → S) :
    0 < joint T θ x z

Uses 9 · Used by 2

Statement usesParameter space of ChromHMM · ChromHMM joint weight of a state path and mark vectors

Proof usesValid HMM built from a valid ChromHMM parameter · Valid hidden Markov model parameters · Valid HMMs · The EM model of a hidden Markov model · Path weight as a product · Hidden Markov model · Joint weight of a state path and the observations

Used byThe log-likelihood is monotone along the ChromHMM iterates · Each ChromHMM step does not decrease the log-likelihood

TheoremThe ChromHMM update maximizes Q(· | θ)#✓fully proved

The ChromHMM update maximizes Q(· | θ) over all valid product-Bernoulli HMMs.

theorem emQ_le_emStep (hx : Rich T xs) (θ' θ : ValidParams S d) :
    emQ (joint T) xs θ' θ ≤ emQ (joint T) xs (emStep T xs hx θ) θ

Uses 29 · Used by 2

Statement usesRich data for the ChromHMM M-step · Parameter space of ChromHMM · One ChromHMM step on rich data · ChromHMM joint weight of a state path and mark vectors · The EM objective

Proof usesChromHMM parameters · Valid ChromHMM parameters · Weight of binary vectors with a mark present · The factored update maximizes the expected log-likelihood · Valid HMM built from a valid ChromHMM parameter · Weight of binary vectors with a mark absent · The weighted log-likelihood is bounded by its value at the normalized counts · Posteriors are probability distributions · Marginal of a latent-variable model · Posterior of a latent-variable model · Valid hidden Markov model parameters · Valid HMMs · The Baum-Welch objective in terms of expected counts · Expected emission counts · Expected initial-state counts · The EM model of a hidden Markov model · Emission count of a state path · Initial-state indicator of a state path · Transition count of a state path · Path weight as a product · Posterior weight of a state path · Expected transition count · Hidden Markov model · Joint weight of a state path and the observations

Used byThe log-likelihood is monotone along the ChromHMM iterates · Each ChromHMM step does not decrease the log-likelihood

TheoremEach ChromHMM step does not decrease the log-likelihood#✓fully proved

Each ChromHMM step does not decrease the log-likelihood.

theorem logLik_le_emStep (hx : Rich T xs) (θ : ValidParams S d) :
    logLik (joint T) xs θ ≤ logLik (joint T) xs (emStep T xs hx θ)

Uses 12

Statement usesRich data for the ChromHMM M-step · Parameter space of ChromHMM · One ChromHMM step on rich data · ChromHMM joint weight of a state path and mark vectors · Log-likelihood of a latent-variable model

Proof usesThe ChromHMM update maximizes Q(· | θ) · Positivity of the ChromHMM joint weight · Valid HMM built from a valid ChromHMM parameter · The EM theorem · Valid hidden Markov model parameters · Valid HMMs · Hidden Markov model

TheoremThe log-likelihood is monotone along the ChromHMM iterates#✓fully proved

The log-likelihood is monotone along the ChromHMM iterates.

theorem logLik_iterate_emStep_monotone (hx : Rich T xs) (θ₀ : ValidParams S d) :
    Monotone fun k => logLik (joint T) xs ((emStep T xs hx)^[k] θ₀)

Uses 12

Statement usesRich data for the ChromHMM M-step · Parameter space of ChromHMM · One ChromHMM step on rich data · ChromHMM joint weight of a state path and mark vectors · Log-likelihood of a latent-variable model

Proof usesThe ChromHMM update maximizes Q(· | θ) · Positivity of the ChromHMM joint weight · Valid HMM built from a valid ChromHMM parameter · EM iterates have monotone likelihood · Valid hidden Markov model parameters · Valid HMMs · Hidden Markov model

TheoremEM log-likelihood as a sum of HMM log-likelihoods#✓fully proved

The EM log-likelihood is the sum of the HMM log-likelihoods of the sequences.

theorem logLik_eq (θ : ValidParams S d) :
    logLik (joint T) xs θ = ∑ n, log (likelihood θ.1.toHMM (xs n) T)

Uses 7

Statement usesChromHMM parameters · Valid ChromHMM parameters · HMM of ChromHMM parameters · Parameter space of ChromHMM · ChromHMM joint weight of a state path and mark vectors · Log-likelihood of a latent-variable model · Likelihood of the observations

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.