Skip to content

Finite continuous-time Markov chains as path processes

29 fully proved

Probability Theory

DefinitionJump matrix of a rate matrix#✓fully proved

The jump matrix Π of a matrix Q (Norris 1997, §2.6): for a state with exit rate q i = -Q i i ≠ 0, Π i j = Q i j / q i for j ≠ i and Π i i = 0; a state with q i = 0 is absorbing, Π i j = δ i j.

noncomputable def ctmcJumpMatrix (Q : Matrix ι ι ℝ) : Matrix ι ι ℝ := fun i j =>
  if Q i i = 0 then (if i = j then 1 else 0) else if i = j then 0 else Q i j / -Q i i
Used by 11
Used byKolmogorov · Jump matrix is row-stochastic · Nonnegativity of the jump matrix · Row of the jump matrix as a probability mass function · 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

Is Rate Matrix

TheoremNonnegativity of the jump matrix#✓fully proved

The entries of the jump matrix of a rate matrix are nonnegative.

theorem ctmcJumpMatrix_nonneg (hQ : IsRateMatrix Q) (i j : ι) : 0 ≤ ctmcJumpMatrix Q i j
Uses 3 · Used by 9
Statement usesRate matrix · Jump matrix of a rate matrix
Proof usesDiagonal entries of a rate matrix are nonpositive
Used byKolmogorov · Jump matrix is row-stochastic · Row of the jump matrix as a probability mass function · 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

TheoremRows of the jump matrix sum to one#✓fully proved

The rows of the jump matrix of a rate matrix sum to 1.

theorem sum_ctmcJumpMatrix (hQ : IsRateMatrix Q) (i : ι) : ∑ j, ctmcJumpMatrix Q i j = 1
Uses 3 · Used by 7
Statement usesRate matrix · Jump matrix of a rate matrix
Proof usesDiagonal of a rate matrix is minus the total jump rate
Used byKolmogorov · Jump matrix is row-stochastic · Row of the jump matrix as a probability mass function · 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

TheoremJump matrix is row-stochastic#✓fully proved

The jump matrix of a rate matrix is row-stochastic.

theorem ctmcJumpMatrix_mem_rowStochastic (hQ : IsRateMatrix Q) :
    ctmcJumpMatrix Q ∈ Matrix.rowStochastic ℝ ι
Uses 4
Statement usesRate matrix · Jump matrix of a rate matrix
Proof usesNonnegativity of the jump matrix · Rows of the jump matrix sum to one

DefinitionRow of the jump matrix as a probability mass function#✓fully proved

Row i of the jump matrix of a rate matrix, as a probability mass function on ι.

noncomputable def ctmcJumpPMF (hQ : IsRateMatrix Q) (i : ι) : PMF ι :=
  PMF.ofFintype (fun j => ENNReal.ofReal (ctmcJumpMatrix Q i j)) (by
    rw [← ENNReal.ofReal_sum_of_nonneg fun j _ => hQ.ctmcJumpMatrix_nonneg i j,
      hQ.sum_ctmcJumpMatrix i, ENNReal.ofReal_one])
Uses 4 · Used by 12
Statement usesRate matrix · Nonnegativity of the jump matrix · Rows of the jump matrix sum to one · Jump matrix of a rate matrix
Used byNon-explosion · Strong Markov property at jump times · Restart law at a fixed time · Kolmogorov · Finite-dimensional distributions · Law of one step of the chain construction · 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

Probability Theory

DefinitionLaw of one step of the chain construction#✓fully proved

The law of one step (ξ, E) of the construction: ξ : ι → ι has independent coordinates with ξ i ∼ Π i, and E is an independent exponential clock of rate 1.

noncomputable def ctmcStepMeasure (hQ : IsRateMatrix Q) : Measure ((ι → ι) × ℝ) :=
  (Measure.pi fun i => (hQ.ctmcJumpPMF i).toMeasure).prod (expMeasure 1)
Uses 2 · Used by 12
Statement usesRate matrix · Row of the jump matrix as a probability mass function
Used byNon-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 · 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

DefinitionLaw of the driving step sequence of a Markov chain#✓fully proved

