Skip to content

McDonald–Kreitman test

12 fully proved

The McDonald–Kreitman test

DefinitionSmith–Eyre-Walker estimator of adaptive substitutions#✓fully proved

The Smith–Eyre-Walker estimator of the proportion of adaptive nonsynonymous substitutions, α̂ = 1 - (D_s P_n) / (D_n P_s).

def alphaHat (Dn Ds Pn Ps : ℝ) : ℝ := 1 - Ds * Pn / (Dn * Ps)
Used by 3
Used byAdaptive proportion estimator equals one minus the neutrality index · α̂ at the expected counts is the proportion of adaptive substitutions · Consistency of α̂ over loci

DefinitionNeutrality index#✓fully proved

The neutrality index NI = (P_n / P_s) / (D_n / D_s).

def neutralityIndex (Dn Ds Pn Ps : ℝ) : ℝ := Pn / Ps / (Dn / Ds)
Used by 1
Used byAdaptive proportion estimator equals one minus the neutrality index

TheoremAdaptive proportion estimator equals one minus the neutrality index#✓fully proved

α̂ = 1 - NI, for all real counts (the junk values of division agree).

theorem alphaHat_eq_one_sub_neutralityIndex (Dn Ds Pn Ps : ℝ) :
    alphaHat Dn Ds Pn Ps = 1 - neutralityIndex Dn Ds Pn Ps
Uses 2
Statement usesSmith–Eyre-Walker estimator of adaptive substitutions · Neutrality index

StructureExpected-count model of the McDonald–Kreitman table#✓fully proved

Expected counts of the MK table without a slightly deleterious class (see the module docstring): synonymous and nonsynonymous mutational targets Ls, Ln, neutral fraction f₀ of nonsynonymous mutations, polymorphisms and neutral fixed differences per unit of neutral target polyRate, divRate (θ_P, λ_D in the module docstring), and A expected adaptive substitutions.

MathlibExt.Biology.PopulationGenetics.McDonaldKreitman.MKModel · 20 lines 
structure MKModel where
  /-- Synonymous mutational target. -/
  Ls : ℝ
  /-- Nonsynonymous mutational target. -/
  Ln : ℝ
  /-- Fraction of nonsynonymous mutations that are neutral. -/
  f₀ : ℝ
  /-- Expected polymorphisms per unit of neutral target. -/
  polyRate : ℝ
  /-- Expected neutral fixed differences per unit of neutral target. -/
  divRate : ℝ
  /-- Expected number of adaptive nonsynonymous substitutions. -/
  A : ℝ
  Ls_pos : 0 < Ls
  Ln_pos : 0 < Ln
  f₀_pos : 0 < f₀
  f₀_le_one : f₀ ≤ 1
  polyRate_pos : 0 < polyRate
  divRate_pos : 0 < divRate
  A_nonneg : 0 ≤ A
Used by 8
Used byProportion of adaptive nonsynonymous substitutions · α̂ at the expected counts is the proportion of adaptive substitutions · Expected nonsynonymous fixed differences · Expected synonymous fixed differences · Expected nonsynonymous polymorphisms · Expected synonymous polymorphisms · The MK null is neutrality · Consistency of α̂ over loci

Expected counts and the adaptive proportion

DefinitionExpected synonymous polymorphisms#✓fully proved

Expected synonymous polymorphisms E P_s = θ_P L_s.

def EPs : ℝ := M.polyRate * M.Ls
Uses 1 · Used by 3
Statement usesExpected-count model of the McDonald–Kreitman table
Used byα̂ at the expected counts is the proportion of adaptive substitutions · The MK null is neutrality · Consistency of α̂ over loci

DefinitionExpected nonsynonymous polymorphisms#✓fully proved

Expected nonsynonymous polymorphisms E P_n = θ_P f₀ L_n.

def EPn : ℝ := M.polyRate * M.f₀ * M.Ln
Uses 1 · Used by 3
Statement usesExpected-count model of the McDonald–Kreitman table
Used byα̂ at the expected counts is the proportion of adaptive substitutions · The MK null is neutrality · Consistency of α̂ over loci

DefinitionExpected synonymous fixed differences#✓fully proved

Expected synonymous fixed differences E D_s = λ_D L_s.

def EDs : ℝ := M.divRate * M.Ls
Uses 1 · Used by 3
Statement usesExpected-count model of the McDonald–Kreitman table
Used byα̂ at the expected counts is the proportion of adaptive substitutions · The MK null is neutrality · Consistency of α̂ over loci

DefinitionExpected nonsynonymous fixed differences#✓fully proved

