Jukes–Cantor model

DefinitionJukes–Cantor transition probability#✓fully proved

The Jukes–Cantor transition probability from base i to base j over a branch of length t, with substitution rate μ.

noncomputable def jcProb (μ t : ℝ) (i j : Fin 4) : ℝ :=
  if i = j then 1 / 4 + 3 / 4 * exp (-4 * μ * t / 3) else 1 / 4 - 1 / 4 * exp (-4 * μ * t / 3)

Used by 17

Used byDetailed balance of the Jukes–Cantor chain · Kolmogorov forward equation · The Jukes–Cantor transition matrix is the matrix exponential of the rate matrix · Nonnegativity of Jukes–Cantor transition probabilities · Jukes–Cantor transition matrix at time zero is the identity · Jukes–Cantor transition matrix as a stochastic matrix · Chapman–Kolmogorov equation for the Jukes–Cantor chain · Probability that the ends of a branch differ · Closed form of the Jukes–Cantor difference probability · Rows of the Jukes–Cantor transition matrix sum to one · Chapman–Kolmogorov equation · Right-hand side of the Jukes–Cantor forward equation in closed form · Statistical consistency of neighbor joining under Jukes–Cantor · JC-corrected distances are path lengths · Jukes–Cantor transition matrix along a path · Chapman–Kolmogorov along a path · Equal-rates GTR chain is the Jukes–Cantor model

DefinitionJukes–Cantor rate matrix#✓fully proved

The Jukes–Cantor rate matrix: rate μ / 3 to each other base, -μ on the diagonal.

noncomputable def jcRate (μ : ℝ) (k j : Fin 4) : ℝ :=
  if k = j then -μ else μ / 3

Used by 6

Used byKolmogorov forward equation · Jukes–Cantor rate matrix as a matrix · Nonnegativity of off-diagonal Jukes–Cantor rates · Diagonalization of the Jukes–Cantor rate matrix · Right-hand side of the Jukes–Cantor forward equation in closed form · Rows of the Jukes–Cantor rate matrix sum to zero

DefinitionProbability that the ends of a branch differ#✓fully proved

The probability that the two ends of a branch of length t carry different bases, given base i at the start.

noncomputable def pDiff (μ t : ℝ) (i : Fin 4) : ℝ :=
  ∑ j ∈ univ.erase i, jcProb μ t i j

Uses 1 · Used by 6

Statement usesJukes–Cantor transition probability

Used byThe Jukes–Cantor distance correction · Closed form of the Jukes–Cantor difference probability · Jukes–Cantor difference probability is below 3/4 · Jukes–Cantor difference probability lies in (0, 3/4) · Nonnegativity of the Jukes–Cantor difference probability · Statistical consistency of neighbor joining under Jukes–Cantor

DefinitionJukes–Cantor distance#✓fully proved

The Jukes–Cantor distance: the expected number of substitutions per site corresponding to a proportion p of differing sites. Meaningful only for 0 ≤ p < 3/4; outside that range the value is Lean's totalized logarithm, not a distance (at p = 3/4 it is 0).

noncomputable def jcDistance (p : ℝ) : ℝ :=
  -(3 / 4) * log (1 - 4 / 3 * p)

Used by 4

Used byThe Jukes–Cantor distance correction · Statistical consistency of neighbor joining under Jukes–Cantor · JC-corrected distances are path lengths · Jukes–Cantor corrected empirical distance

TheoremNonnegativity of off-diagonal Jukes–Cantor rates#✓fully proved

Off-diagonal Jukes–Cantor rates are nonnegative when 0 ≤ μ.

theorem jcRate_nonneg {μ : ℝ} (hμ : 0 ≤ μ) {k j : Fin 4} (h : k ≠ j) : 0 ≤ jcRate μ k j

Uses 1 · Used by 1

Statement usesJukes–Cantor rate matrix

Used byJukes–Cantor matrix is a rate matrix

TheoremRows of the Jukes–Cantor rate matrix sum to zero#✓fully proved

Each row of the Jukes–Cantor rate matrix sums to 0.

theorem sum_jcRate (μ : ℝ) (k : Fin 4) : ∑ j, jcRate μ k j = 0

Uses 1 · Used by 1

Statement usesJukes–Cantor rate matrix

Used byJukes–Cantor matrix is a rate matrix