The law of the i.i.d. step sequence ω : ℕ → (ι → ι) × ℝ driving the chain.

noncomputable def ctmcInputMeasure (hQ : IsRateMatrix Q) : Measure (ℕ → (ι → ι) × ℝ) :=
  Measure.infinitePi fun _ => ctmcStepMeasure hQ
Uses 2 · Used by 17
Statement usesRate matrix · Law of one step of the chain construction
Used byCovariance of the coalescence times, path form · Mean coalescence time at locus A, path form · Product moment of the two coalescence times, path form · Mean coalescence time at locus B, path form · Non-explosion · Strong Markov property at jump times · Restart law at a fixed time · Kolmogorov · Finite-dimensional distributions · 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

DefinitionJump chain of a continuous-time Markov chain#✓fully proved

The jump chain started at i: Y 0 = i and Y (n + 1) = ξ n (Y n).

def ctmcJumpChain (i : ι) (ω : ℕ → (ι → ι) × ℝ) : ℕ → ι
  | 0 => i
  | n + 1 => (ω n).1 (ctmcJumpChain i ω n)
Used by 19
Used byNon-explosion · Holding times of a continuous-time Markov chain · Holding times of the shifted steps · Strong Markov property at jump times · Jump chain of the shifted steps · Additivity of jump times under shifting · Path of a continuous-time Markov chain · First-jump decomposition · Path value between consecutive jump times · Path restarts at a jump time · Measurability of the holding times · Measurability of the jump chain · Joint measurability of the chain path in time and steps · 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

DefinitionHolding times of a continuous-time Markov chain#✓fully proved

The n-th holding time S n = E n / q (Y n), where q k = -Q k k; it is ∞ when Y n is absorbing (q (Y n) = 0). Negative clock values, a null event, give S n = 0.

noncomputable def ctmcHoldingTime (Q : Matrix ι ι ℝ) (i : ι) (ω : ℕ → (ι → ι) × ℝ) (n : ℕ) :
    ℝ≥0∞ :=
  if Q (ctmcJumpChain i ω n) (ctmcJumpChain i ω n) = 0 then ∞
  else ENNReal.ofReal ((ω n).2 / -Q (ctmcJumpChain i ω n) (ctmcJumpChain i ω n))
Uses 1 · Used by 18
Statement usesJump chain of a continuous-time Markov chain
Used byNon-explosion · Holding times of the shifted steps · Restart law at a fixed time · Kolmogorov · Jump times of a continuous-time Markov chain · Additivity of jump times under shifting · Jump times are nondecreasing · First-jump decomposition · Measurability of the holding times · Measurability of the jump times · First-jump decomposition of a hitting time · Hitting time from inside the target set is zero · 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

DefinitionJump times of a continuous-time Markov chain#✓fully proved

The n-th jump time T n = S 0 + ⋯ + S (n - 1), with T 0 = 0.

noncomputable def ctmcJumpTime (Q : Matrix ι ι ℝ) (i : ι) (ω : ℕ → (ι → ι) × ℝ) (n : ℕ) :
    ℝ≥0∞ :=
  ∑ k ∈ range n, ctmcHoldingTime Q i ω k
Uses 1 · Used by 16
Statement usesHolding times of a continuous-time Markov chain
Used byNon-explosion · Strong Markov property at jump times · Additivity of jump times under shifting · Jump times are nondecreasing · Path of a continuous-time Markov chain · First-jump decomposition · Path value between consecutive jump times · Path restarts at a jump time · Measurability of the jump times · Joint measurability of the chain path in time and steps · 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

DefinitionPath of a continuous-time Markov chain#✓fully proved

The path of the chain started at i: X t = Y n for the n with T n ≤ t < T (n + 1). If t is at or after the explosion time sup T n (a null event, by IsRateMatrix.ae_tendsto_ctmcJumpTime), the value is an arbitrary state that does not depend on i, Q or ω.

noncomputable def ctmcPath (Q : Matrix ι ι ℝ) (i : ι) (ω : ℕ → (ι → ι) × ℝ) (t : ℝ≥0) : ι :=
  haveI : Nonempty ι := ⟨i⟩
  if h : ∃ n, (t : ℝ≥0∞) < ctmcJumpTime Q i ω (n + 1) then ctmcJumpChain i ω (Nat.find h)
  else Classical.ofNonempty
