Time-reversible nucleotide substitution models

DefinitionGeneral time-reversible (GTR) rate matrix#✓fully proved

The GTR rate matrix (Tavaré 1986) with base frequencies π and exchangeabilities s: s i j * π j off the diagonal and minus the off-diagonal row sum on it. The diagonal of s is not used.

noncomputable def gtrRate (π : ι → ℝ) (s : Matrix ι ι ℝ) : Matrix ι ι ℝ :=
  Matrix.of fun i j => if i = j then -∑ k ∈ univ.erase i, s i k * π k else s i j * π j

Used by 17

Used byGoldman–Yang codon rate matrix · Eq. 6 for the SiPhy matrix · π is the equilibrium of the SiPhy matrix · SiPhy matrix is a rate matrix · The SiPhy rate matrix · Equal-rates GTR chain is the Jukes–Cantor model · F81 rate matrix · JC69 is the equal-rates GTR model · HKY85 rate matrix · HKY85 with κ = 1 is F81 · Time-reversibility of the GTR chain · GTR is reversible · GTR matrix is a rate matrix · K80 with κ = 1 is the Jukes–Cantor model · Rows of the GTR rate matrix sum to zero · Base frequencies are stationary for the GTR chain · Base frequencies are invariant for the GTR generator

TheoremRows of the GTR rate matrix sum to zero#✓fully proved

The rows of the GTR matrix sum to 0, for all parameters.

theorem sum_gtrRate (π : ι → ℝ) (s : Matrix ι ι ℝ) (i : ι) : ∑ j, gtrRate π s i j = 0

Uses 1 · Used by 3

Statement usesGeneral time-reversible (GTR) rate matrix

Used byGTR matrix is a rate matrix · Base frequencies are stationary for the GTR chain · Base frequencies are invariant for the GTR generator

TheoremGTR matrix is a rate matrix#✓fully proved

With nonnegative base frequencies and nonnegative off-diagonal exchangeabilities, the GTR matrix is a rate matrix (the diagonal s i i is not used by gtrRate).

theorem isRateMatrix_gtrRate {π : ι → ℝ} {s : Matrix ι ι ℝ} (hπ : ∀ i, 0 ≤ π i)
    (hs : ∀ i j, i ≠ j → 0 ≤ s i j) : IsRateMatrix (gtrRate π s)

Uses 3 · Used by 4

Statement usesGeneral time-reversible (GTR) rate matrix · Rate matrix

Proof usesRows of the GTR rate matrix sum to zero

Used byGoldman–Yang matrix is a rate matrix · SiPhy matrix is a rate matrix · F81 matrix is a rate matrix · HKY85 matrix is a rate matrix

TheoremGTR is reversible#✓fully proved

With symmetric exchangeabilities, the GTR matrix is in detailed balance with its base frequencies, π i Q i j = π j Q j i (Tavaré 1986).

theorem isDetailedBalance_gtrRate (π : ι → ℝ) {s : Matrix ι ι ℝ} (hs : ∀ i j, s i j = s j i) :
    IsDetailedBalance π (gtrRate π s)

Uses 2 · Used by 7

Statement usesGeneral time-reversible (GTR) rate matrix · Detailed balance

Used byThe Goldman–Yang chain is reversible · π is the equilibrium of the SiPhy matrix · Time-reversibility of the GTR chain · Detailed balance of the F81 model · Detailed balance of the HKY85 model · Base frequencies are stationary for the GTR chain · Base frequencies are invariant for the GTR generator

TheoremBase frequencies are invariant for the GTR generator#✓fully proved

The base frequencies are invariant for the GTR generator: π Q = 0.

theorem vecMul_gtrRate (π : ι → ℝ) {s : Matrix ι ι ℝ} (hs : ∀ i j, s i j = s j i) :
    π ᵥ* gtrRate π s = 0

Uses 4

Statement usesGeneral time-reversible (GTR) rate matrix

Proof usesGTR is reversible · Rows of the GTR rate matrix sum to zero · Detailed balance implies invariance for the generator

TheoremBase frequencies are stationary for the GTR chain#✓fully proved

The base frequencies are stationary for the GTR transition function at every time.

theorem vecMul_ctmcTransition_gtrRate (π : ι → ℝ) {s : Matrix ι ι ℝ}
    (hs : ∀ i j, s i j = s j i) (t : ℝ) : π ᵥ* ctmcTransition (gtrRate π s) t = π

Uses 5