TheoremRows of the Jukes–Cantor transition matrix sum to one#✓fully proved

Each row of the Jukes–Cantor transition matrix sums to 1.

theorem sum_jcProb (μ t : ℝ) (i : Fin 4) : ∑ j, jcProb μ t i j = 1

Uses 1 · Used by 2

Statement usesJukes–Cantor transition probability

Used byJukes–Cantor transition matrix as a stochastic matrix · Closed form of the Jukes–Cantor difference probability

TheoremNonnegativity of Jukes–Cantor transition probabilities#✓fully proved

The Jukes–Cantor transition probabilities are nonnegative when 0 ≤ μ * t.

theorem jcProb_nonneg {μ t : ℝ} (h : 0 ≤ μ * t) (i j : Fin 4) : 0 ≤ jcProb μ t i j

Uses 1 · Used by 1

Statement usesJukes–Cantor transition probability

Used byJukes–Cantor transition matrix as a stochastic matrix

TheoremJukes–Cantor transition matrix at time zero is the identity#✓fully proved

At time 0 the Jukes–Cantor transition matrix is the identity.

theorem jcProb_zero (μ : ℝ) (i j : Fin 4) : jcProb μ 0 i j = if i = j then 1 else 0

Uses 1 · Used by 2

Statement usesJukes–Cantor transition probability

Used byChapman–Kolmogorov equation for the Jukes–Cantor chain · Chapman–Kolmogorov along a path

TheoremChapman–Kolmogorov equation#✓fully proved

Chapman–Kolmogorov equation for the Jukes–Cantor model.

theorem sum_jcProb_mul_jcProb (μ s t : ℝ) (i j : Fin 4) :
    ∑ k, jcProb μ s i k * jcProb μ t k j = jcProb μ (s + t) i j

Uses 1 · Used by 2

Statement usesJukes–Cantor transition probability

Used byChapman–Kolmogorov equation for the Jukes–Cantor chain · Chapman–Kolmogorov along a path

TheoremRight-hand side of the Jukes–Cantor forward equation in closed form#✓fully proved

The right-hand side of the forward equation, in closed form.

theorem sum_jcProb_mul_jcRate (μ t : ℝ) (i j : Fin 4) :
    ∑ k, jcProb μ t i k * jcRate μ k j =
      if i = j then -μ * exp (-4 * μ * t / 3) else μ / 3 * exp (-4 * μ * t / 3)

Uses 2 · Used by 1

Statement usesJukes–Cantor transition probability · Jukes–Cantor rate matrix

Used byKolmogorov forward equation

TheoremKolmogorov forward equation#✓fully proved

Kolmogorov forward equation for the Jukes–Cantor model: d/dt P(t) = P(t) Q with Q = jcRate μ.

theorem hasDerivAt_jcProb (μ t : ℝ) (i j : Fin 4) :
    HasDerivAt (fun t => jcProb μ t i j) (∑ k, jcProb μ t i k * jcRate μ k j) t

Uses 3

Statement usesJukes–Cantor transition probability · Jukes–Cantor rate matrix

Proof usesRight-hand side of the Jukes–Cantor forward equation in closed form

TheoremClosed form of the Jukes–Cantor difference probability#✓fully proved

The probability that the two ends of a branch differ is 3/4 · (1 - exp (-4 μ t / 3)), whatever the starting base.

theorem pDiff_eq (μ t : ℝ) (i : Fin 4) :
    pDiff μ t i = 3 / 4 * (1 - exp (-4 * μ * t / 3))

Uses 3 · Used by 4

Statement usesProbability that the ends of a branch differ

Proof usesJukes–Cantor transition probability · Rows of the Jukes–Cantor transition matrix sum to one

Used byThe Jukes–Cantor distance correction · Jukes–Cantor difference probability is below 3/4 · Nonnegativity of the Jukes–Cantor difference probability · Statistical consistency of neighbor joining under Jukes–Cantor

DefinitionJukes–Cantor transition matrix as a stochastic matrix#✓fully proved

The Jukes–Cantor transition matrix over a branch with 0 ≤ μ * t, packaged as a StochasticMatrix on the four states Fin (3 + 1) so that the finite Markov-chain API (matrix powers, stationarity, detailed balance) applies to it.

