Profile scores for amino acid substitutions

16 fully proved

Profile log-odds scores

DefinitionProfile log-odds score of a residue#✓fully proved

The profile log-odds score log (p a / q a) of residue a: p is the position-specific profile probability (estimated from aligned homologs), q the background probability. Meaningful for p a, q a > 0; otherwise Lean's log 0 = 0 and x / 0 = 0 give junk.

noncomputable def profileScore (p q : A → ℝ) (a : A) : ℝ :=
  log (p a / q a)

Used by 5

Used byPSIC score difference of a substitution · PSIC difference as a log ratio of likelihood ratios · Gibbs' inequality for the profile score · Expected profile score under the background is nonpositive · The score is a log-likelihood ratio

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

For a sequence s over independent positions with profiles p j and background q (all positive), the summed profile score is the log of the likelihood ratio ∏ p_j(s_j) / ∏ q(s_j) of the profile model against the background.

theorem sum_profileScore_eq_log_likelihood_ratio {ι : Type*} [Fintype ι] (p : ι → A → ℝ)
    (q : A → ℝ) (s : ι → A) (hp : ∀ j a, 0 < p j a) (hq : ∀ a, 0 < q a) :
    ∑ j, profileScore (p j) q (s j) = log ((∏ j, p j (s j)) / ∏ j, q (s j))

Uses 1

Statement usesProfile log-odds score of a residue

TheoremGibbs' inequality for the profile score#✓fully proved

If p and q are probability vectors and q is positive, the expected score under the profile, ∑ p a log (p a / q a) (the Kullback–Leibler divergence), is nonnegative.

theorem sum_mul_profileScore_nonneg [Fintype A] {p q : A → ℝ} (hp : ∀ a, 0 ≤ p a)
    (hq : ∀ a, 0 < q a) (hp1 : ∑ a, p a = 1) (hq1 : ∑ a, q a = 1) :
    0 ≤ ∑ a, p a * profileScore p q a

Uses 1

Statement usesProfile log-odds score of a residue

TheoremExpected profile score under the background is nonpositive#✓fully proved

If p and q are probability vectors and p is positive, the expected score under the background, ∑ q a log (p a / q a), is nonpositive.

theorem sum_mul_profileScore_nonpos [Fintype A] {p q : A → ℝ} (hp : ∀ a, 0 < p a)
    (hq : ∀ a, 0 ≤ q a) (hp1 : ∑ a, p a = 1) (hq1 : ∑ a, q a = 1) :
    ∑ a, q a * profileScore p q a ≤ 0

Uses 1

Statement usesProfile log-odds score of a residue

DefinitionPSIC score difference of a substitution#✓fully proved

The PSIC score difference of a substitution from the wild-type residue wt to the mutant residue mt: profileScore p q wt - profileScore p q mt.

noncomputable def psicDifference (p q : A → ℝ) (wt mt : A) : ℝ :=
  profileScore p q wt - profileScore p q mt

Uses 1 · Used by 2

Statement usesProfile log-odds score of a residue

Used byPSIC difference as a log ratio of likelihood ratios · Positivity criterion for the PSIC difference

TheoremPSIC difference as a log ratio of likelihood ratios#✓fully proved

The PSIC difference is the log of the ratio of the two residues' likelihood ratios.

theorem psicDifference_eq_log {p q : A → ℝ} {wt mt : A} (hp : ∀ a, 0 < p a)
    (hq : ∀ a, 0 < q a) :
    psicDifference p q wt mt = log ((p wt / q wt) / (p mt / q mt))

Uses 2 · Used by 1

Statement usesPSIC score difference of a substitution

Proof usesProfile log-odds score of a residue

Used byPositivity criterion for the PSIC difference

TheoremPositivity criterion for the PSIC difference#✓fully proved

The PSIC difference is positive iff the wild type is more enriched in the profile, relative to background, than the mutant.

theorem psicDifference_pos_iff {p q : A → ℝ} {wt mt : A} (hp : ∀ a, 0 < p a)
    (hq : ∀ a, 0 < q a) :
    0 < psicDifference p q wt mt ↔ p mt / q mt < p wt / q wt

Uses 2

Statement usesPSIC score difference of a substitution

Proof usesPSIC difference as a log ratio of likelihood ratios

Naive-Bayes combination of features

StructureTwo-class naive Bayes model#✓fully proved

A two-class naive Bayes model: class damaging has prior prior ∈ (0, 1), class benign the complement; each feature j takes values in the finite type X j with class-conditional probabilities damaging j and benign j, assumed positive; features are conditionally independent given the class. The tables are estimated from training data.

structure NaiveBayes (ι : Type*) (X : ι → Type*) [∀ j, Fintype (X j)] where
  /-- The prior probability of the class *damaging*. -/
  prior : ℝ
  prior_pos : 0 < prior
  prior_lt_one : prior < 1
  /-- The likelihood of each value of feature `j` given *damaging*. -/
  damaging : ∀ j, X j → ℝ
  /-- The likelihood of each value of feature `j` given *benign*. -/
  benign : ∀ j, X j → ℝ
  damaging_pos : ∀ j v, 0 < damaging j v
  benign_pos : ∀ j v, 0 < benign j v
  sum_damaging : ∀ j, ∑ v, damaging j v = 1
  sum_benign : ∀ j, ∑ v, benign j v = 1

