Codon substitution models and dN/dS

AbbreviationCodon as a triple of nucleotides#✓fully proved

A codon: three nucleotides, each in Fin 4 (order A, C, G, T).

abbrev Codon := Fin 3 → Fin 4
Used by 24
Used byNonsynonymous substitution rate per nonsynonymous site (dN) · dN / dS = ω · Synonymous substitution rate per synonymous site (dS) · Positions at which two codons differ · Goldman–Yang codon exchangeability · Dependence of Goldman–Yang exchangeabilities on ω · Symmetry of Goldman–Yang exchangeabilities · Goldman–Yang codon rate matrix · Off-diagonal entries of the Goldman–Yang rate matrix · The Goldman–Yang chain is reversible · Goldman–Yang matrix is a rate matrix · Codons differing at exactly one position · Symmetry of single-position codon changes · Codon change consisting of transitions · Symmetry of transition codon changes · Stationary rate of nonsynonymous substitutions · Nonsynonymous rate is linear in ω · Positivity of the nonsynonymous rate · Number of nonsynonymous sites per codon · Stationary rate of synonymous substitutions · Synonymous rate does not depend on ω · Positivity of the synonymous rate · Number of synonymous sites per codon · Synonymous and nonsynonymous sites sum to three

DefinitionPositions at which two codons differ#✓fully proved

The positions at which two codons differ.