noncomputable def jcStochasticMatrix (μ t : ℝ) (h : 0 ≤ μ * t) : StochasticMatrix 3 where
  prob := jcProb μ t
  nonneg := jcProb_nonneg h
  row_sum := sum_jcProb μ t

Uses 4 · Used by 2

Statement usesJukes–Cantor transition probability · Nonnegativity of Jukes–Cantor transition probabilities · Rows of the Jukes–Cantor transition matrix sum to one · Stochastic matrix

Used byDetailed balance of the Jukes–Cantor chain · Chapman–Kolmogorov equation for the Jukes–Cantor chain

TheoremChapman–Kolmogorov equation for the Jukes–Cantor chain#✓fully proved

The n-step matrix of the Jukes–Cantor chain observed every t time units is the transition matrix over the branch length n * t (Chapman–Kolmogorov).

theorem matPow_jcStochasticMatrix (μ t : ℝ) (h : 0 ≤ μ * t) (n : ℕ) (i j : Fin 4) :
    (jcStochasticMatrix μ t h).matPow n i j = jcProb μ (n * t) i j

Uses 6

Statement usesJukes–Cantor transition probability · Jukes–Cantor transition matrix as a stochastic matrix · Matrix powers of a stochastic matrix

Proof usesJukes–Cantor transition matrix at time zero is the identity · Chapman–Kolmogorov equation · Stochastic matrix

TheoremDetailed balance of the Jukes–Cantor chain#✓fully proved

The uniform distribution satisfies detailed balance with the Jukes–Cantor matrix (the matrix is symmetric), hence is stationary.

theorem detailedBalance_jcStochasticMatrix (μ t : ℝ) (h : 0 ≤ μ * t) :
    (jcStochasticMatrix μ t h).DetailedBalance
      ⟨fun _ => 1 / 4, fun _ => by norm_num, by simp⟩

Uses 5

Statement usesJukes–Cantor transition matrix as a stochastic matrix · Detailed balance · Probability distribution on a finite state space

Proof usesJukes–Cantor transition probability · Stochastic matrix

TheoremNonnegativity of the Jukes–Cantor difference probability#✓fully proved

The probability that the ends of a branch differ is nonnegative when 0 ≤ μ * t.

theorem pDiff_nonneg {μ t : ℝ} (h : 0 ≤ μ * t) (i : Fin 4) : 0 ≤ pDiff μ t i

Uses 2 · Used by 1

Statement usesProbability that the ends of a branch differ

Proof usesClosed form of the Jukes–Cantor difference probability

Used byJukes–Cantor difference probability lies in (0, 3/4)

TheoremJukes–Cantor difference probability is below 3/4#✓fully proved

The probability that the ends of a branch differ is below the saturation value 3/4, for all real μ and t (it is negative when μ * t < 0, see pDiff_mem_Ico).

theorem pDiff_lt_three_quarters (μ t : ℝ) (i : Fin 4) : pDiff μ t i < 3 / 4

Uses 2 · Used by 2

Statement usesProbability that the ends of a branch differ

Proof usesClosed form of the Jukes–Cantor difference probability

Used byJukes–Cantor difference probability lies in (0, 3/4) · Statistical consistency of neighbor joining under Jukes–Cantor

TheoremJukes–Cantor difference probability lies in (0, 3/4)#✓fully proved

For 0 ≤ μ * t the probability that the ends of a branch differ lies in [0, 3/4), the domain of jcDistance.

theorem pDiff_mem_Ico {μ t : ℝ} (h : 0 ≤ μ * t) (i : Fin 4) :
    pDiff μ t i ∈ Set.Ico 0 (3 / 4)

Uses 3

Statement usesProbability that the ends of a branch differ

Proof usesJukes–Cantor difference probability is below 3/4 · Nonnegativity of the Jukes–Cantor difference probability

TheoremThe Jukes–Cantor distance correction#✓fully proved

-(3/4) · log (1 - 4/3 · pDiff μ t i) = μ * t, the expected number of substitutions per site along the branch.

theorem jcDistance_pDiff (μ t : ℝ) (i : Fin 4) : jcDistance (pDiff μ t i) = μ * t

Uses 3 · Used by 2

Statement usesJukes–Cantor distance · Probability that the ends of a branch differ

Proof usesClosed form of the Jukes–Cantor difference probability