Uses 2 · Used by 16
Statement usesJump chain of a continuous-time Markov chain · Jump times of a continuous-time Markov chain
Used byCovariance of the coalescence times, path form · Mean coalescence time at locus A, path form · Product moment of the two coalescence times, path form · Mean coalescence time at locus B, path form · Strong Markov property at jump times · Restart law at a fixed time · Kolmogorov · Finite-dimensional distributions · First-jump decomposition · Path value between consecutive jump times · Path restarts at a jump time · Measurability of the chain state at a fixed time · Joint measurability of the chain path in time and steps · Hitting time of a continuous-time Markov chain · First-jump decomposition of a hitting time · Hitting time from inside the target set is zero

DefinitionShift of the step sequence of a Markov chain#✓fully proved

The shift of the step sequence by n: (shift n ω) m = ω (n + m).

def ctmcShift (n : ℕ) (ω : ℕ → (ι → ι) × ℝ) : ℕ → (ι → ι) × ℝ := fun m => ω (n + m)
Used by 16
Used byHolding times of the shifted steps · Strong Markov property at jump times · Restart law at a fixed time · Kolmogorov · Jump chain of the shifted steps · Additivity of jump times under shifting · First-jump decomposition · Path restarts at a jump time · First-jump decomposition of a hitting time · Hitting time from inside the target set is zero · 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

TheoremJump times are nondecreasing#✓fully proved

The jump times are nondecreasing.

theorem ctmcJumpTime_mono (i : ι) (ω : ℕ → (ι → ι) × ℝ) : Monotone (ctmcJumpTime Q i ω)
Uses 2 · Used by 8
Statement usesJump times of a continuous-time Markov chain
Proof usesHolding times of a continuous-time Markov chain
Used byPath value between consecutive jump times · Path restarts at a jump time · 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

TheoremPath value between consecutive jump times#✓fully proved

If T n ≤ t < T (n + 1), then X t = Y n.

theorem ctmcPath_eq_of_mem (i : ι) (ω : ℕ → (ι → ι) × ℝ) {t : ℝ≥0} {n : ℕ}
    (h₁ : ctmcJumpTime Q i ω n ≤ t) (h₂ : (t : ℝ≥0∞) < ctmcJumpTime Q i ω (n + 1)) :
    ctmcPath Q i ω t = ctmcJumpChain i ω n
Uses 4 · Used by 2
Statement usesJump chain of a continuous-time Markov chain · Jump times of a continuous-time Markov chain · Path of a continuous-time Markov chain
Proof usesJump times are nondecreasing
Used byFirst-jump decomposition · Joint measurability of the chain path in time and steps

TheoremJump chain of the shifted steps#✓fully proved

The jump chain of the shifted steps started at Y n is the jump chain after n.

theorem ctmcJumpChain_shift (i : ι) (ω : ℕ → (ι → ι) × ℝ) (n m : ℕ) :
    ctmcJumpChain (ctmcJumpChain i ω n) (ctmcShift n ω) m = ctmcJumpChain i ω (n + m)
Uses 2 · Used by 2
Statement usesJump chain of a continuous-time Markov chain · Shift of the step sequence of a Markov chain
Used byHolding times of the shifted steps · Path restarts at a jump time

TheoremHolding times of the shifted steps#✓fully proved

The holding times of the shifted steps started at Y n are the holding times after n.

theorem ctmcHoldingTime_shift (i : ι) (ω : ℕ → (ι → ι) × ℝ) (n m : ℕ) :
    ctmcHoldingTime Q (ctmcJumpChain i ω n) (ctmcShift n ω) m =
      ctmcHoldingTime Q i ω (n + m)
Uses 4 · Used by 1
Statement usesHolding times of a continuous-time Markov chain · Jump chain of a continuous-time Markov chain · Shift of the step sequence of a Markov chain
Proof usesJump chain of the shifted steps
Used byAdditivity of jump times under shifting

TheoremAdditivity of jump times under shifting#✓fully proved

T (n + m) = T n + T' m, where T' are the jump times of the shifted steps started at Y n.

