Position weight matrices

DefinitionScore of a site under a position weight matrix#✓fully proved

The score ∑ᵢ W i (s i) of a site s of width w under a position weight matrix W.

def score {R : Type*} [AddCommMonoid R] (W : Fin w → α → R) (s : Fin w → α) : R :=
  ∑ i, W i (s i)

Used by 13

Used byScaling and rounding error · The convolution response is the PWM score of the window · The reverse-complement filter scans the other strand · Max pooling returns the best PWM hit · Every window's PWM score is at most the max-pooled output · Exact p-values · The column recursion computes the exact score distribution · The log-odds score is a log-likelihood ratio · Log-odds score of a selected site is its scaled energy up to a constant · Law of energy-selected background sites · Berg–von Hippel · Thresholding the log-odds score is most powerful · The expected log-odds score is the total information content

DefinitionSite likelihood under a column-independent model#✓fully proved

The likelihood ∏ᵢ p i (s i) of a site under the product (column-independent) site model p.

def siteLik (p : Fin w → α → ℝ) (s : Fin w → α) : ℝ := ∏ i, p i (s i)

Used by 10

Used byThe M-step maximizes the EM objective · Joint likelihood with no motif occurrence · The joint is the window model · Positivity of the motif model · The log-odds score is a log-likelihood ratio · Berg–von Hippel · Thresholding the log-odds score is most powerful · Product site likelihoods form a distribution · The expected log-odds score is the total information content · Likelihood ratio of a motif window

DefinitionBackground likelihood of a sequence#✓fully proved

The likelihood ∏ₖ q (x k) of a sequence of length m under the background of independent letters with law q.

def bgLik {m : ℕ} (q : α → ℝ) (x : Fin m → α) : ℝ := ∏ k, q (x k)

Used by 14

Used byThe M-step maximizes the EM objective · Joint likelihood of a sequence and a motif occurrence · Joint likelihood with no motif occurrence · The joint is the window model · Positivity of the motif model · Exact p-values · The E-step in closed form · The column recursion computes the exact score distribution · The log-odds score is a log-likelihood ratio · Law of energy-selected background sites · Berg–von Hippel · Background likelihoods form a distribution · Thresholding the log-odds score is most powerful · Likelihood ratio of a motif window

DefinitionLog-odds matrix of a site model#✓fully proved

The log-odds matrix log (p i b / q b) of a site model against a background (natural logarithm).

noncomputable def logOdds (p : Fin w → α → ℝ) (q : α → ℝ) : Fin w → α → ℝ :=
  fun i b => log (p i b / q b)

Used by 5

Used byLog-odds are affine in the energies · The log-odds score is a log-likelihood ratio · Log-odds score of a selected site is its scaled energy up to a constant · Thresholding the log-odds score is most powerful · The expected log-odds score is the total information content

TheoremThe log-odds score is a log-likelihood ratio#✓fully proved

The log-odds score is a log-likelihood ratio (Staden 1989; Stormo 2000): for positive site model and background, score (logOdds p q) s = log (siteLik p s / bgLik q s).

theorem score_logOdds {p : Fin w → α → ℝ} {q : α → ℝ} (hp : ∀ i b, 0 < p i b)
    (hq : ∀ b, 0 < q b) (s : Fin w → α) :
    score (logOdds p q) s = log (siteLik p s / bgLik q s)

Uses 4 · Used by 1

Statement usesBackground likelihood of a sequence · Log-odds matrix of a site model · Score of a site under a position weight matrix · Site likelihood under a column-independent model

Used byThresholding the log-odds score is most powerful

TheoremProduct site likelihoods form a distribution#✓fully proved

A product of column distributions is a distribution on sites.

theorem sum_siteLik {p : Fin w → α → ℝ} (hp : ∀ i, IsDist (p i)) :
    ∑ s, siteLik p s = 1

Uses 2

Statement usesSite likelihood under a column-independent model · Probability distributions on a finite latent space

TheoremBackground likelihoods form a distribution#✓fully proved

The background law of independent letters is a distribution on sequences.

theorem sum_bgLik {m : ℕ} {q : α → ℝ} (hq : IsDist q) : ∑ x : Fin m → α, bgLik q x = 1

Uses 2

Statement usesBackground likelihood of a sequence · Probability distributions on a finite latent space

TheoremThresholding the log-odds score is most powerful#✓fully proved

Thresholding the log-odds score is most powerful (Neyman–Pearson): a test φ of the background (null) against the site model whose background size is at most that of the threshold test score > t has at most its power.

theorem sum_mul_siteLik_le_of_sum_mul_bgLik_le {p : Fin w → α → ℝ} {q : α → ℝ}
    (hp : ∀ i b, 0 < p i b) (hq : ∀ b, 0 < q b) (t : ℝ) (φ : (Fin w → α) → ℝ)
    (hφ0 : ∀ s, 0 ≤ φ s) (hφ1 : ∀ s, φ s ≤ 1)
    (hsize : ∑ s, φ s * bgLik q s ≤
      ∑ s, (if t < score (logOdds p q) s then 1 else 0) * bgLik q s) :
    ∑ s, φ s * siteLik p s ≤
      ∑ s, (if t < score (logOdds p q) s then 1 else 0) * siteLik p s

Uses 6

Statement usesBackground likelihood of a sequence · Log-odds matrix of a site model · Score of a site under a position weight matrix · Site likelihood under a column-independent model

Proof usesThe log-odds score is a log-likelihood ratio · Neyman–Pearson lemma

DefinitionInformation content of a position weight matrix column#✓fully proved

The information content ∑_b p b log₂ (p b / q b) (in bits) of a PWM column p against the background q (Schneider et al. 1986). Letters with p b = 0 contribute 0.