def diffPositions (c c' : Codon) : Finset (Fin 3) := univ.filter fun k => c k ≠ c' k
Uses 1 · Used by 8
Statement usesCodon as a triple of nucleotides
Used byGoldman–Yang codon exchangeability · Dependence of Goldman–Yang exchangeabilities on ω · Symmetry of Goldman–Yang exchangeabilities · Goldman–Yang matrix is a rate matrix · Codons differing at exactly one position · Symmetry of single-position codon changes · Positivity of the nonsynonymous rate · Positivity of the synonymous rate

DefinitionCodons differing at exactly one position#✓fully proved

Two codons differ at exactly one position.

def IsSingleChange (c c' : Codon) : Prop := (diffPositions c c').card = 1
Uses 2 · Used by 7
Statement usesCodon as a triple of nucleotides · Positions at which two codons differ
Used byGoldman–Yang codon exchangeability · Dependence of Goldman–Yang exchangeabilities on ω · Symmetry of Goldman–Yang exchangeabilities · Goldman–Yang matrix is a rate matrix · Symmetry of single-position codon changes · Positivity of the nonsynonymous rate · Positivity of the synonymous rate

DefinitionCodon change consisting of transitions#✓fully proved

Every differing position is a transition (same parity: A ↔ G or C ↔ T).

def IsTransitionChange (c c' : Codon) : Prop :=
  ∀ k, c k ≠ c' k → (c k : ℕ) % 2 = (c' k : ℕ) % 2
Uses 1 · Used by 7
Statement usesCodon as a triple of nucleotides
Used byGoldman–Yang codon exchangeability · Dependence of Goldman–Yang exchangeabilities on ω · Symmetry of Goldman–Yang exchangeabilities · Goldman–Yang matrix is a rate matrix · Symmetry of transition codon changes · Positivity of the nonsynonymous rate · Positivity of the synonymous rate

TheoremSymmetry of single-position codon changes#✓fully proved

Differing at exactly one position is symmetric.

theorem isSingleChange_comm (c c' : Codon) : IsSingleChange c c' ↔ IsSingleChange c' c
Uses 3 · Used by 1
Statement usesCodon as a triple of nucleotides · Codons differing at exactly one position
Proof usesPositions at which two codons differ
Used bySymmetry of Goldman–Yang exchangeabilities

TheoremSymmetry of transition codon changes#✓fully proved

Being a transition change is symmetric.

theorem isTransitionChange_comm (c c' : Codon) :
    IsTransitionChange c c' ↔ IsTransitionChange c' c
Uses 2 · Used by 1
Statement usesCodon as a triple of nucleotides · Codon change consisting of transitions
Used bySymmetry of Goldman–Yang exchangeabilities

DefinitionGoldman–Yang codon exchangeability#✓fully proved

The Goldman–Yang exchangeability between codons i and j: 0 unless they differ at one position; otherwise κ for a transition (1 for a transversion), times ω if the amino acid changes.

def gyExchange (nuc : ι → Codon) (aa : ι → α) (κ ω : ℝ) : Matrix ι ι ℝ :=
  Matrix.of fun i j =>
    if IsSingleChange (nuc i) (nuc j) then
      (if IsTransitionChange (nuc i) (nuc j) then κ else 1) * (if aa i = aa j then 1 else ω)
    else 0
Uses 4 · Used by 10
Statement usesCodon as a triple of nucleotides · Codons differing at exactly one position · Codon change consisting of transitions · Positions at which two codons differ
Used byDependence of Goldman–Yang exchangeabilities on ω · Symmetry of Goldman–Yang exchangeabilities · Goldman–Yang codon rate matrix · Off-diagonal entries of the Goldman–Yang rate matrix · The Goldman–Yang chain is reversible · Goldman–Yang matrix is a rate matrix · Nonsynonymous rate is linear in ω · Positivity of the nonsynonymous rate · Synonymous rate does not depend on ω · Positivity of the synonymous rate

TheoremSymmetry of Goldman–Yang exchangeabilities#✓fully proved

The Goldman–Yang exchangeabilities are symmetric.

theorem gyExchange_symm (nuc : ι → Codon) (aa : ι → α) (κ ω : ℝ) (i j : ι) :
    gyExchange nuc aa κ ω i j = gyExchange nuc aa κ ω j i
Uses 7 · Used by 1
Statement usesCodon as a triple of nucleotides · Goldman–Yang codon exchangeability
Proof usesCodons differing at exactly one position · Codon change consisting of transitions · Positions at which two codons differ · Symmetry of single-position codon changes · Symmetry of transition codon changes
Used byThe Goldman–Yang chain is reversible

TheoremDependence of Goldman–Yang exchangeabilities on ω#✓fully proved

The nonsynonymous exchangeabilities are linear in ω, the synonymous ones do not involve it.

theorem gyExchange_eq (nuc : ι → Codon) (aa : ι → α) (κ ω : ℝ) (i j : ι) :
    gyExchange nuc aa κ ω i j =
      (if aa i = aa j then 1 else ω) * gyExchange nuc aa κ 1 i j
Uses 5 · Used by 2
Statement usesCodon as a triple of nucleotides · Goldman–Yang codon exchangeability
Proof usesCodons differing at exactly one position · Codon change consisting of transitions · Positions at which two codons differ
Used byNonsynonymous rate is linear in ω · Synonymous rate does not depend on ω

DefinitionGoldman–Yang codon rate matrix#✓fully proved

The Goldman–Yang rate matrix (Goldman & Yang 1994): the GTR matrix with codon frequencies π and exchangeabilities gyExchange.

def gyRate (π : ι → ℝ) (nuc : ι → Codon) (aa : ι → α) (κ ω : ℝ) : Matrix ι ι ℝ :=
  gtrRate π (gyExchange nuc aa κ ω)
Uses 3 · Used by 9
Statement usesCodon as a triple of nucleotides · Goldman–Yang codon exchangeability · General time-reversible (GTR) rate matrix
Used byOff-diagonal entries of the Goldman–Yang rate matrix · The Goldman–Yang chain is reversible · Goldman–Yang matrix is a rate matrix · Stationary rate of nonsynonymous substitutions · Nonsynonymous rate is linear in ω · Positivity of the nonsynonymous rate · Stationary rate of synonymous substitutions · Synonymous rate does not depend on ω · Positivity of the synonymous rate

DefinitionStationary rate of synonymous substitutions#✓fully proved

The stationary rate of synonymous substitutions per codon, ρ_S = ∑_{i ≠ j, aa i = aa j} π_i Q_ij. This is the stationary rate when ∑ i, π i = 1; for unnormalized weights it is scaled by (∑ i, π i) ^ 2.

def synRate (π : ι → ℝ) (nuc : ι → Codon) (aa : ι → α) (κ ω : ℝ) : ℝ :=
  ∑ i, ∑ j ∈ univ.filter fun j => j ≠ i ∧ aa j = aa i, π i * gyRate π nuc aa κ ω i j
Uses 2 · Used by 7
Statement usesCodon as a triple of nucleotides · Goldman–Yang codon rate matrix
Used bydN / dS = ω · Synonymous substitution rate per synonymous site (dS) · Number of nonsynonymous sites per codon · Synonymous rate does not depend on ω · Positivity of the synonymous rate · Number of synonymous sites per codon · Synonymous and nonsynonymous sites sum to three

DefinitionStationary rate of nonsynonymous substitutions#✓fully proved

The stationary rate of nonsynonymous substitutions per codon, ρ_N = ∑_{aa i ≠ aa j} π_i Q_ij. This is the stationary rate when ∑ i, π i = 1; for unnormalized weights it is scaled by (∑ i, π i) ^ 2.

def nonsynRate (π : ι → ℝ) (nuc : ι → Codon) (aa : ι → α) (κ ω : ℝ) : ℝ :=
  ∑ i, ∑ j ∈ univ.filter fun j => aa j ≠ aa i, π i * gyRate π nuc aa κ ω i j
Uses 2 · Used by 7
Statement usesCodon as a triple of nucleotides · Goldman–Yang codon rate matrix
Used byNonsynonymous substitution rate per nonsynonymous site (dN) · dN / dS = ω · Nonsynonymous rate is linear in ω · Positivity of the nonsynonymous rate · Number of nonsynonymous sites per codon · Number of synonymous sites per codon · Synonymous and nonsynonymous sites sum to three

DefinitionNumber of synonymous sites per codon#✓fully proved

The number of synonymous sites per codon, counted under ω = 1: S = 3 ρ_S(1) / (ρ_S(1) + ρ_N(1)).

def synSites (π : ι → ℝ) (nuc : ι → Codon) (aa : ι → α) (κ : ℝ) : ℝ :=
  3 * synRate π nuc aa κ 1 / (synRate π nuc aa κ 1 + nonsynRate π nuc aa κ 1)
Uses 3 · Used by 3
Statement usesCodon as a triple of nucleotides · Stationary rate of nonsynonymous substitutions · Stationary rate of synonymous substitutions
Used bydN / dS = ω · Synonymous substitution rate per synonymous site (dS) · Synonymous and nonsynonymous sites sum to three

DefinitionNumber of nonsynonymous sites per codon#✓fully proved

The number of nonsynonymous sites per codon, counted under ω = 1: N = 3 ρ_N(1) / (ρ_S(1) + ρ_N(1)).

def nonsynSites (π : ι → ℝ) (nuc : ι → Codon) (aa : ι → α) (κ : ℝ) : ℝ :=
  3 * nonsynRate π nuc aa κ 1 / (synRate π nuc aa κ 1 + nonsynRate π nuc aa κ 1)
Uses 3 · Used by 3
Statement usesCodon as a triple of nucleotides · Stationary rate of nonsynonymous substitutions · Stationary rate of synonymous substitutions
Used byNonsynonymous substitution rate per nonsynonymous site (dN) · dN / dS = ω · Synonymous and nonsynonymous sites sum to three

DefinitionSynonymous substitution rate per synonymous site (dS)#✓fully proved

The synonymous rate per synonymous site, dS = ρ_S(ω) / S.

def dS (π : ι → ℝ) (nuc : ι → Codon) (aa : ι → α) (κ ω : ℝ) : ℝ :=
  synRate π nuc aa κ ω / synSites π nuc aa κ
Uses 3 · Used by 1
Statement usesCodon as a triple of nucleotides · Stationary rate of synonymous substitutions · Number of synonymous sites per codon
Used bydN / dS = ω

DefinitionNonsynonymous substitution rate per nonsynonymous site (dN)#✓fully proved

The nonsynonymous rate per nonsynonymous site, dN = ρ_N(ω) / N.

def dN (π : ι → ℝ) (nuc : ι → Codon) (aa : ι → α) (κ ω : ℝ) : ℝ :=
  nonsynRate π nuc aa κ ω / nonsynSites π nuc aa κ
Uses 3 · Used by 1
Statement usesCodon as a triple of nucleotides · Stationary rate of nonsynonymous substitutions · Number of nonsynonymous sites per codon
Used bydN / dS = ω

TheoremOff-diagonal entries of the Goldman–Yang rate matrix#✓fully proved

Off the diagonal the Goldman–Yang rate is gyExchange i j * π j.

theorem gyRate_of_ne {i j : ι} (h : i ≠ j) :
    gyRate π nuc aa κ ω i j = gyExchange nuc aa κ ω i j * π j
Uses 3 · Used by 4
Statement usesCodon as a triple of nucleotides · Goldman–Yang codon exchangeability · Goldman–Yang codon rate matrix
Used byNonsynonymous rate is linear in ω · Positivity of the nonsynonymous rate · Synonymous rate does not depend on ω · Positivity of the synonymous rate

TheoremGoldman–Yang matrix is a rate matrix#✓fully proved

With nonnegative frequencies, κ ≥ 0 and ω ≥ 0, the Goldman–Yang matrix is a rate matrix.

theorem isRateMatrix_gyRate {π : ι → ℝ} (hπ : ∀ i, 0 ≤ π i) {κ ω : ℝ} (hκ : 0 ≤ κ)
    (hω : 0 ≤ ω) : IsRateMatrix (gyRate π nuc aa κ ω)
Uses 8
Statement usesCodon as a triple of nucleotides · Goldman–Yang codon rate matrix · Rate matrix
Proof usesCodons differing at exactly one position · Codon change consisting of transitions · Positions at which two codons differ · Goldman–Yang codon exchangeability · GTR matrix is a rate matrix

TheoremThe Goldman–Yang chain is reversible#✓fully proved

It is in detailed balance with its codon frequencies.

theorem isDetailedBalance_gyRate : IsDetailedBalance π (gyRate π nuc aa κ ω)
Uses 6
Statement usesCodon as a triple of nucleotides · Goldman–Yang codon rate matrix · Detailed balance
Proof usesGoldman–Yang codon exchangeability · Symmetry of Goldman–Yang exchangeabilities · GTR is reversible

TheoremSynonymous rate does not depend on ω#✓fully proved

The synonymous rate does not depend on ω: ρ_S(ω) = ρ_S(1).

theorem synRate_eq : synRate π nuc aa κ ω = synRate π nuc aa κ 1
Uses 6 · Used by 1
Statement usesCodon as a triple of nucleotides · Stationary rate of synonymous substitutions
Proof usesGoldman–Yang codon exchangeability · Dependence of Goldman–Yang exchangeabilities on ω · Goldman–Yang codon rate matrix · Off-diagonal entries of the Goldman–Yang rate matrix
Used bydN / dS = ω

TheoremNonsynonymous rate is linear in ω#✓fully proved

The nonsynonymous rate is linear in ω: ρ_N(ω) = ω ρ_N(1).

theorem nonsynRate_eq : nonsynRate π nuc aa κ ω = ω * nonsynRate π nuc aa κ 1
Uses 6 · Used by 1
Statement usesCodon as a triple of nucleotides · Stationary rate of nonsynonymous substitutions
Proof usesGoldman–Yang codon exchangeability · Dependence of Goldman–Yang exchangeabilities on ω · Goldman–Yang codon rate matrix · Off-diagonal entries of the Goldman–Yang rate matrix
Used bydN / dS = ω

TheoremSynonymous and nonsynonymous sites sum to three#✓fully proved

There are three sites per codon: S + N = 3 when ρ_S(1) + ρ_N(1) ≠ 0.

theorem synSites_add_nonsynSites (h : synRate π nuc aa κ 1 + nonsynRate π nuc aa κ 1 ≠ 0) :
    synSites π nuc aa κ + nonsynSites π nuc aa κ = 3
Uses 5
Statement usesCodon as a triple of nucleotides · Stationary rate of nonsynonymous substitutions · Number of nonsynonymous sites per codon · Stationary rate of synonymous substitutions · Number of synonymous sites per codon

TheoremdN / dS = ω#✓fully proved

dN / dS = ω in the Goldman–Yang model with sites counted under ω = 1 (derived; see the module docstring for the site definition), provided ρ_S(1) > 0 and ρ_N(1) > 0.

theorem dN_div_dS (hS : 0 < synRate π nuc aa κ 1) (hN : 0 < nonsynRate π nuc aa κ 1) :
    dN π nuc aa κ ω / dS π nuc aa κ ω = ω
Uses 9
Statement usesCodon as a triple of nucleotides · Nonsynonymous substitution rate per nonsynonymous site (dN) · Synonymous substitution rate per synonymous site (dS) · Stationary rate of nonsynonymous substitutions · Stationary rate of synonymous substitutions
Proof usesNonsynonymous rate is linear in ω · Number of nonsynonymous sites per codon · Synonymous rate does not depend on ω · Number of synonymous sites per codon

TheoremPositivity of the synonymous rate#✓fully proved

ρ_S(1) > 0 if the frequencies are nonnegative, κ > 0, and some synonymous single change joins two codons of positive frequency.

theorem synRate_pos_of_mem {π : ι → ℝ} (hπ : ∀ i, 0 ≤ π i) {κ : ℝ} (hκ : 0 < κ) {i j : ι}
    (hij : i ≠ j) (haa : aa i = aa j) (hs : IsSingleChange (nuc i) (nuc j)) (hi : 0 < π i)
    (hj : 0 < π j) : 0 < synRate π nuc aa κ 1
Uses 8
Statement usesCodon as a triple of nucleotides · Codons differing at exactly one position · Stationary rate of synonymous substitutions
Proof usesCodon change consisting of transitions · Positions at which two codons differ · Goldman–Yang codon exchangeability · Goldman–Yang codon rate matrix · Off-diagonal entries of the Goldman–Yang rate matrix

TheoremPositivity of the nonsynonymous rate#✓fully proved

ρ_N(1) > 0 if the frequencies are nonnegative, κ > 0, and some nonsynonymous single change joins two codons of positive frequency.

theorem nonsynRate_pos_of_mem {π : ι → ℝ} (hπ : ∀ i, 0 ≤ π i) {κ : ℝ} (hκ : 0 < κ) {i j : ι}
    (haa : aa i ≠ aa j) (hs : IsSingleChange (nuc i) (nuc j)) (hi : 0 < π i)
    (hj : 0 < π j) : 0 < nonsynRate π nuc aa κ 1
Uses 8
Statement usesCodon as a triple of nucleotides · Codons differing at exactly one position · Stationary rate of nonsynonymous substitutions
Proof usesCodon change consisting of transitions · Positions at which two codons differ · Goldman–Yang codon exchangeability · Goldman–Yang codon rate matrix · Off-diagonal entries of the Goldman–Yang rate matrix
25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.