theorem ctmcJumpTime_add (i : ι) (ω : ℕ → (ι → ι) × ℝ) (n m : ℕ) :
    ctmcJumpTime Q i ω (n + m) =
      ctmcJumpTime Q i ω n + ctmcJumpTime Q (ctmcJumpChain i ω n) (ctmcShift n ω) m
Uses 5 · Used by 7
Statement usesJump chain of a continuous-time Markov chain · Jump times of a continuous-time Markov chain · Shift of the step sequence of a Markov chain
Proof usesHolding times of a continuous-time Markov chain · Holding times of the shifted steps
Used byPath restarts at a jump time · 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

TheoremPath restarts at a jump time#✓fully proved

After a finite jump time T n, the path is the path started at Y n driven by the shifted steps: X (T n + s) = X' s with X' built from shift n ω started at Y n.

theorem ctmcPath_jumpTime_add (i : ι) (ω : ℕ → (ι → ι) × ℝ) (n : ℕ)
    (hn : ctmcJumpTime Q i ω n ≠ ∞) (s : ℝ≥0) :
    ctmcPath Q i ω ((ctmcJumpTime Q i ω n).toNNReal + s) =
      ctmcPath Q (ctmcJumpChain i ω n) (ctmcShift n ω) s
Uses 7 · Used by 2
Statement usesJump chain of a continuous-time Markov chain · Jump times of a continuous-time Markov chain · Path of a continuous-time Markov chain · Shift of the step sequence of a Markov chain
Proof usesJump chain of the shifted steps · Additivity of jump times under shifting · Jump times are nondecreasing
Used byStrong Markov property at jump times · First-jump decomposition

TheoremFirst-jump decomposition#✓fully proved

First-jump decomposition of the path: before the first holding time the chain is at i; afterwards it is the chain started at ξ 0 i driven by the shifted steps.

theorem ctmcPath_eq_ite (i : ι) (ω : ℕ → (ι → ι) × ℝ) (t : ℝ≥0) :
    ctmcPath Q i ω t = if (t : ℝ≥0∞) < ctmcHoldingTime Q i ω 0 then i
      else ctmcPath Q ((ω 0).1 i) (ctmcShift 1 ω) (t - (ctmcHoldingTime Q i ω 0).toNNReal)
Uses 7 · Used by 4
Statement usesHolding times of a continuous-time Markov chain · Path of a continuous-time Markov chain · Shift of the step sequence of a Markov chain
Proof usesJump chain of a continuous-time Markov chain · Jump times of a continuous-time Markov chain · Path value between consecutive jump times · Path restarts at a jump time
Used byRestart law at a fixed time · Kolmogorov · First-jump decomposition of a hitting time · Hitting time from inside the target set is zero

TheoremMeasurability of the jump chain#✓fully proved

The jump chain Y n is a measurable function of the steps.

theorem measurable_ctmcJumpChain (i : ι) (n : ℕ) :
    Measurable fun ω => ctmcJumpChain i ω n
Uses 1 · Used by 2
Statement usesJump chain of a continuous-time Markov chain
Used byMeasurability of the holding times · Joint measurability of the chain path in time and steps

TheoremMeasurability of the holding times#✓fully proved

The holding time S n is a measurable function of the steps.

theorem measurable_ctmcHoldingTime (i : ι) (n : ℕ) :
    Measurable fun ω => ctmcHoldingTime Q i ω n
Uses 3 · Used by 7
Statement usesHolding times of a continuous-time Markov chain
Proof usesJump chain of a continuous-time Markov chain · Measurability of the jump chain
Used byMeasurability of the jump 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

TheoremMeasurability of the jump times#✓fully proved

The jump time T n is a measurable function of the steps.

theorem measurable_ctmcJumpTime (i : ι) (n : ℕ) :
    Measurable fun ω => ctmcJumpTime Q i ω n
Uses 3 · Used by 1
Statement usesJump times of a continuous-time Markov chain
Proof usesHolding times of a continuous-time Markov chain · Measurability of the holding times
Used byJoint measurability of the chain path in time and steps

TheoremJoint measurability of the chain path in time and steps#✓fully proved

The path (t, ω) ↦ X t is jointly measurable in the time and the steps.

