The transition semigroup of a finite continuous-time Markov chain

13 fully proved

Probability Theory

DefinitionTransition semigroup of a continuous-time Markov chain#✓fully proved

The transition function P t = exp (t • Q) of the finite continuous-time Markov chain with generator Q (Norris 1997, Theorem 2.1.1).

noncomputable def ctmcTransition (Q : Matrix ι ι ℝ) (t : ℝ) : Matrix ι ι ℝ :=
  exp (t • Q)

Used by 26

Used byPartition coalescent transition matrix is row-stochastic · Time-t marginal as a continuous-time chain transition · Reversible continuous-time models give reversible semigroups · Equal-rates GTR chain is the Jukes–Cantor model · Time-reversibility of the GTR chain · Base frequencies are stationary for the GTR chain · Stationary law of the stochastic mass-action chain on a finite class · Restart law at a fixed time · Kolmogorov · Finite-dimensional distributions · Detailed balance propagates to the transition function · Detailed balance implies invariance for the transition semigroup · Invariance under the semigroup · The sticky kernel is the equal-input transition function · Generator commutes with the transition function · Chapman–Kolmogorov equation for the transition semigroup · Uniformization · Transition function of a rate matrix is row-stochastic · Transition function fixes the constant vector · Nonnegativity of the transition function of a rate matrix · Exponential of a nonnegative matrix is nonnegative · Rescaling the generator rescales time · Transition function at time zero is the identity · Kolmogorov backward equation · Kolmogorov forward equation · Rows of the transition function sum to one

TheoremTransition function at time zero is the identity#✓fully proved

At time 0 the transition function is the identity.

@[simp]
theorem ctmcTransition_zero : ctmcTransition Q 0 = 1

Uses 1 · Used by 1

Statement usesTransition semigroup of a continuous-time Markov chain

Used byKolmogorov

TheoremChapman–Kolmogorov equation for the transition semigroup#✓fully proved

The semigroup property (Chapman–Kolmogorov equation): P (s + t) = P s * P t.

theorem ctmcTransition_add (s t : ℝ) :
    ctmcTransition Q (s + t) = ctmcTransition Q s * ctmcTransition Q t

Uses 1 · Used by 1

Statement usesTransition semigroup of a continuous-time Markov chain

Used byReversible continuous-time models give reversible semigroups

TheoremRescaling the generator rescales time#✓fully proved

Rescaling the generator rescales time: exp (t • (a • Q)) = exp ((a * t) • Q).

theorem ctmcTransition_smul (a t : ℝ) : ctmcTransition (a • Q) t = ctmcTransition Q (a * t)

Uses 1

Statement usesTransition semigroup of a continuous-time Markov chain

TheoremGenerator commutes with the transition function#✓fully proved

The generator commutes with the transition function.

theorem commute_ctmcTransition (t : ℝ) : Commute Q (ctmcTransition Q t)

Uses 1

Statement usesTransition semigroup of a continuous-time Markov chain

TheoremKolmogorov backward equation#✓fully proved

The Kolmogorov backward equation P' t = Q * P t (Norris 1997, Theorem 2.1.1).

theorem hasDerivAt_ctmcTransition_backward (t : ℝ) :
    HasDerivAt (ctmcTransition Q) (Q * ctmcTransition Q t) t

Uses 1 · Used by 1

Statement usesTransition semigroup of a continuous-time Markov chain

Used byKolmogorov

TheoremKolmogorov forward equation#✓fully proved

The Kolmogorov forward equation P' t = P t * Q (Norris 1997, Theorem 2.1.1).

theorem hasDerivAt_ctmcTransition_forward (t : ℝ) :
    HasDerivAt (ctmcTransition Q) (ctmcTransition Q t * Q) t

Uses 1

Statement usesTransition semigroup of a continuous-time Markov chain

TheoremUniformization#✓fully proved

For every real c, exp (t • Q) = e^{-c t} • exp (t • (Q + c • 1)) (Jensen 1953).

theorem ctmcTransition_eq_exp_smul_uniformized (c t : ℝ) :
    ctmcTransition Q t =
      Real.exp (-(c * t)) • ctmcTransition (Q + c • (1 : Matrix ι ι ℝ)) t

Uses 1 · Used by 1

Statement usesTransition semigroup of a continuous-time Markov chain

Used byNonnegativity of the transition function of a rate matrix

TheoremExponential of a nonnegative matrix is nonnegative#✓fully proved

If A has nonnegative entries, so does exp (t • A) for t ≥ 0.

theorem ctmcTransition_nonneg_of_nonneg {A : Matrix ι ι ℝ} (hA : ∀ i j, 0 ≤ A i j) {t : ℝ}
    (ht : 0 ≤ t) (i j : ι) : 0 ≤ ctmcTransition A t i j

Uses 1 · Used by 1

Statement usesTransition semigroup of a continuous-time Markov chain

Used byNonnegativity of the transition function of a rate matrix

TheoremTransition function fixes the constant vector#✓fully proved

If Q annihilates the constant vector 1, then P t fixes it: P t *ᵥ 1 = 1.

theorem ctmcTransition_mulVec_one {Q : Matrix ι ι ℝ} (hQ : Q *ᵥ 1 = 0) (t : ℝ) :
    ctmcTransition Q t *ᵥ 1 = 1

Uses 1 · Used by 1

Statement usesTransition semigroup of a continuous-time Markov chain

Used byRows of the transition function sum to one

Is Rate Matrix

TheoremRows of the transition function sum to one#✓fully proved

The rows of the transition function of a rate matrix sum to 1, for every real t.

theorem sum_ctmcTransition (hQ : IsRateMatrix Q) (t : ℝ) (i : ι) :
    ∑ j, ctmcTransition Q t i j = 1

Uses 4 · Used by 2

Statement usesRate matrix · Transition semigroup of a continuous-time Markov chain

Proof usesRate matrix annihilates the constant vector · Transition function fixes the constant vector

Used byKolmogorov · Transition function of a rate matrix is row-stochastic

TheoremNonnegativity of the transition function of a rate matrix#✓fully proved

The transition function of a rate matrix has nonnegative entries for t ≥ 0, by uniformization.

theorem ctmcTransition_nonneg (hQ : IsRateMatrix Q) {t : ℝ} (ht : 0 ≤ t) (i j : ι) :
    0 ≤ ctmcTransition Q t i j

Uses 5 · Used by 3

Statement usesRate matrix · Transition semigroup of a continuous-time Markov chain

Proof usesExistence of a uniformization constant for a rate matrix · Uniformization · Exponential of a nonnegative matrix is nonnegative

Used byNonnegativity of the time-t marginal · Kolmogorov · Transition function of a rate matrix is row-stochastic

TheoremTransition function of a rate matrix is row-stochastic#✓fully proved

The transition function of a rate matrix is row-stochastic for t ≥ 0 (Norris 1997, Theorem 2.1.2).

theorem ctmcTransition_mem_rowStochastic (hQ : IsRateMatrix Q) {t : ℝ} (ht : 0 ≤ t) :
    ctmcTransition Q t ∈ rowStochastic ℝ ι

Uses 4 · Used by 1

Statement usesRate matrix · Transition semigroup of a continuous-time Markov chain

Proof usesNonnegativity of the transition function of a rate matrix · Rows of the transition function sum to one

Used byPartition coalescent transition matrix is row-stochastic

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.