Stationarity and detailed balance for finite continuous-time Markov chains

5 fully proved

Probability Theory

DefinitionDetailed balance#✓fully proved

The row vector π is in detailed balance with the matrix Q: π i * Q i j = π j * Q j i for all i j (Norris 1997, §3.7). This is only the algebraic equation: it holds for π = 0 and every Q. For a probability vector π and a stochastic matrix it is the reversibility of the chain started from π.

def IsDetailedBalance (π : ι → ℝ) (Q : Matrix ι ι ℝ) : Prop :=
  ∀ i j, π i * Q i j = π j * Q j i

Used by 10

Used byThe Goldman–Yang chain is reversible · π is the equilibrium of the SiPhy matrix · Reversible continuous-time models give reversible semigroups · Time-reversibility of the GTR chain · Detailed balance of the F81 model · GTR is reversible · Detailed balance of the HKY85 model · Detailed balance propagates to the transition function · Detailed balance implies invariance for the transition semigroup · Detailed balance implies invariance for the generator

TheoremInvariance under the semigroup#✓fully proved

π Q = 0 if and only if π P t = π for every real t (Norris 1997, §3.5, finite state space).

theorem vecMul_eq_zero_iff_forall_vecMul_ctmcTransition [DecidableEq ι] (π : ι → ℝ)
    (Q : Matrix ι ι ℝ) :
    π ᵥ* Q = 0 ↔ ∀ t, π ᵥ* ctmcTransition Q t = π

Uses 1 · Used by 2

Statement usesTransition semigroup of a continuous-time Markov chain

Used byStationary law of the stochastic mass-action chain on a finite class · Detailed balance implies invariance for the transition semigroup

Is Detailed Balance

TheoremDetailed balance implies invariance for the generator#✓fully proved

Detailed balance with a matrix whose rows sum to 0 implies invariance π Q = 0 (Norris 1997, §3.7).

theorem vecMul_eq_zero (h : IsDetailedBalance π Q) (hQ : ∀ i, ∑ j, Q i j = 0) :
    π ᵥ* Q = 0

Uses 1 · Used by 2

Statement usesDetailed balance

Used byBase frequencies are invariant for the GTR generator · Detailed balance implies invariance for the transition semigroup

TheoremDetailed balance propagates to the transition function#✓fully proved

Detailed balance for Q implies π i P t i j = π j P t j i for every t (Norris 1997, §3.7). For a probability vector π and a rate matrix Q this is the reversibility of the chain started from π.

theorem ctmcTransition [DecidableEq ι] (h : IsDetailedBalance π Q) (t : ℝ) :
    IsDetailedBalance π (ctmcTransition Q t)

Uses 2 · Used by 2

Statement usesDetailed balance · Transition semigroup of a continuous-time Markov chain

Used byReversible continuous-time models give reversible semigroups · Time-reversibility of the GTR chain

TheoremDetailed balance implies invariance for the transition semigroup#✓fully proved

Detailed balance with a matrix whose rows sum to 0 (for instance a rate matrix) makes π invariant for every P t.

theorem vecMul_ctmcTransition [DecidableEq ι] (h : IsDetailedBalance π Q)
    (hQ : ∀ i, ∑ j, Q i j = 0) (t : ℝ) :
    π ᵥ* ProbabilityTheory.ctmcTransition Q t = π

Uses 4 · Used by 1

Statement usesDetailed balance · Transition semigroup of a continuous-time Markov chain

Proof usesDetailed balance implies invariance for the generator · Invariance under the semigroup

Used byBase frequencies are stationary for the GTR chain

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.