theorem measurable_ctmcPath_uncurry (i : ι) :
    Measurable fun p : ℝ≥0 × (ℕ → (ι → ι) × ℝ) => ctmcPath Q i p.2 p.1
Uses 6 · Used by 3
Statement usesPath of a continuous-time Markov chain
Proof usesJump chain of a continuous-time Markov chain · Jump times of a continuous-time Markov chain · Path value between consecutive jump times · Measurability of the jump chain · Measurability of the jump times
Used byRestart law at a fixed time · Kolmogorov · Measurability of the chain state at a fixed time

TheoremMeasurability of the chain state at a fixed time#✓fully proved

The state X t is a measurable function of the steps.

theorem measurable_ctmcPath (i : ι) (t : ℝ≥0) : Measurable fun ω => ctmcPath Q i ω t
Uses 2 · Used by 2
Statement usesPath of a continuous-time Markov chain
Proof usesJoint measurability of the chain path in time and steps
Used byStrong Markov property at jump times · Restart law at a fixed time

Is Rate Matrix

TheoremNon-explosion#✓fully proved

Non-explosion (Norris 1997, §2.7, for a finite state space): almost surely the jump times of the chain started at i tend to ∞, so X t is a genuine state of the jump chain for every t ≥ 0.

theorem ae_tendsto_ctmcJumpTime (hQ : IsRateMatrix Q) (i : ι) :
    ∀ᵐ ω ∂ctmcInputMeasure hQ, Tendsto (ctmcJumpTime Q i ω) atTop (𝓝 ∞)
Uses 10 · Used by 6
Statement usesRate matrix · Law of the driving step sequence of a Markov chain · Jump times of a continuous-time Markov chain
Proof usesRow of the jump matrix as a probability mass function · Diagonal entries of a rate matrix are nonpositive · Holding times of a continuous-time Markov chain · Jump chain of a continuous-time Markov chain · Law of one step of the chain construction · Integrability of the identity under the exponential law · Mean of the exponential law
Used byMean 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

TheoremStrong Markov property at jump times#✓fully proved

Strong Markov property at jump times (Norris 1997, §2.6–2.7): let A be a measurable set of histories of the first n steps such that T n < ∞ whenever the history lies in A; these histories determine Y 0, …, Y n and S 0, …, S (n - 1). Then for every state k and every measurable set B of paths, the path after T n is independent of the event {history ∈ A, Y n = k} and distributed as the chain started at k.

theorem ctmcInputMeasure_ctmcPath_jumpTime_add (hQ : IsRateMatrix Q) (i : ι) (n : ℕ)
    {A : Set (Fin n → (ι → ι) × ℝ)} (hA : MeasurableSet A)
    (hAT : ∀ ω : ℕ → (ι → ι) × ℝ, (fun k : Fin n => ω k) ∈ A → ctmcJumpTime Q i ω n ≠ ∞)
    (k : ι) {B : Set (ℝ≥0 → ι)} (hB : MeasurableSet B) :
    ctmcInputMeasure hQ
        ({ω | (fun k : Fin n => ω k) ∈ A} ∩ {ω | ctmcJumpChain i ω n = k} ∩
          {ω | (fun s => ctmcPath Q i ω ((ctmcJumpTime Q i ω n).toNNReal + s)) ∈ B}) =
      ctmcInputMeasure hQ
          ({ω | (fun k : Fin n => ω k) ∈ A} ∩ {ω | ctmcJumpChain i ω n = k}) *
        ctmcInputMeasure hQ {ω | (fun s => ctmcPath Q k ω s) ∈ B}
Uses 10
Statement usesRate matrix · Law of the driving step sequence of a Markov chain · Jump chain of a continuous-time Markov chain · Jump times of a continuous-time Markov chain · Path of a continuous-time Markov chain
Proof usesRow of the jump matrix as a probability mass function · Path restarts at a jump time · Shift of the step sequence of a Markov chain · Law of one step of the chain construction · Measurability of the chain state at a fixed time

TheoremKolmogorov#✓fully proved