Expected nonsynonymous fixed differences E D_n = λ_D f₀ L_n + A.

def EDn : ℝ := M.divRate * M.f₀ * M.Ln + M.A
Uses 1 · Used by 4
Statement usesExpected-count model of the McDonald–Kreitman table
Used byProportion of adaptive nonsynonymous substitutions · α̂ at the expected counts is the proportion of adaptive substitutions · The MK null is neutrality · Consistency of α̂ over loci

DefinitionProportion of adaptive nonsynonymous substitutions#✓fully proved

The proportion of nonsynonymous substitutions that are adaptive, α = A / E D_n.

def alpha : ℝ := M.A / M.EDn
Uses 2 · Used by 2
Statement usesExpected-count model of the McDonald–Kreitman table · Expected nonsynonymous fixed differences
Used byα̂ at the expected counts is the proportion of adaptive substitutions · Consistency of α̂ over loci

Theoremα̂ at the expected counts is the proportion of adaptive substitutions#✓fully proved

(Smith & Eyre-Walker 2002): 1 - (E D_s E P_n) / (E D_n E P_s) = A / E D_n.

theorem alphaHat_expected : alphaHat M.EDn M.EDs M.EPn M.EPs = M.alpha
Uses 7 · Used by 1
Statement usesExpected-count model of the McDonald–Kreitman table · Expected nonsynonymous fixed differences · Expected synonymous fixed differences · Expected nonsynonymous polymorphisms · Expected synonymous polymorphisms · Proportion of adaptive nonsynonymous substitutions · Smith–Eyre-Walker estimator of adaptive substitutions
Used byConsistency of α̂ over loci

TheoremThe MK null is neutrality#✓fully proved

The proportions of nonsynonymous changes among expected fixed differences and expected polymorphisms agree iff there are no adaptive substitutions.

theorem propNonsyn_eq_iff :
    M.EDn / (M.EDn + M.EDs) = M.EPn / (M.EPn + M.EPs) ↔ M.A = 0
Uses 5
Statement usesExpected-count model of the McDonald–Kreitman table · Expected nonsynonymous fixed differences · Expected synonymous fixed differences · Expected nonsynonymous polymorphisms · Expected synonymous polymorphisms

TheoremConsistency of α̂ over loci#✓fully proved

Let Dn i, Ds i, Pn i, Ps i be the counts at locus i; suppose each of the four sequences consists of pairwise independent, identically distributed, integrable variables whose means are the expected counts of M (the loci are exchangeable copies of the model). Then almost surely α̂ computed from the counts summed over the first m loci converges to α = A / E D_n as m → ∞.

theorem tendsto_alphaHat {Ω : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω}
    {Dn Ds Pn Ps : ℕ → Ω → ℝ}
    (hDn : Integrable (Dn 0) μ) (hDs : Integrable (Ds 0) μ)
    (hPn : Integrable (Pn 0) μ) (hPs : Integrable (Ps 0) μ)
    (iDn : Pairwise ((· ⟂ᵢ[μ] ·) on Dn)) (iDs : Pairwise ((· ⟂ᵢ[μ] ·) on Ds))
    (iPn : Pairwise ((· ⟂ᵢ[μ] ·) on Pn)) (iPs : Pairwise ((· ⟂ᵢ[μ] ·) on Ps))
    (dDn : ∀ i, IdentDistrib (Dn i) (Dn 0) μ μ) (dDs : ∀ i, IdentDistrib (Ds i) (Ds 0) μ μ)
    (dPn : ∀ i, IdentDistrib (Pn i) (Pn 0) μ μ) (dPs : ∀ i, IdentDistrib (Ps i) (Ps 0) μ μ)
    (eDn : μ[Dn 0] = M.EDn) (eDs : μ[Ds 0] = M.EDs) (ePn : μ[Pn 0] = M.EPn)
    (ePs : μ[Ps 0] = M.EPs) :
    ∀ᵐ ω ∂μ, Tendsto (fun m : ℕ => alphaHat (∑ i ∈ range m, Dn i ω) (∑ i ∈ range m, Ds i ω)
      (∑ i ∈ range m, Pn i ω) (∑ i ∈ range m, Ps i ω)) atTop (𝓝 M.alpha)
Uses 8
Statement usesExpected-count model of the McDonald–Kreitman table · Expected nonsynonymous fixed differences · Expected synonymous fixed differences · Expected nonsynonymous polymorphisms · Expected synonymous polymorphisms · Proportion of adaptive nonsynonymous substitutions · Smith–Eyre-Walker estimator of adaptive substitutions
Proof usesα̂ at the expected counts is the proportion of adaptive substitutions

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.