Rate matrices of finite continuous-time Markov chains

6 fully proved

Probability Theory

StructureRate matrix#✓fully proved

A real square matrix Q is a rate matrix (a Q-matrix in Norris's terminology) if its off-diagonal entries are nonnegative and each of its rows sums to 0 (Norris 1997, §2.1).

structure IsRateMatrix (Q : Matrix ι ι ℝ) : Prop where
  /-- The jump rates `Q i j`, `i ≠ j`, are nonnegative. -/
  nonneg_of_ne : ∀ ⦃i j : ι⦄, i ≠ j → 0 ≤ Q i j
  /-- Each row sums to `0`. -/
  sum_row : ∀ i, ∑ j, Q i j = 0

Used by 42

Used byΛ-coalescent block-counting generator is a rate matrix · Partition rate matrix is a rate matrix · The two-locus coalescent rate matrix is a rate matrix · Goldman–Yang matrix is a rate matrix · SiPhy matrix is a rate matrix · F81 matrix is a rate matrix · GTR matrix is a rate matrix · HKY85 matrix is a rate matrix · Jukes–Cantor matrix is a rate matrix · K80 matrix is a rate matrix · Stationary law of the stochastic mass-action chain on a finite class · Uniqueness in the Markov chain tree theorem · Restricted mass-action generator is a rate matrix · In-tree weights of an irreducible rate matrix are positive · Non-explosion · Law of the driving step sequence of a Markov chain · Strong Markov property at jump times · Restart law at a fixed time · Kolmogorov · Finite-dimensional distributions · Jump matrix is row-stochastic · Nonnegativity of the jump matrix · Row of the jump matrix as a probability mass function · Law of one step of the chain construction · Rows of the jump matrix sum to one · Backward equations for the mean hitting time · Backward equations for the product moment of two hitting times · Mean hitting time, first-step equation · Minimality of the mean hitting time · Product moment of two hitting times, first-step equation · Minimality of the product moment · Product moment of hitting times from inside their union is zero · Mean hitting time from inside the target set is zero · Uniformization · Diagonal of a rate matrix is minus the total jump rate · Diagonal entries of a rate matrix are nonpositive · Existence of a uniformization constant for a rate matrix · Rate matrix annihilates the constant vector · Equal-input generator is a rate matrix · Transition function of a rate matrix is row-stochastic · Nonnegativity of the transition function of a rate matrix · Rows of the transition function sum to one

Is Rate Matrix

TheoremDiagonal of a rate matrix is minus the total jump rate#✓fully proved

The diagonal entry of a rate matrix is minus the total jump rate out of the state.

theorem diag_eq [DecidableEq ι] (hQ : IsRateMatrix Q) (i : ι) :
    Q i i = -∑ j ∈ univ.erase i, Q i j

Uses 1 · Used by 4

Statement usesRate matrix

Used byRows of the jump matrix sum to one · Backward equations for the mean hitting time · Backward equations for the product moment of two hitting times · Diagonal entries of a rate matrix are nonpositive

TheoremDiagonal entries of a rate matrix are nonpositive#✓fully proved

The diagonal entries of a rate matrix are nonpositive.

theorem diag_nonpos (hQ : IsRateMatrix Q) (i : ι) : Q i i ≤ 0

Uses 2 · Used by 13

Statement usesRate matrix

Proof usesDiagonal of a rate matrix is minus the total jump rate

Used byNon-explosion · Restart law at a fixed time · Kolmogorov · Nonnegativity of the jump matrix · Backward equations for the mean hitting time · Backward equations for the product moment of two hitting times · Mean hitting time, first-step equation · Minimality of the mean hitting time · Product moment of two hitting times, first-step equation · Minimality of the product moment · Product moment of hitting times from inside their union is zero · Mean hitting time from inside the target set is zero · Existence of a uniformization constant for a rate matrix

TheoremRate matrix annihilates the constant vector#✓fully proved

A rate matrix annihilates the constant vector 1.

theorem mulVec_one (hQ : IsRateMatrix Q) : Q *ᵥ 1 = 0

Uses 1 · Used by 1

Statement usesRate matrix

Used byRows of the transition function sum to one

TheoremUniformization#✓fully proved

If c bounds every exit rate -Q i i, then Q + c • 1 has nonnegative entries (Jensen 1953).

theorem add_smul_one_nonneg [DecidableEq ι] (hQ : IsRateMatrix Q) {c : ℝ}
    (hc : ∀ i, -Q i i ≤ c) (i j : ι) :
    0 ≤ (Q + c • (1 : Matrix ι ι ℝ)) i j

Uses 1 · Used by 1

Statement usesRate matrix

Used byExistence of a uniformization constant for a rate matrix

TheoremExistence of a uniformization constant for a rate matrix#✓fully proved

Every rate matrix admits a uniformization constant c ≥ 0.

theorem exists_add_smul_one_nonneg [DecidableEq ι] (hQ : IsRateMatrix Q) :
    ∃ c : ℝ, 0 ≤ c ∧ ∀ i j, 0 ≤ (Q + c • (1 : Matrix ι ι ℝ)) i j

Uses 3 · Used by 1

Statement usesRate matrix

Proof usesUniformization · Diagonal entries of a rate matrix are nonpositive

Used byNonnegativity of the transition function of a rate matrix

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.