Used by 8

Used byJoint probability of class and features in naive Bayes · Log-likelihood ratio of a feature value · Naive Bayes posterior probability of damage · Naive-Bayes posterior · Naive Bayes posterior is strictly monotone in the score · Monotonicity in a feature value · Naive Bayes score · Naive Bayes joint law is a probability law

DefinitionJoint probability of class and features in naive Bayes#✓fully proved

The joint probability of class c (true = damaging) and feature values x: π ∏ P_D(x_j) or (1 - π) ∏ P_B(x_j).

noncomputable def joint (c : Bool) (x : ∀ j, X j) : ℝ :=
  if c then M.prior * ∏ j, M.damaging j (x j) else (1 - M.prior) * ∏ j, M.benign j (x j)

Uses 1 · Used by 3

Statement usesTwo-class naive Bayes model

Used byNaive Bayes posterior probability of damage · Naive-Bayes posterior · Naive Bayes joint law is a probability law

TheoremNaive Bayes joint law is a probability law#✓fully proved

The joint law of class and features is a probability law.

theorem sum_joint [DecidableEq ι] : ∑ c, ∑ x, M.joint c x = 1

Uses 2

Statement usesTwo-class naive Bayes model · Joint probability of class and features in naive Bayes

DefinitionNaive Bayes posterior probability of damage#✓fully proved

The posterior probability that the variant is damaging given feature values x (Bayes' rule on the joint law).

noncomputable def posterior (x : ∀ j, X j) : ℝ :=
  M.joint true x / ∑ c, M.joint c x

Uses 2 · Used by 3

Statement usesTwo-class naive Bayes model · Joint probability of class and features in naive Bayes

Used byNaive-Bayes posterior · Naive Bayes posterior is strictly monotone in the score · Monotonicity in a feature value

DefinitionLog-likelihood ratio of a feature value#✓fully proved

The log-likelihood ratio log (P_D(v) / P_B(v)) of value v of feature j.

noncomputable def logLikelihoodRatio (j : ι) (v : X j) : ℝ :=
  log (M.damaging j v / M.benign j v)

Uses 1 · Used by 2

Statement usesTwo-class naive Bayes model

Used byMonotonicity in a feature value · Naive Bayes score

DefinitionNaive Bayes score#✓fully proved

The naive-Bayes score: prior log-odds plus the features' log-likelihood ratios.

noncomputable def score (x : ∀ j, X j) : ℝ :=
  log (M.prior / (1 - M.prior)) + ∑ j, M.logLikelihoodRatio j (x j)

Uses 2 · Used by 3

Statement usesTwo-class naive Bayes model · Log-likelihood ratio of a feature value

Used byNaive-Bayes posterior · Naive Bayes posterior is strictly monotone in the score · Monotonicity in a feature value

TheoremNaive-Bayes posterior#✓fully proved

The posterior probability of damaging is the logistic function of the score.

theorem posterior_eq_sigmoid (x : ∀ j, X j) : M.posterior x = sigmoid (M.score x)

Uses 5 · Used by 2

Statement usesTwo-class naive Bayes model · Naive Bayes posterior probability of damage · Naive Bayes score

Proof usesJoint probability of class and features in naive Bayes · The logistic function of the log odds

Used byNaive Bayes posterior is strictly monotone in the score · Monotonicity in a feature value

TheoremNaive Bayes posterior is strictly monotone in the score#✓fully proved

The posterior is strictly monotone in the score.

theorem posterior_lt_posterior_iff (x y : ∀ j, X j) :
    M.posterior x < M.posterior y ↔ M.score x < M.score y

Uses 4

Statement usesTwo-class naive Bayes model · Naive Bayes posterior probability of damage · Naive Bayes score

Proof usesNaive-Bayes posterior

TheoremMonotonicity in a feature value#✓fully proved

Let feature j carry a numerical value g v (for example a PSIC-difference bin) such that its likelihood ratio P_D(v) / P_B(v) is monotone in g v. With the other features fixed, the posterior is monotone in g.

theorem posterior_update_le_of_monotone [DecidableEq ι] (x : ∀ j, X j) (j : ι) (g : X j → ℝ)
    (hg : ∀ v w, g v ≤ g w → M.damaging j v / M.benign j v ≤ M.damaging j w / M.benign j w)
    {v w : X j} (hvw : g v ≤ g w) :
    M.posterior (Function.update x j v) ≤ M.posterior (Function.update x j w)

Uses 5

Statement usesTwo-class naive Bayes model · Naive Bayes posterior probability of damage

Proof usesLog-likelihood ratio of a feature value · Naive-Bayes posterior · Naive Bayes score

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.