Kolmogorov (Norris 1997, §2.8, Theorem 2.8.2 for a finite state space): the chain built from the jump chain and the holding times has transition function exp (t • Q): P_i(X t = j) = exp (t Q) i j for every t ≥ 0.

theorem ctmcInputMeasure_real_ctmcPath_eq (hQ : IsRateMatrix Q) (i j : ι) (t : ℝ≥0) :
    (ctmcInputMeasure hQ).real {ω | ctmcPath Q i ω t = j} = ctmcTransition Q t i j
Uses 20 · Used by 1
Statement usesRate matrix · Law of the driving step sequence of a Markov chain · Path of a continuous-time Markov chain · Transition semigroup of a continuous-time Markov chain
Proof usesNonnegativity of the jump matrix · Row of the jump matrix as a probability mass function · Nonnegativity of the transition function of a rate matrix · Diagonal entries of a rate matrix are nonpositive · Rows of the jump matrix sum to one · Rows of the transition function sum to one · Holding times of a continuous-time Markov chain · Jump matrix of a rate matrix · First-jump decomposition · Shift of the step sequence of a Markov chain · Law of one step of the chain construction · Transition function at time zero is the identity · Kolmogorov backward equation · Integrability criterion for the exponential law · Integrals against the exponential law · Joint measurability of the chain path in time and steps
Used byRestart law at a fixed time

TheoremRestart law at a fixed time#✓fully proved

Restart law at a fixed time (cf. the Markov property, Norris 1997, §2.8), for events of X s and of the path after s only: for the chain started at i, the probability that X s = k and that the path after s lies in a measurable set B is exp (s Q) i k times the probability that the chain started at k lies in B. This is weaker than the Markov property with respect to the natural filtration: arbitrary events of the path before s are not covered (only through the finite-dimensional distributions, ctmcInputMeasure_real_ctmcPath_fdd).

theorem ctmcInputMeasure_real_ctmcPath_add (hQ : IsRateMatrix Q) (i k : ι) (s : ℝ≥0)
    {B : Set (ℝ≥0 → ι)} (hB : MeasurableSet B) :
    (ctmcInputMeasure hQ).real
        {ω | ctmcPath Q i ω s = k ∧ (fun u => ctmcPath Q i ω (s + u)) ∈ B} =
      ctmcTransition Q s i k *
        (ctmcInputMeasure hQ).real {ω | (fun u => ctmcPath Q k ω u) ∈ B}
Uses 14 · Used by 1
Statement usesRate matrix · Law of the driving step sequence of a Markov chain · Path of a continuous-time Markov chain · Transition semigroup of a continuous-time Markov chain
Proof usesKolmogorov · Row of the jump matrix as a probability mass function · Diagonal entries of a rate matrix are nonpositive · Holding times of a continuous-time Markov chain · First-jump decomposition · Shift of the step sequence of a Markov chain · Law of one step of the chain construction · Integrals against the exponential law · Measurability of the chain state at a fixed time · Joint measurability of the chain path in time and steps
Used byFinite-dimensional distributions

TheoremFinite-dimensional distributions#✓fully proved

Finite-dimensional distributions (Norris 1997, §2.8, Theorem 2.8.2 (c)): with increments s 0, …, s (n - 1) ≥ 0, times t k = s 0 + ⋯ + s k, and states j 0, …, j (n - 1), P_i(X (t k) = j k for all k) = ∏ₖ exp (s k Q) (j (k - 1)) (j k), where j (-1) = i.

theorem ctmcInputMeasure_real_ctmcPath_fdd (hQ : IsRateMatrix Q) (i : ι) {n : ℕ}
    (s : Fin n → ℝ≥0) (j : Fin n → ι) :
    (ctmcInputMeasure hQ).real {ω | ∀ k, ctmcPath Q i ω (∑ l ∈ Iic k, s l) = j k} =
      ∏ k, ctmcTransition Q (s k) ((Fin.cons i j : Fin (n + 1) → ι) k.castSucc) (j k)
Uses 7
Statement usesRate matrix · Law of the driving step sequence of a Markov chain · Path of a continuous-time Markov chain · Transition semigroup of a continuous-time Markov chain
Proof usesRestart law at a fixed time · Row of the jump matrix as a probability mass function · Law of one step of the chain construction

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.