noncomputable def infoContent (p q : α → ℝ) : ℝ := (∑ b, p b * log (p b / q b)) / log 2

Used by 6

Used byInformation content is a Kullback–Leibler divergence · Information content is nonnegative · Information content against the uniform background · Information content is at most the log of the alphabet size · A DNA column carries at most two bits · The expected log-odds score is the total information content

TheoremInformation content is a Kullback–Leibler divergence#✓fully proved

For laws P ≪ Q, the information content of P against Q is KL(P ‖ Q) / log 2, Mathlib's klDiv in bits.

theorem infoContent_eq_klDiv [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : PMF α)
    (hPQ : ∀ a, Q a = 0 → P a = 0) :
    infoContent (fun b => (P b).toReal) (fun b => (Q b).toReal) =
      (InformationTheory.klDiv P.toMeasure Q.toMeasure).toReal / log 2

Uses 2

Statement usesInformation content of a position weight matrix column

Proof usesKullback–Leibler divergence of finite probability laws

TheoremInformation content is nonnegative#✓fully proved

Information content is nonnegative (Gibbs' inequality) for a column distribution and a positive background distribution.

theorem infoContent_nonneg {p q : α → ℝ} (hp : IsDist p) (hq : IsDist q)
    (hq0 : ∀ b, 0 < q b) : 0 ≤ infoContent p q

Uses 3

Statement usesInformation content of a position weight matrix column · Probability distributions on a finite latent space

Proof usesGibbs' inequality (evidence lower bound form)

TheoremInformation content against the uniform background#✓fully proved

Information content against the uniform background (Schneider et al. 1986): log₂ |α| - H(p), the maximal entropy minus the column entropy.

theorem infoContent_uniform [Nonempty α] (P : PMF α) :
    infoContent (fun b => (P b).toReal) (fun _ => ((Fintype.card α : ℝ))⁻¹) =
      logb 2 (Fintype.card α) - InformationTheory.shannonEntropy P

Uses 2 · Used by 1

Statement usesInformation content of a position weight matrix column · Shannon entropy

Used byInformation content is at most the log of the alphabet size

TheoremInformation content is at most the log of the alphabet size#✓fully proved

Against the uniform background, a column carries at most log₂ |α| bits.

theorem infoContent_uniform_le [Nonempty α] (P : PMF α) :
    infoContent (fun b => (P b).toReal) (fun _ => ((Fintype.card α : ℝ))⁻¹) ≤
      logb 2 (Fintype.card α)

Uses 3 · Used by 1

Statement usesInformation content of a position weight matrix column

Proof usesInformation content against the uniform background · Shannon entropy

Used byA DNA column carries at most two bits

TheoremA DNA column carries at most two bits#✓fully proved

For a four-letter alphabet (DNA) and the uniform background, a column carries between 0 and 2 bits.

theorem infoContent_uniform_le_two [Nonempty α] (h4 : Fintype.card α = 4) (P : PMF α) :
    infoContent (fun b => (P b).toReal) (fun _ => ((Fintype.card α : ℝ))⁻¹) ≤ 2

Uses 2

Statement usesInformation content of a position weight matrix column

Proof usesInformation content is at most the log of the alphabet size

TheoremThe expected log-odds score is the total information content#✓fully proved

Under the site model, E[score] = log 2 · ∑ᵢ IC(pᵢ ‖ q). This is an identity for every q (both sides use the same logarithms); it is an expected log-likelihood ratio for a positive background.

theorem sum_siteLik_mul_score_logOdds {p : Fin w → α → ℝ} {q : α → ℝ}
    (hp : ∀ i, IsDist (p i)) :
    ∑ s, siteLik p s * score (logOdds p q) s = log 2 * ∑ i, infoContent (p i) q

Uses 5

Statement usesInformation content of a position weight matrix column · Log-odds matrix of a site model · Score of a site under a position weight matrix · Site likelihood under a column-independent model · Probability distributions on a finite latent space

DefinitionOne column step of the score-distribution recursion#✓fully proved

One column of the score-distribution recursion: from the distribution d of the score of the first columns, the distribution after adding a column c with background q, ∑_b q b · (d shifted by c b).

noncomputable def scoreStep (q : α → ℝ) (d : ℤ →₀ ℝ) (c : α → ℤ) : ℤ →₀ ℝ :=
  ∑ b, q b • d.mapDomain (· + c b)

Used by 2

Used byBackground score distribution of an integer matrix · The column recursion computes the exact score distribution

DefinitionBackground score distribution of an integer matrix#✓fully proved

The background distribution of the score of an integer matrix M, computed column by column from the point mass at 0 (Staden 1989; Touzet and Varré 2007).

noncomputable def scoreDist (q : α → ℝ) (M : Fin w → α → ℤ) : ℤ →₀ ℝ :=
  (List.ofFn M).foldl (scoreStep q) (Finsupp.single 0 1)

Uses 1 · Used by 3

Statement usesOne column step of the score-distribution recursion

Used byExact p-value of a score threshold · Exact p-values · The column recursion computes the exact score distribution

TheoremThe column recursion computes the exact score distribution#✓fully proved

scoreDist q M t is ∑_{s : score M s = t} ∏ᵢ q (s i), for every q. When q is a distribution this is the background probability of the score t (the weights sum to 1 by sum_bgLik).

theorem scoreDist_apply (q : α → ℝ) (M : Fin w → α → ℤ) (t : ℤ) :
    scoreDist q M t = ∑ s with score M s = t, bgLik q s

Uses 4 · Used by 1

Statement usesBackground likelihood of a sequence · Score of a site under a position weight matrix · Background score distribution of an integer matrix

Proof usesOne column step of the score-distribution recursion

Used byExact p-values

DefinitionExact p-value of a score threshold#✓fully proved

The exact p-value of the score threshold t, summed over the computed distribution.

noncomputable def pValue (q : α → ℝ) (M : Fin w → α → ℤ) (t : ℤ) : ℝ :=
  ∑ u ∈ (scoreDist q M).support with t ≤ u, scoreDist q M u

Uses 1 · Used by 1

Statement usesBackground score distribution of an integer matrix

Used byExact p-values

TheoremExact p-values#✓fully proved

pValue q M t = ∑_{s : score M s ≥ t} ∏ᵢ q (s i), the background probability P_q(score M ≥ t) when q is a distribution.

theorem pValue_eq (q : α → ℝ) (M : Fin w → α → ℤ) (t : ℤ) :
    pValue q M t = ∑ s with t ≤ score M s, bgLik q s

Uses 5

Statement usesBackground likelihood of a sequence · Exact p-value of a score threshold · Score of a site under a position weight matrix

Proof usesBackground score distribution of an integer matrix · The column recursion computes the exact score distribution

TheoremScaling and rounding error#✓fully proved

Rounding c · W to integers changes the rescaled score of every site by at most w / (2c).

theorem abs_score_sub_score_round_le (W : Fin w → α → ℝ) {c : ℝ} (hc : 0 < c)
    (s : Fin w → α) :
    |score W s - ((score (fun i b => round (c * W i b)) s : ℤ) : ℝ) / c| ≤ w / (2 * c)

Uses 1

Statement usesScore of a site under a position weight matrix

DefinitionColumn partition function of an energy matrix#✓fully proved

The column partition function Z = ∑_b q b e^{-λ ε b} of energies ε at inverse temperature λ.

noncomputable def partitionFn (q ε : α → ℝ) (lam : ℝ) : ℝ := ∑ b, q b * exp (-lam * ε b)

Used by 6

Used byBoltzmann position weight matrix · Columns of the Boltzmann matrix are distributions · Log-odds are affine in the energies · Positivity of the column partition function · Log-odds score of a selected site is its scaled energy up to a constant · Berg–von Hippel

DefinitionBoltzmann position weight matrix#✓fully proved

The Boltzmann PWM q b e^{-λ ε i b} / Zᵢ of an energy matrix ε.

noncomputable def boltzmannPWM (q : α → ℝ) (ε : Fin w → α → ℝ) (lam : ℝ) : Fin w → α → ℝ :=
  fun i b => q b * exp (-lam * ε i b) / partitionFn q (ε i) lam

Uses 1 · Used by 4

Statement usesColumn partition function of an energy matrix

Used byColumns of the Boltzmann matrix are distributions · Log-odds are affine in the energies · Log-odds score of a selected site is its scaled energy up to a constant · Berg–von Hippel

DefinitionLaw of energy-selected background sites#✓fully proved

The law of background sites selected with weight e^{-λ E(s)} for the additive energy E s = score ε s = ∑ᵢ ε i (s i): q(s) e^{-λ E(s)} / ∑_{s'} q(s') e^{-λ E(s')}.

noncomputable def selectedLaw (q : α → ℝ) (ε : Fin w → α → ℝ) (lam : ℝ) (s : Fin w → α) : ℝ :=
  bgLik q s * exp (-lam * score ε s) / ∑ s', bgLik q s' * exp (-lam * score ε s')

Uses 2 · Used by 1

Statement usesBackground likelihood of a sequence · Score of a site under a position weight matrix

Used byBerg–von Hippel

TheoremPositivity of the column partition function#✓fully proved

The partition function of a positive background is positive.

theorem partitionFn_pos [Nonempty α] {q : α → ℝ} (hq : ∀ b, 0 < q b) (ε : α → ℝ) (lam : ℝ) :
    0 < partitionFn q ε lam

Uses 1 · Used by 2

Statement usesColumn partition function of an energy matrix

Used byColumns of the Boltzmann matrix are distributions · Log-odds are affine in the energies

TheoremColumns of the Boltzmann matrix are distributions#✓fully proved

Each column of the Boltzmann PWM is a distribution.

theorem isDist_boltzmannPWM [Nonempty α] {q : α → ℝ} (hq : ∀ b, 0 < q b)
    (ε : Fin w → α → ℝ) (lam : ℝ) (i : Fin w) : IsDist (boltzmannPWM q ε lam i)

Uses 4

Statement usesBoltzmann position weight matrix · Probability distributions on a finite latent space

Proof usesColumn partition function of an energy matrix · Positivity of the column partition function

TheoremBerg–von Hippel#✓fully proved

Boltzmann selection of background sites with an additive energy yields the product site model with columns boltzmannPWM. This is an identity for every q (both sides vanish when some Zᵢ = 0); it is a statement about laws for positive q.

theorem selectedLaw_eq_siteLik (q : α → ℝ) (ε : Fin w → α → ℝ) (lam : ℝ) (s : Fin w → α) :
    selectedLaw q ε lam s = siteLik (boltzmannPWM q ε lam) s

Uses 6

Statement usesBoltzmann position weight matrix · Law of energy-selected background sites · Site likelihood under a column-independent model

Proof usesBackground likelihood of a sequence · Column partition function of an energy matrix · Score of a site under a position weight matrix

TheoremLog-odds are affine in the energies#✓fully proved

log (p i b / q b) = -λ ε i b - log Zᵢ for the Boltzmann PWM.

theorem logOdds_boltzmannPWM [Nonempty α] {q : α → ℝ} (hq : ∀ b, 0 < q b)
    (ε : Fin w → α → ℝ) (lam : ℝ) (i : Fin w) (b : α) :
    logOdds (boltzmannPWM q ε lam) q i b = -lam * ε i b - log (partitionFn q (ε i) lam)

Uses 4 · Used by 1

Statement usesBoltzmann position weight matrix · Log-odds matrix of a site model · Column partition function of an energy matrix

Proof usesPositivity of the column partition function

Used byLog-odds score of a selected site is its scaled energy up to a constant

TheoremLog-odds score of a selected site is its scaled energy up to a constant#✓fully proved

The log-odds score of a selected site is -λ E(s) up to the constant ∑ᵢ log Zᵢ.

theorem score_logOdds_boltzmannPWM [Nonempty α] {q : α → ℝ} (hq : ∀ b, 0 < q b)
    (ε : Fin w → α → ℝ) (lam : ℝ) (s : Fin w → α) :
    score (logOdds (boltzmannPWM q ε lam) q) s =
      -lam * score ε s - ∑ i, log (partitionFn q (ε i) lam)

Uses 5

Statement usesBoltzmann position weight matrix · Log-odds matrix of a site model · Column partition function of an energy matrix · Score of a site under a position weight matrix

Proof usesLog-odds are affine in the energies

DefinitionSequence position of a motif column#✓fully proved

The position j + i of motif column i for a motif starting at j, in a sequence of length n + w (so n + 1 possible starts).

def sitePos (j : Fin (n + 1)) (i : Fin w) : Fin (n + w) := ⟨j + i, by omega⟩

Used by 6

Used byCoverage condition for motif columns · The M-step maximizes the EM objective · Expected letter counts in motif columns · Positivity of expected motif counts · The joint is the window model · Window of a sequence at a given start

DefinitionWindow of a sequence at a given start#✓fully proved

The window of width w of x starting at j.

def window (x : Fin (n + w) → α) (j : Fin (n + 1)) : Fin w → α := fun i => x (sitePos j i)

Uses 1 · Used by 5

Statement usesSequence position of a motif column

Used byThe M-step maximizes the EM objective · Joint likelihood with no motif occurrence · The joint is the window model · Positivity of the motif model · Likelihood ratio of a motif window

DefinitionLikelihood ratio of a motif window#✓fully proved

The likelihood ratio of the window at j under the site model θ against the background q, and 1 when there is no motif occurrence.

noncomputable def windowRatio (q : α → ℝ) (θ : Fin w → α → ℝ) (x : Fin (n + w) → α) :
    Option (Fin (n + 1)) → ℝ
  | none => 1
  | some j => siteLik θ (window x j) / bgLik q (window x j)

Uses 3 · Used by 6

Statement usesBackground likelihood of a sequence · Site likelihood under a column-independent model · Window of a sequence at a given start

Used byThe M-step maximizes the EM objective · Joint likelihood of a sequence and a motif occurrence · Joint likelihood with no motif occurrence · The joint is the window model · Positivity of the motif model · The E-step in closed form

DefinitionJoint likelihood of a sequence and a motif occurrence#✓fully proved

The joint likelihood of a sequence x and a latent occurrence z with prior prior z and start start z (none: no occurrence): background letters outside the window, site-model letters inside. One occurrence per sequence (OOPS) is Z = Fin (n + 1), start = some, prior uniform; zero or one (ZOOPS) is Z = Option (Fin (n + 1)), start = id, prior none = 1 - γ and prior (some j) = γ / (n + 1) for a fixed γ. The background q is a fixed parameter.

noncomputable def motifJoint (q : α → ℝ) (prior : Z → ℝ) (start : Z → Option (Fin (n + 1)))
    (θ : Fin w → α → ℝ) (x : Fin (n + w) → α) (z : Z) : ℝ :=
  prior z * bgLik q x * windowRatio q θ x (start z)

Uses 2 · Used by 3

Statement usesBackground likelihood of a sequence · Likelihood ratio of a motif window

Used byJoint likelihood with no motif occurrence · The joint is the window model · Motif model as an EM model

TheoremThe joint is the window model#✓fully proved

For a positive background and an occurrence at j, the joint is the prior times the product of θ (k - j) inside the window and q outside.

theorem motifJoint_of_start_eq_some {q : α → ℝ} (hq : ∀ b, 0 < q b) (prior : Z → ℝ)
    (start : Z → Option (Fin (n + 1))) (θ : Fin w → α → ℝ) (x : Fin (n + w) → α) {z : Z}
    {j : Fin (n + 1)} (hz : start z = some j) :
    motifJoint q prior start θ x z = prior z * ∏ k : Fin (n + w),
      if h : (j : ℕ) ≤ k ∧ (k : ℕ) < j + w then θ ⟨k - j, by omega⟩ (x k) else q (x k)

Uses 6

Statement usesJoint likelihood of a sequence and a motif occurrence

Proof usesBackground likelihood of a sequence · Site likelihood under a column-independent model · Sequence position of a motif column · Window of a sequence at a given start · Likelihood ratio of a motif window

TheoremJoint likelihood with no motif occurrence#✓fully proved

With no occurrence, the joint is the prior times the background likelihood.

theorem motifJoint_of_start_eq_none (q : α → ℝ) (prior : Z → ℝ)
    (start : Z → Option (Fin (n + 1))) (θ : Fin w → α → ℝ) (x : Fin (n + w) → α) {z : Z}
    (hz : start z = none) : motifJoint q prior start θ x z = prior z * bgLik q x

Uses 5

Statement usesBackground likelihood of a sequence · Joint likelihood of a sequence and a motif occurrence

Proof usesSite likelihood under a column-independent model · Window of a sequence at a given start · Likelihood ratio of a motif window

AbbreviationPositive position weight matrices#✓fully proved

PWMs with positive entries and columns summing to 1: the EM parameter space.

abbrev PosPWM (w : ℕ) (α : Type*) [Fintype α] : Type _ :=
  {θ : Fin w → α → ℝ // (∀ i b, 0 < θ i b) ∧ ∀ i, ∑ b, θ i b = 1}

Used by 8

Used byThe M-step maximizes the EM objective · Expected letter counts in motif columns · Positivity of expected motif counts · The motif likelihood is nondecreasing along the EM iterates · M-step for position weight matrices · Motif model as an EM model · Positivity of the motif model · The E-step in closed form

DefinitionMotif model as an EM model#✓fully proved

The motif model as an EM model on PosPWM.

noncomputable def motifModel (q : α → ℝ) (prior : Z → ℝ) (start : Z → Option (Fin (n + 1))) :
    PosPWM w α → (Fin (n + w) → α) → Z → ℝ :=
  fun θ => motifJoint q prior start θ.1

Uses 2 · Used by 6

Statement usesPositive position weight matrices · Joint likelihood of a sequence and a motif occurrence

Used byThe M-step maximizes the EM objective · Expected letter counts in motif columns · Positivity of expected motif counts · The motif likelihood is nondecreasing along the EM iterates · Positivity of the motif model · The E-step in closed form

TheoremPositivity of the motif model#✓fully proved

The motif model is positive for a positive background and a positive prior.

theorem motifModel_pos {q : α → ℝ} (hq : ∀ b, 0 < q b) {prior : Z → ℝ} (hprior : ∀ z, 0 < prior z)
    (start : Z → Option (Fin (n + 1))) (θ : PosPWM w α) (x : Fin (n + w) → α) (z : Z) :
    0 < motifModel q prior start θ x z

Uses 6 · Used by 2

Statement usesPositive position weight matrices · Motif model as an EM model

Proof usesBackground likelihood of a sequence · Site likelihood under a column-independent model · Window of a sequence at a given start · Likelihood ratio of a motif window

Used byPositivity of expected motif counts · The motif likelihood is nondecreasing along the EM iterates

TheoremThe E-step in closed form#✓fully proved

The posterior of the occurrence z is proportional to its prior times the likelihood ratio of its window (Lawrence and Reilly 1990; Bailey and Elkan 1995).

theorem posterior_motifModel {q : α → ℝ} (hq : ∀ b, 0 < q b) (prior : Z → ℝ)
    (start : Z → Option (Fin (n + 1))) (θ : PosPWM w α) (x : Fin (n + w) → α) (z : Z) :
    posterior (motifModel q prior start) θ x z =
      prior z * windowRatio q θ.1 x (start z) /
        ∑ z', prior z' * windowRatio q θ.1 x (start z')

Uses 6

Statement usesPositive position weight matrices · Motif model as an EM model · Likelihood ratio of a motif window · Posterior of a latent-variable model

Proof usesBackground likelihood of a sequence · Marginal of a latent-variable model

DefinitionExpected letter counts in motif columns#✓fully proved

The expected count of letter b in motif column i under the posteriors at θ: ∑ₘ ∑_z P(z | xₘ, θ) [start z = some j ∧ xₘ (j + i) = b].

noncomputable def expectedCounts (q : α → ℝ) (prior : Z → ℝ) (start : Z → Option (Fin (n + 1)))
    (xs : Fin N → Fin (n + w) → α) (θ : PosPWM w α) (i : Fin w) (b : α) : ℝ :=
  ∑ m, ∑ z, posterior (motifModel q prior start) θ (xs m) z *
    (match start z with
      | none => 0
      | some j => if xs m (sitePos j i) = b then 1 else 0)

Uses 4 · Used by 3

Statement usesPositive position weight matrices · Motif model as an EM model · Sequence position of a motif column · Posterior of a latent-variable model

Used byThe M-step maximizes the EM objective · Positivity of expected motif counts · M-step for position weight matrices

DefinitionCoverage condition for motif columns#✓fully proved

Every letter can occur in every motif column: for each column i and letter b some sequence has b at offset i of some possible occurrence. This keeps the M-step positive.

def Covers (start : Z → Option (Fin (n + 1))) (xs : Fin N → Fin (n + w) → α) : Prop :=
  ∀ (i : Fin w) (b : α), ∃ m z j, start z = some j ∧ xs m (sitePos j i) = b

Uses 1 · Used by 4

Statement usesSequence position of a motif column

Used byThe M-step maximizes the EM objective · Positivity of expected motif counts · The motif likelihood is nondecreasing along the EM iterates · M-step for position weight matrices

TheoremPositivity of expected motif counts#✓fully proved

Under Covers, every expected count is positive.

theorem expectedCounts_pos [Nonempty Z] {q : α → ℝ} (hq : ∀ b, 0 < q b) {prior : Z → ℝ}
    (hprior : ∀ z, 0 < prior z) {start : Z → Option (Fin (n + 1))}
    {xs : Fin N → Fin (n + w) → α} (hcov : Covers start xs) (θ : PosPWM w α) (i : Fin w)
    (b : α) : 0 < expectedCounts q prior start xs θ i b

Uses 8 · Used by 2

Statement usesCoverage condition for motif columns · Positive position weight matrices · Expected letter counts in motif columns

Proof usesMotif model as an EM model · Positivity of the motif model · Sequence position of a motif column · Marginal of a latent-variable model · Posterior of a latent-variable model

Used byThe M-step maximizes the EM objective · M-step for position weight matrices

DefinitionM-step for position weight matrices#✓fully proved

The M-step: normalized expected letter counts, θ' i b = c i b / ∑_{b'} c i b'.

noncomputable def mStep [Nonempty α] [Nonempty Z] {q : α → ℝ} (hq : ∀ b, 0 < q b) {prior : Z → ℝ}
    (hprior : ∀ z, 0 < prior z) {start : Z → Option (Fin (n + 1))}
    {xs : Fin N → Fin (n + w) → α} (hcov : Covers start xs) (θ : PosPWM w α) : PosPWM w α :=
  ⟨fun i b => expectedCounts q prior start xs θ i b /
      ∑ b', expectedCounts q prior start xs θ i b',
    fun i b => div_pos (expectedCounts_pos hq hprior hcov θ i b)
      (Finset.sum_pos (fun b' _ => expectedCounts_pos hq hprior hcov θ i b')
        ⟨b, Finset.mem_univ b⟩),
    fun i => by
      rw [← Finset.sum_div, div_self (Finset.sum_pos
        (fun b' _ => expectedCounts_pos hq hprior hcov θ i b') ⟨Classical.arbitrary α,
          Finset.mem_univ _⟩).ne']⟩

Uses 4 · Used by 2

Statement usesCoverage condition for motif columns · Positive position weight matrices · Expected letter counts in motif columns · Positivity of expected motif counts

Used byThe M-step maximizes the EM objective · The motif likelihood is nondecreasing along the EM iterates

TheoremThe M-step maximizes the EM objective#✓fully proved

The M-step maximizes the EM objective over PWMs with positive entries and normalized columns: for every θ', Q(θ' | θ) ≤ Q(mStep θ | θ) (Gibbs' inequality per column).

theorem emQ_le_emQ_mStep [Nonempty α] [Nonempty Z] {q : α → ℝ} (hq : ∀ b, 0 < q b) {prior : Z → ℝ}
    (hprior : ∀ z, 0 < prior z) {start : Z → Option (Fin (n + 1))} {xs : Fin N → Fin (n + w) → α}
    (hcov : Covers start xs) (θ θ' : PosPWM w α) :
    emQ (motifModel q prior start) xs θ' θ ≤
      emQ (motifModel q prior start) xs (mStep hq hprior hcov θ) θ

Uses 14 · Used by 1

Statement usesCoverage condition for motif columns · Positive position weight matrices · M-step for position weight matrices · Motif model as an EM model · The EM objective

Proof usesBackground likelihood of a sequence · Expected letter counts in motif columns · Positivity of expected motif counts · Site likelihood under a column-independent model · Sequence position of a motif column · Window of a sequence at a given start · Likelihood ratio of a motif window · The weighted log-likelihood is bounded by its value at the normalized counts · Posterior of a latent-variable model

Used byThe motif likelihood is nondecreasing along the EM iterates

TheoremThe motif likelihood is nondecreasing along the EM iterates#✓fully proved

The motif likelihood is nondecreasing along the EM iterates.

theorem logLik_iterate_mStep_monotone [Nonempty α] [Nonempty Z] {q : α → ℝ} (hq : ∀ b, 0 < q b)
    {prior : Z → ℝ} (hprior : ∀ z, 0 < prior z) {start : Z → Option (Fin (n + 1))}
    {xs : Fin N → Fin (n + w) → α} (hcov : Covers start xs) (θ₀ : PosPWM w α) :
    Monotone fun k => logLik (motifModel q prior start) xs ((mStep hq hprior hcov)^[k] θ₀)

Uses 8

Statement usesCoverage condition for motif columns · Positive position weight matrices · M-step for position weight matrices · Motif model as an EM model · Log-likelihood of a latent-variable model

Proof usesThe M-step maximizes the EM objective · Positivity of the motif model · EM iterates have monotone likelihood

DefinitionMoment generating function of a pair score#✓fully proved

The moment generating function ∑ₐ ∑_b pₐ p_b e^{λ s_{ab}} of a pair score under independent letters with law p.

noncomputable def pairMGF (p : α → ℝ) (s : α → α → ℝ) (lam : ℝ) : ℝ :=
  ∑ a, ∑ b, p a * p b * exp (lam * s a b)

Used by 4

Used byKarlin–Altschul λ · Target frequencies form a distribution on pairs · The relative entropy of the target frequencies · The target score is positive

TheoremKarlin–Altschul λ#✓fully proved

Karlin–Altschul λ (Karlin and Altschul 1990): if the expected score under a positive background distribution is negative and some score is positive, there is a unique λ > 0 with ∑ pₐ p_b e^{λ s_{ab}} = 1.

theorem existsUnique_pairMGF_eq_one {p : α → ℝ} {s : α → α → ℝ} (hp : IsDist p)
    (hp0 : ∀ a, 0 < p a) (hneg : ∑ a, ∑ b, p a * p b * s a b < 0) (hpos : ∃ a b, 0 < s a b) :
    ∃! lam, 0 < lam ∧ pairMGF p s lam = 1

Uses 2

Statement usesMoment generating function of a pair score · Probability distributions on a finite latent space

DefinitionImplicit target frequencies of a score matrix#✓fully proved

The implicit target frequencies q_{ab} = pₐ p_b e^{λ s_{ab}} of a score matrix.

noncomputable def targetFreq (p : α → ℝ) (s : α → α → ℝ) (lam : ℝ) (ab : α × α) : ℝ :=
  p ab.1 * p ab.2 * exp (lam * s ab.1 ab.2)

Used by 4

Used byTarget frequencies form a distribution on pairs · The relative entropy of the target frequencies · Every such score matrix is a log-odds matrix · The target score is positive

TheoremTarget frequencies form a distribution on pairs#✓fully proved

At a root of pairMGF p s λ = 1 the target frequencies form a distribution on pairs.

theorem isDist_targetFreq {p : α → ℝ} {s : α → α → ℝ} (hp0 : ∀ a, 0 < p a) {lam : ℝ}
    (hlam : pairMGF p s lam = 1) : IsDist (targetFreq p s lam)

Uses 3 · Used by 1

Statement usesMoment generating function of a pair score · Implicit target frequencies of a score matrix · Probability distributions on a finite latent space

Used byThe relative entropy of the target frequencies

TheoremEvery such score matrix is a log-odds matrix#✓fully proved

Every such score matrix is a log-odds matrix (Karlin and Altschul 1990): s_{ab} = log (q_{ab} / (pₐ p_b)) / λ for every λ > 0; at the Karlin–Altschul root the q_{ab} form a distribution (isDist_targetFreq), the implicit target frequencies.

theorem score_eq_log_targetFreq {p : α → ℝ} (hp0 : ∀ a, 0 < p a) (s : α → α → ℝ) {lam : ℝ}
    (hlam : 0 < lam) (a b : α) : s a b = log (targetFreq p s lam (a, b) / (p a * p b)) / lam

Uses 1

Statement usesImplicit target frequencies of a score matrix

TheoremThe relative entropy of the target frequencies#✓fully proved

The relative entropy of the target frequencies (Altschul 1991): λ ∑ q_{ab} s_{ab} = ∑ q_{ab} log (q_{ab} / (pₐ p_b)), which is nonnegative.

theorem relEntropy_eq_and_nonneg {p : α → ℝ} {s : α → α → ℝ} (hp : IsDist p)
    (hp0 : ∀ a, 0 < p a) {lam : ℝ} (hlam : pairMGF p s lam = 1) :
    lam * ∑ ab, targetFreq p s lam ab * s ab.1 ab.2 =
        ∑ ab, targetFreq p s lam ab * log (targetFreq p s lam ab / (p ab.1 * p ab.2)) ∧
      0 ≤ lam * ∑ ab, targetFreq p s lam ab * s ab.1 ab.2

Uses 5

Statement usesMoment generating function of a pair score · Implicit target frequencies of a score matrix · Probability distributions on a finite latent space

Proof usesTarget frequencies form a distribution on pairs · Gibbs' inequality (evidence lower bound form)

TheoremThe target score is positive#✓fully proved

At the Karlin–Altschul root λ > 0, the expected score ∑ q_{ab} s_{ab} under the target frequencies is positive.

theorem sum_targetFreq_mul_pos {p : α → ℝ} {s : α → α → ℝ} (hp : IsDist p)
    (hp0 : ∀ a, 0 < p a) (hpos : ∃ a b, 0 < s a b) {lam : ℝ} (hlam0 : 0 < lam)
    (hlam : pairMGF p s lam = 1) : 0 < ∑ ab, targetFreq p s lam ab * s ab.1 ab.2

Uses 3

Statement usesMoment generating function of a pair score · Implicit target frequencies of a score matrix · Probability distributions on a finite latent space

DefinitionOne-hot encoding of a letter#✓fully proved

The one-hot encoding of a letter: oneHot a b = 1 if b = a and 0 otherwise.

def oneHot (a : σ) (b : σ) : ℝ := if a = b then 1 else 0

Used by 4

Used byConvolution filter response at a window · The convolution response is the PWM score of the window · Translation equivariance · Filter responses read only positions within the sequence length

DefinitionConvolution filter response at a window#✓fully proved

The response of a convolution (cross-correlation) filter W of width w on the one-hot encoded sequence x at the window starting at i: ∑ k, ∑ b, W k b * oneHot (x (i + k)) b.

def conv (W : Fin w → σ → ℝ) (x : ℕ → σ) (i : ℕ) : ℝ :=
  ∑ k : Fin w, ∑ b, W k b * oneHot (x (i + k)) b

Uses 1 · Used by 9

Statement usesOne-hot encoding of a letter

Used byThe convolution response is the PWM score of the window · The reverse-complement filter scans the other strand · Translation equivariance · Max pooling returns the best PWM hit · Every window's PWM score is at most the max-pooled output · Global max pooling · Filter responses read only positions within the sequence length · Max pooling the reverse-complement filter equals max pooling W on the reverse complement · Bias and ReLU commute with max pooling

DefinitionWindow of a sequence starting at a position#✓fully proved

The window of length w of x starting at i.

def window (x : ℕ → σ) (i : ℕ) : Fin w → σ := fun k => x (i + k)

Used by 4

Used byThe convolution response is the PWM score of the window · The reverse-complement filter scans the other strand · Max pooling returns the best PWM hit · Every window's PWM score is at most the max-pooled output

TheoremThe convolution response is the PWM score of the window#✓fully proved

The convolution response is the PWM score of the window.

theorem conv_eq_pwmScore (W : Fin w → σ → ℝ) (x : ℕ → σ) (i : ℕ) :
    conv W x i = Cslib.Bioinformatics.Motifs.PWM.score W (window x i)

Uses 4 · Used by 3

Statement usesScore of a site under a position weight matrix · Convolution filter response at a window · Window of a sequence starting at a position

Proof usesOne-hot encoding of a letter

Used byThe reverse-complement filter scans the other strand · Max pooling returns the best PWM hit · Every window's PWM score is at most the max-pooled output

DefinitionGlobal max pooling#✓fully proved

Global max pooling over the m + 1 windows of a sequence of length m + w.

def maxPool (W : Fin w → σ → ℝ) (x : ℕ → σ) (m : ℕ) : ℝ :=
  (range (m + 1)).sup' nonempty_range_add_one (conv W x)

Uses 1 · Used by 7

Statement usesConvolution filter response at a window

Used byBoth-strand convolution score · The both-strand score is invariant under reverse complementing the sequence · Max pooling returns the best PWM hit · Every window's PWM score is at most the max-pooled output · Filter responses read only positions within the sequence length · Max pooling the reverse-complement filter equals max pooling W on the reverse complement · Bias and ReLU commute with max pooling

TheoremEvery window's PWM score is at most the max-pooled output#✓fully proved

Every window's PWM score is at most the max-pooled output.

theorem le_maxPool (W : Fin w → σ → ℝ) (x : ℕ → σ) {m i : ℕ} (hi : i ≤ m) :
    Cslib.Bioinformatics.Motifs.PWM.score W (window x i) ≤ maxPool W x m

Uses 5

Statement usesScore of a site under a position weight matrix · Global max pooling · Window of a sequence starting at a position

Proof usesConvolution filter response at a window · The convolution response is the PWM score of the window

TheoremMax pooling returns the best PWM hit#✓fully proved

Some window attains the max-pooled output.

theorem exists_eq_maxPool (W : Fin w → σ → ℝ) (x : ℕ → σ) (m : ℕ) :
    ∃ i ≤ m, Cslib.Bioinformatics.Motifs.PWM.score W (window x i) = maxPool W x m

Uses 5

Statement usesScore of a site under a position weight matrix · Global max pooling · Window of a sequence starting at a position

Proof usesConvolution filter response at a window · The convolution response is the PWM score of the window

TheoremBias and ReLU commute with max pooling#✓fully proved

Pooling max (conv + β) 0 over the windows gives max (maxPool + β) 0.

theorem maxPool_relu (W : Fin w → σ → ℝ) (x : ℕ → σ) (m : ℕ) (β : ℝ) :
    (range (m + 1)).sup' nonempty_range_add_one (fun i => max (conv W x i + β) 0) =
      max (maxPool W x m + β) 0

Uses 2

Statement usesConvolution filter response at a window · Global max pooling

TheoremTranslation equivariance#✓fully proved

Dropping the first letter shifts the responses by one window.

theorem conv_shift (W : Fin w → σ → ℝ) (x : ℕ → σ) (i : ℕ) :
    conv W (fun j => x (j + 1)) i = conv W x (i + 1)

Uses 2

Statement usesConvolution filter response at a window

Proof usesOne-hot encoding of a letter

DefinitionReverse complement of a sequence prefix#✓fully proved

The reverse complement of the length-L prefix of x: position j < L holds the complement of x (L - 1 - j).

def rcSeq (L : ℕ) (x : ℕ → σ) (j : ℕ) : σ := comp (x (L - 1 - j))

Used by 3

Used byThe both-strand score is invariant under reverse complementing the sequence · The reverse-complement filter scans the other strand · Max pooling the reverse-complement filter equals max pooling W on the reverse complement

DefinitionReverse-complement filter#✓fully proved

The reverse-complement filter: rcFilter W k b = W (Fin.rev k) (comp b).

def rcFilter (W : Fin w → σ → ℝ) (k : Fin w) (b : σ) : ℝ := W k.rev (comp b)

Used by 4

Used byBoth-strand convolution score · The both-strand score is invariant under reverse complementing the sequence · The reverse-complement filter scans the other strand · Max pooling the reverse-complement filter equals max pooling W on the reverse complement

TheoremThe reverse-complement filter scans the other strand#✓fully proved

On a sequence of length m + w, its response at window i ≤ m is the response of W on the reverse complement at window m - i.

theorem conv_rcFilter (W : Fin w → σ → ℝ) (x : ℕ → σ) {m i : ℕ} (hi : i ≤ m) :
    conv (rcFilter comp W) x i = conv W (rcSeq comp (m + w) x) (m - i)

Uses 6 · Used by 1

Statement usesConvolution filter response at a window · Reverse-complement filter · Reverse complement of a sequence prefix

Proof usesScore of a site under a position weight matrix · The convolution response is the PWM score of the window · Window of a sequence starting at a position

Used byMax pooling the reverse-complement filter equals max pooling W on the reverse complement

TheoremMax pooling the reverse-complement filter equals max pooling W on the reverse complement#✓fully proved

Max pooling the reverse-complement filter equals max pooling W on the reverse complement.

theorem maxPool_rcFilter (W : Fin w → σ → ℝ) (x : ℕ → σ) (m : ℕ) :
    maxPool (rcFilter comp W) x m = maxPool W (rcSeq comp (m + w) x) m

Uses 5 · Used by 1

Statement usesGlobal max pooling · Reverse-complement filter · Reverse complement of a sequence prefix

Proof usesConvolution filter response at a window · The reverse-complement filter scans the other strand

Used byThe both-strand score is invariant under reverse complementing the sequence

TheoremFilter responses read only positions within the sequence length#✓fully proved

The responses only read the positions < m + w of a sequence of length m + w.

theorem maxPool_congr (W : Fin w → σ → ℝ) {x y : ℕ → σ} {m : ℕ}
    (hxy : ∀ j < m + w, x j = y j) : maxPool W x m = maxPool W y m

Uses 3 · Used by 1

Statement usesGlobal max pooling

Proof usesConvolution filter response at a window · One-hot encoding of a letter

Used byThe both-strand score is invariant under reverse complementing the sequence

DefinitionBoth-strand convolution score#✓fully proved

The both-strand score: the larger of the max-pooled responses of W and of its reverse complement.

def bothStrands (W : Fin w → σ → ℝ) (x : ℕ → σ) (m : ℕ) : ℝ :=
  max (maxPool W x m) (maxPool (rcFilter comp W) x m)

Uses 2 · Used by 1

Statement usesGlobal max pooling · Reverse-complement filter

Used byThe both-strand score is invariant under reverse complementing the sequence

TheoremThe both-strand score is invariant under reverse complementing the sequence#✓fully proved

The both-strand score is invariant under reverse complementing the sequence, for an involutive complement.

theorem bothStrands_rcSeq (hcomp : Function.Involutive comp) (W : Fin w → σ → ℝ)
    (x : ℕ → σ) (m : ℕ) :
    bothStrands comp W (rcSeq comp (m + w) x) m = bothStrands comp W x m

Uses 6

Statement usesBoth-strand convolution score · Reverse complement of a sequence prefix

Proof usesGlobal max pooling · Filter responses read only positions within the sequence length · Max pooling the reverse-complement filter equals max pooling W on the reverse complement · Reverse-complement filter

68 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.