Statement usesGeneral time-reversible (GTR) rate matrix · Transition semigroup of a continuous-time Markov chain

Proof usesGTR is reversible · Rows of the GTR rate matrix sum to zero · Detailed balance implies invariance for the transition semigroup

TheoremTime-reversibility of the GTR chain#✓fully proved

Detailed balance of the GTR transition function with the base frequencies, π i P t i j = π j P t j i for every t (time-reversibility of the GTR chain).

theorem isDetailedBalance_ctmcTransition_gtrRate (π : ι → ℝ) {s : Matrix ι ι ℝ}
    (hs : ∀ i j, s i j = s j i) (t : ℝ) :
    IsDetailedBalance π (ctmcTransition (gtrRate π s) t)

Uses 5

Statement usesGeneral time-reversible (GTR) rate matrix · Detailed balance · Transition semigroup of a continuous-time Markov chain

Proof usesGTR is reversible · Detailed balance propagates to the transition function

21 fully proved

Nucleotide models on Fin 4 (order A, C, G, T)

DefinitionHKY85 exchangeabilities#✓fully proved

The HKY85 exchangeabilities: κ for a transition (indices of equal parity: A ↔ G, C ↔ T in the order A, C, G, T), 1 for a transversion. The diagonal (also κ) is not used by gtrRate.

def hkyExchangeability (κ : ℝ) : Matrix (Fin 4) (Fin 4) ℝ :=
  Matrix.of fun i j => if (i : ℕ) % 2 = (j : ℕ) % 2 then κ else 1

Used by 4

Used byHKY85 rate matrix · HKY85 with κ = 1 is F81 · Detailed balance of the HKY85 model · HKY85 matrix is a rate matrix

DefinitionHKY85 rate matrix#✓fully proved

The HKY85 rate matrix (Hasegawa–Kishino–Yano 1985) with base frequencies π and transition/transversion ratio κ: rate κ π j for a transition to j, π j for a transversion.

noncomputable def hkyRate (π : Fin 4 → ℝ) (κ : ℝ) : Matrix (Fin 4) (Fin 4) ℝ :=
  gtrRate π (hkyExchangeability κ)

Uses 2 · Used by 5

Statement usesGeneral time-reversible (GTR) rate matrix · HKY85 exchangeabilities

Used byHKY85 with κ = 1 is F81 · Detailed balance of the HKY85 model · HKY85 matrix is a rate matrix · K80 rate matrix · K80 with κ = 1 is the Jukes–Cantor model

DefinitionF81 rate matrix#✓fully proved

The F81 rate matrix (Felsenstein 1981): rate π j to every other base j.

noncomputable def f81Rate (π : Fin 4 → ℝ) : Matrix (Fin 4) (Fin 4) ℝ :=
  gtrRate π (Matrix.of fun _ _ => 1)

Uses 1 · Used by 4

Statement usesGeneral time-reversible (GTR) rate matrix

Used byHKY85 with κ = 1 is F81 · Detailed balance of the F81 model · F81 matrix is a rate matrix · K80 with κ = 1 is the Jukes–Cantor model

DefinitionK80 rate matrix#✓fully proved

The K80 rate matrix (Kimura 1980): equal base frequencies 1/4, rate κ / 4 for a transition and 1 / 4 for each transversion.

noncomputable def k80Rate (κ : ℝ) : Matrix (Fin 4) (Fin 4) ℝ :=
  hkyRate (fun _ => 1 / 4) κ

Uses 1 · Used by 2

Statement usesHKY85 rate matrix

Used byK80 matrix is a rate matrix · K80 with κ = 1 is the Jukes–Cantor model

TheoremHKY85 matrix is a rate matrix#✓fully proved

With nonnegative base frequencies and κ ≥ 0, the HKY85 matrix is a rate matrix.

theorem isRateMatrix_hkyRate {π : Fin 4 → ℝ} {κ : ℝ} (hπ : ∀ i, 0 ≤ π i) (hκ : 0 ≤ κ) :
    IsRateMatrix (hkyRate π κ)

Uses 4 · Used by 1

Statement usesHKY85 rate matrix · Rate matrix

Proof usesHKY85 exchangeabilities · GTR matrix is a rate matrix

Used byK80 matrix is a rate matrix

TheoremF81 matrix is a rate matrix#✓fully proved

With nonnegative base frequencies, the F81 matrix is a rate matrix.

theorem isRateMatrix_f81Rate {π : Fin 4 → ℝ} (hπ : ∀ i, 0 ≤ π i) : IsRateMatrix (f81Rate π)