Used byStatistical consistency of neighbor joining under Jukes–Cantor · JC-corrected distances are path lengths

DefinitionJukes–Cantor rate matrix as a matrix#✓fully proved

The Jukes–Cantor rate matrix as a Matrix.

noncomputable def jcRateMatrix (μ : ℝ) : Matrix (Fin 4) (Fin 4) ℝ :=
  Matrix.of (jcRate μ)

Uses 1 · Used by 6

Statement usesJukes–Cantor rate matrix

Used byThe Jukes–Cantor transition matrix is the matrix exponential of the rate matrix · Diagonalization of the Jukes–Cantor rate matrix · Equal-rates GTR chain is the Jukes–Cantor model · JC69 is the equal-rates GTR model · Jukes–Cantor matrix is a rate matrix · K80 with κ = 1 is the Jukes–Cantor model

DefinitionEigenbasis of the Jukes–Cantor rate matrix#✓fully proved

An eigenbasis of the Jukes–Cantor rate matrix, as columns: the constant vector (eigenvalue 0) and three vectors with zero sum (eigenvalue -4 μ / 3).

def jcEigenbasis : Matrix (Fin 4) (Fin 4) ℝ :=
  !![1, 1, 1, 1; 1, -1, 0, 0; 1, 0, -1, 0; 1, 0, 0, -1]

Used by 3

Used byInvertible Jukes–Cantor eigenbasis · The Jukes–Cantor transition matrix is the matrix exponential of the rate matrix · Diagonalization of the Jukes–Cantor rate matrix

DefinitionInvertible Jukes–Cantor eigenbasis#✓fully proved

The eigenbasis as a unit, with its explicit inverse.

noncomputable def jcEigenbasisUnit : (Matrix (Fin 4) (Fin 4) ℝ)ˣ where
  val := jcEigenbasis
  inv := !![1/4, 1/4, 1/4, 1/4; 1/4, -3/4, 1/4, 1/4; 1/4, 1/4, -3/4, 1/4; 1/4, 1/4, 1/4, -3/4]
  val_inv := by
    ext i j
    fin_cases i <;> fin_cases j <;> norm_num [jcEigenbasis, mul_apply, Fin.sum_univ_four]
  inv_val := by
    ext i j
    fin_cases i <;> fin_cases j <;> norm_num [jcEigenbasis, mul_apply, Fin.sum_univ_four]

Uses 1 · Used by 2

Statement usesEigenbasis of the Jukes–Cantor rate matrix

Used byThe Jukes–Cantor transition matrix is the matrix exponential of the rate matrix · Diagonalization of the Jukes–Cantor rate matrix

TheoremDiagonalization of the Jukes–Cantor rate matrix#✓fully proved

Diagonalization of t • jcRateMatrix μ.

theorem smul_jcRateMatrix_eq (μ t : ℝ) :
    t • jcRateMatrix μ =
      (jcEigenbasisUnit : Matrix (Fin 4) (Fin 4) ℝ) *
        diagonal ![0, -4 * μ * t / 3, -4 * μ * t / 3, -4 * μ * t / 3] *
        (↑jcEigenbasisUnit⁻¹ : Matrix (Fin 4) (Fin 4) ℝ)

Uses 4 · Used by 1

Statement usesInvertible Jukes–Cantor eigenbasis · Jukes–Cantor rate matrix as a matrix

Proof usesEigenbasis of the Jukes–Cantor rate matrix · Jukes–Cantor rate matrix

Used byThe Jukes–Cantor transition matrix is the matrix exponential of the rate matrix

TheoremThe Jukes–Cantor transition matrix is the matrix exponential of the rate matrix#✓fully proved

jcProb μ t = exp (t • jcRateMatrix μ).

theorem jcProb_eq_exp (μ t : ℝ) (i j : Fin 4) :
    jcProb μ t i j = NormedSpace.exp (t • jcRateMatrix μ) i j

Uses 5 · Used by 1

Statement usesJukes–Cantor transition probability · Jukes–Cantor rate matrix as a matrix

Proof usesEigenbasis of the Jukes–Cantor rate matrix · Invertible Jukes–Cantor eigenbasis · Diagonalization of the Jukes–Cantor rate matrix

Used byEqual-rates GTR chain is the Jukes–Cantor model

25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.