Uses 3

Statement usesF81 rate matrix · Rate matrix

Proof usesGTR matrix is a rate matrix

TheoremK80 matrix is a rate matrix#✓fully proved

With κ ≥ 0, the K80 matrix is a rate matrix.

theorem isRateMatrix_k80Rate {κ : ℝ} (hκ : 0 ≤ κ) : IsRateMatrix (k80Rate κ)

Uses 3

Statement usesK80 rate matrix · Rate matrix

Proof usesHKY85 matrix is a rate matrix

TheoremDetailed balance of the HKY85 model#✓fully proved

HKY85 is in detailed balance with its base frequencies.

theorem isDetailedBalance_hkyRate (π : Fin 4 → ℝ) (κ : ℝ) :
    IsDetailedBalance π (hkyRate π κ)

Uses 4

Statement usesHKY85 rate matrix · Detailed balance

Proof usesHKY85 exchangeabilities · GTR is reversible

TheoremDetailed balance of the F81 model#✓fully proved

F81 is in detailed balance with its base frequencies.

theorem isDetailedBalance_f81Rate (π : Fin 4 → ℝ) : IsDetailedBalance π (f81Rate π)

Uses 3

Statement usesF81 rate matrix · Detailed balance

Proof usesGTR is reversible

TheoremHKY85 with κ = 1 is F81#✓fully proved

HKY85 with κ = 1 is F81.

theorem hkyRate_one (π : Fin 4 → ℝ) : hkyRate π 1 = f81Rate π

Uses 4 · Used by 1

Statement usesF81 rate matrix · HKY85 rate matrix

Proof usesGeneral time-reversible (GTR) rate matrix · HKY85 exchangeabilities

Used byK80 with κ = 1 is the Jukes–Cantor model

The Jukes–Cantor model as the equal-rates case

TheoremJC69 is the equal-rates GTR model#✓fully proved

Equal base frequencies 1/4 and equal exchangeabilities 4 μ / 3 give the Jukes–Cantor rate matrix jcRateMatrix μ.

theorem gtrRate_jukesCantor (μ : ℝ) :
    gtrRate (fun _ : Fin 4 => 1 / 4) (Matrix.of fun _ _ => 4 * μ / 3) = jcRateMatrix μ

Uses 2 · Used by 2

Statement usesJukes–Cantor rate matrix as a matrix · General time-reversible (GTR) rate matrix

Used byEqual-rates GTR chain is the Jukes–Cantor model · K80 with κ = 1 is the Jukes–Cantor model

TheoremEqual-rates GTR chain is the Jukes–Cantor model#✓fully proved

The equal-rates GTR transition function is the Jukes–Cantor transition probability jcProb μ t (by JukesCantor.jcProb_eq_exp).

theorem ctmcTransition_gtrRate_jukesCantor (μ t : ℝ) (i j : Fin 4) :
    ctmcTransition (gtrRate (fun _ : Fin 4 => 1 / 4) (Matrix.of fun _ _ => 4 * μ / 3)) t i j =
      jcProb μ t i j

Uses 6

Statement usesJukes–Cantor transition probability · General time-reversible (GTR) rate matrix · Transition semigroup of a continuous-time Markov chain

Proof usesThe Jukes–Cantor transition matrix is the matrix exponential of the rate matrix · Jukes–Cantor rate matrix as a matrix · JC69 is the equal-rates GTR model

TheoremJukes–Cantor matrix is a rate matrix#✓fully proved

For μ ≥ 0 the Jukes–Cantor matrix is a rate matrix.

theorem isRateMatrix_jcRateMatrix {μ : ℝ} (hμ : 0 ≤ μ) : IsRateMatrix (jcRateMatrix μ)

Uses 4

Statement usesJukes–Cantor rate matrix as a matrix · Rate matrix

Proof usesNonnegativity of off-diagonal Jukes–Cantor rates · Rows of the Jukes–Cantor rate matrix sum to zero

TheoremK80 with κ = 1 is the Jukes–Cantor model#✓fully proved

K80 with κ = 1 is JC69 with substitution rate μ = 3/4.

theorem k80Rate_one : k80Rate 1 = jcRateMatrix (3 / 4)

Uses 7

Statement usesJukes–Cantor rate matrix as a matrix · K80 rate matrix

Proof usesF81 rate matrix · General time-reversible (GTR) rate matrix · JC69 is the equal-rates GTR model · HKY85 rate matrix · HKY85 with κ = 1 is F81

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.