Hitting times of finite continuous-time Markov chains

11 fully proved

Probability Theory

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

The hitting time inf {t ≥ 0 | X t ∈ A} of a set of states A by the chain X = ctmcPath Q i ω started at i, valued in ℝ≥0∞ (it is ∞ if A is never visited).

noncomputable def ctmcHittingTime (Q : Matrix ι ι ℝ) (i : ι) (A : Set ι)
    (ω : ℕ → (ι → ι) × ℝ) : ℝ≥0∞ :=
  ⨅ (t : ℝ≥0) (_ : ctmcPath Q i ω t ∈ A), (t : ℝ≥0∞)

Uses 1 · Used by 13

Statement usesPath of a continuous-time Markov chain

Used byMean coalescence time at locus A, path form · Product moment of the two coalescence times, path form · Mean coalescence time at locus B, path form · Backward equations for the mean hitting time · First-jump decomposition of a hitting time · Hitting time from inside the target set is zero · 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

TheoremFirst-jump decomposition of a hitting time#✓fully proved

From a state i ∉ A, the hitting time of A is the first holding time plus the hitting time of the chain restarted after the first jump.

theorem ctmcHittingTime_eq_add {A : Set ι} {i : ι} (hi : i ∉ A) (ω : ℕ → (ι → ι) × ℝ) :
    ctmcHittingTime Q i A ω =
      ctmcHoldingTime Q i ω 0 + ctmcHittingTime Q ((ω 0).1 i) A (ctmcShift 1 ω)

Uses 5 · Used by 6

Statement usesHitting time of a continuous-time Markov chain · Holding times of a continuous-time Markov chain · Shift of the step sequence of a Markov chain

Proof usesPath of a continuous-time Markov chain · First-jump decomposition

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

TheoremHitting time from inside the target set is zero#✓fully proved

From a state i ∈ A, the hitting time of A is 0 as soon as the first holding time is positive (which fails only on a null event, see ctmcHoldingTime).

theorem ctmcHittingTime_eq_zero {A : Set ι} {i : ι} (hi : i ∈ A) {ω : ℕ → (ι → ι) × ℝ}
    (hS : 0 < ctmcHoldingTime Q i ω 0) : ctmcHittingTime Q i A ω = 0

Uses 5 · Used by 6

Statement usesHitting time of a continuous-time Markov chain · Holding times of a continuous-time Markov chain

Proof usesPath of a continuous-time Markov chain · First-jump decomposition · Shift of the step sequence of a Markov chain

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

Is Rate Matrix

TheoremMean hitting time, first-step equation#✓fully proved

Mean hitting time, first-step equation (compare Norris 1997, §3.3): from i ∉ A with q i = -Q i i ≠ 0, E_i H_A = 1 / q i + ∑ⱼ Π i j E_j H_A in ℝ≥0∞.

theorem lintegral_ctmcHittingTime (hQ : IsRateMatrix Q) {A : Set ι} {i : ι} (hi : i ∉ A)
    (hq : Q i i ≠ 0) :
    ∫⁻ ω, ctmcHittingTime Q i A ω ∂ctmcInputMeasure hQ =
      ENNReal.ofReal (1 / -Q i i) + ∑ j, ENNReal.ofReal (ctmcJumpMatrix Q i j) *
        ∫⁻ ω, ctmcHittingTime Q j A ω ∂ctmcInputMeasure hQ

Uses 21 · Used by 2

Statement usesRate matrix · Hitting time of a continuous-time Markov chain · Law of the driving step sequence of a Markov chain · Jump matrix of a rate matrix

Proof usesNon-explosion · Nonnegativity of the jump matrix · Row of the jump matrix as a probability mass function · Diagonal entries of a rate matrix are nonpositive · Rows of the jump matrix sum to one · First-jump decomposition of a hitting time · Hitting time from inside the target set is zero · Holding times of a continuous-time Markov chain · Jump chain of a continuous-time Markov chain · Jump times of a continuous-time Markov chain · Additivity of jump times under shifting · Jump times are nondecreasing · Shift of the step sequence of a Markov chain · Law of one step of the chain construction · Integrability of the identity under the exponential law · Mean of the exponential law · Measurability of the holding times

Used byBackward equations for the mean hitting time · Product moment of two hitting times, first-step equation

TheoremMean hitting time from inside the target set is zero#✓fully proved

From a state of A, the mean hitting time of A is 0.

theorem lintegral_ctmcHittingTime_of_mem (hQ : IsRateMatrix Q) {A : Set ι} {i : ι}
    (hi : i ∈ A) : ∫⁻ ω, ctmcHittingTime Q i A ω ∂ctmcInputMeasure hQ = 0

Uses 16 · Used by 1

Statement usesRate matrix · Hitting time of a continuous-time Markov chain · Law of the driving step sequence of a Markov chain

Proof usesNon-explosion · Row of the jump matrix as a probability mass function · Diagonal entries of a rate matrix are nonpositive · First-jump decomposition of a hitting time · Hitting time from inside the target set is zero · Holding times of a continuous-time Markov chain · Jump chain of a continuous-time Markov chain · Jump times of a continuous-time Markov chain · Additivity of jump times under shifting · Jump times are nondecreasing · Shift of the step sequence of a Markov chain · Law of one step of the chain construction · Measurability of the holding times

Used byBackward equations for the mean hitting time

TheoremMinimality of the mean hitting time#✓fully proved

Minimality of the mean hitting time (compare Norris 1997, §3.3): if every state off A has a positive exit rate, every m : ι → ℝ≥0∞ with 1 / q i + ∑ⱼ Π i j m j ≤ m i off A dominates E_i H_A.

theorem lintegral_ctmcHittingTime_le (hQ : IsRateMatrix Q) {A : Set ι}
    (hq : ∀ i ∉ A, Q i i ≠ 0) {m : ι → ℝ≥0∞}
    (hm : ∀ i ∉ A, ENNReal.ofReal (1 / -Q i i) + ∑ j, ENNReal.ofReal (ctmcJumpMatrix Q i j) * m j
      ≤ m i) (i : ι) :
    ∫⁻ ω, ctmcHittingTime Q i A ω ∂ctmcInputMeasure hQ ≤ m i

Uses 21 · Used by 2

Statement usesRate matrix · Hitting time of a continuous-time Markov chain · Law of the driving step sequence of a Markov chain · Jump matrix of a rate matrix

Proof usesNon-explosion · Nonnegativity of the jump matrix · Row of the jump matrix as a probability mass function · Diagonal entries of a rate matrix are nonpositive · Rows of the jump matrix sum to one · First-jump decomposition of a hitting time · Hitting time from inside the target set is zero · Holding times of a continuous-time Markov chain · Jump chain of a continuous-time Markov chain · Jump times of a continuous-time Markov chain · Additivity of jump times under shifting · Jump times are nondecreasing · Shift of the step sequence of a Markov chain · Law of one step of the chain construction · Integrability of the identity under the exponential law · Mean of the exponential law · Measurability of the holding times

Used byBackward equations for the mean hitting time · Backward equations for the product moment of two hitting times

TheoremProduct moment of two hitting times, first-step equation#✓fully proved

From i ∉ A ∪ B with q i ≠ 0, E_i (H_A H_B) = (E_i H_A + E_i H_B) / q i + ∑ⱼ Π i j E_j (H_A H_B) in ℝ≥0∞.

theorem lintegral_ctmcHittingTime_mul (hQ : IsRateMatrix Q) {A B : Set ι} {i : ι}
    (hi : i ∉ A ∪ B) (hq : Q i i ≠ 0) :
    ∫⁻ ω, ctmcHittingTime Q i A ω * ctmcHittingTime Q i B ω ∂ctmcInputMeasure hQ =
      ENNReal.ofReal (1 / -Q i i) *
          (∫⁻ ω, ctmcHittingTime Q i A ω ∂ctmcInputMeasure hQ +
            ∫⁻ ω, ctmcHittingTime Q i B ω ∂ctmcInputMeasure hQ) +
        ∑ j, ENNReal.ofReal (ctmcJumpMatrix Q i j) *
          ∫⁻ ω, ctmcHittingTime Q j A ω * ctmcHittingTime Q j B ω ∂ctmcInputMeasure hQ

Uses 24 · Used by 1

Statement usesRate matrix · Hitting time of a continuous-time Markov chain · Law of the driving step sequence of a Markov chain · Jump matrix of a rate matrix

Proof usesNon-explosion · Nonnegativity of the jump matrix · Row of the jump matrix as a probability mass function · Diagonal entries of a rate matrix are nonpositive · Mean hitting time, first-step equation · Rows of the jump matrix sum to one · First-jump decomposition of a hitting time · Hitting time from inside the target set is zero · Holding times of a continuous-time Markov chain · Jump chain of a continuous-time Markov chain · Jump times of a continuous-time Markov chain · Additivity of jump times under shifting · Jump times are nondecreasing · Shift of the step sequence of a Markov chain · Law of one step of the chain construction · Integrability of the identity under the exponential law · Finiteness of all moments of the exponential law · Mean of the exponential law · Second moment of the exponential law · Measurability of the holding times

Used byBackward equations for the product moment of two hitting times

TheoremProduct moment of hitting times from inside their union is zero#✓fully proved

From a state of A ∪ B, the product moment of the hitting times of A and B is 0.

theorem lintegral_ctmcHittingTime_mul_of_mem (hQ : IsRateMatrix Q) {A B : Set ι} {i : ι}
    (hi : i ∈ A ∪ B) :
    ∫⁻ ω, ctmcHittingTime Q i A ω * ctmcHittingTime Q i B ω ∂ctmcInputMeasure hQ = 0

Uses 16 · Used by 1

Statement usesRate matrix · Hitting time of a continuous-time Markov chain · Law of the driving step sequence of a Markov chain

Proof usesNon-explosion · Row of the jump matrix as a probability mass function · Diagonal entries of a rate matrix are nonpositive · First-jump decomposition of a hitting time · Hitting time from inside the target set is zero · Holding times of a continuous-time Markov chain · Jump chain of a continuous-time Markov chain · Jump times of a continuous-time Markov chain · Additivity of jump times under shifting · Jump times are nondecreasing · Shift of the step sequence of a Markov chain · Law of one step of the chain construction · Measurability of the holding times

Used byBackward equations for the product moment of two hitting times

TheoremMinimality of the product moment#✓fully proved

If mA, mB are supersolutions of the mean equations of A and B (as in lintegral_ctmcHittingTime_le) and F satisfies (mA i + mB i) / q i + ∑ⱼ Π i j F j ≤ F i off A ∪ B, then F dominates E_i (H_A H_B).

theorem lintegral_ctmcHittingTime_mul_le (hQ : IsRateMatrix Q) {A B : Set ι}
    (hqA : ∀ i ∉ A, Q i i ≠ 0) (hqB : ∀ i ∉ B, Q i i ≠ 0) {mA mB F : ι → ℝ≥0∞}
    (hmA : ∀ i ∉ A, ENNReal.ofReal (1 / -Q i i) +
      ∑ j, ENNReal.ofReal (ctmcJumpMatrix Q i j) * mA j ≤ mA i)
    (hmB : ∀ i ∉ B, ENNReal.ofReal (1 / -Q i i) +
      ∑ j, ENNReal.ofReal (ctmcJumpMatrix Q i j) * mB j ≤ mB i)
    (hF : ∀ i ∉ A ∪ B, ENNReal.ofReal (1 / -Q i i) * (mA i + mB i) +
      ∑ j, ENNReal.ofReal (ctmcJumpMatrix Q i j) * F j ≤ F i) (i : ι) :
    ∫⁻ ω, ctmcHittingTime Q i A ω * ctmcHittingTime Q i B ω ∂ctmcInputMeasure hQ ≤ F i

Uses 23 · Used by 1

Statement usesRate matrix · Hitting time of a continuous-time Markov chain · Law of the driving step sequence of a Markov chain · Jump matrix of a rate matrix

Proof usesNon-explosion · Nonnegativity of the jump matrix · Row of the jump matrix as a probability mass function · Diagonal entries of a rate matrix are nonpositive · Rows of the jump matrix sum to one · First-jump decomposition of a hitting time · Hitting time from inside the target set is zero · Holding times of a continuous-time Markov chain · Jump chain of a continuous-time Markov chain · Jump times of a continuous-time Markov chain · Additivity of jump times under shifting · Jump times are nondecreasing · Shift of the step sequence of a Markov chain · Law of one step of the chain construction · Integrability of the identity under the exponential law · Finiteness of all moments of the exponential law · Mean of the exponential law · Second moment of the exponential law · Measurability of the holding times

Used byBackward equations for the product moment of two hitting times

TheoremBackward equations for the mean hitting time#✓fully proved

Backward equations for the mean hitting time (compare Norris 1997, §3.3): if m : ι → ℝ is nonnegative and (Q m) i = -1 for i ∉ A, then E_i H_A ≤ m i (so it is finite), E_i H_A = 0 on A, and the real vector E_i H_A solves the same backward equations. With uniqueness of the solution, this identifies E_i H_A.

theorem ctmcHittingTime_backward (hQ : IsRateMatrix Q) {A : Set ι} {m : ι → ℝ}
    (hm0 : ∀ i, 0 ≤ m i) (hm : ∀ i ∉ A, (Q *ᵥ m) i = -1) :
    (∀ i, ∫⁻ ω, ctmcHittingTime Q i A ω ∂ctmcInputMeasure hQ ≤ ENNReal.ofReal (m i)) ∧
      (∀ i ∈ A, (∫⁻ ω, ctmcHittingTime Q i A ω ∂ctmcInputMeasure hQ).toReal = 0) ∧
      ∀ i ∉ A, (Q *ᵥ fun j => (∫⁻ ω, ctmcHittingTime Q j A ω ∂ctmcInputMeasure hQ).toReal) i =
        -1

Uses 10 · Used by 3

Statement usesRate matrix · Hitting time of a continuous-time Markov chain · Law of the driving step sequence of a Markov chain

Proof usesNonnegativity of the jump matrix · Diagonal of a rate matrix is minus the total jump rate · Diagonal entries of a rate matrix are nonpositive · Mean hitting time, first-step equation · Minimality of the mean hitting time · Mean hitting time from inside the target set is zero · Jump matrix of a rate matrix

Used byMean coalescence time at locus A, path form · Product moment of the two coalescence times, path form · Mean coalescence time at locus B, path form

TheoremBackward equations for the product moment of two hitting times#✓fully proved

Let mA, mB, f be nonnegative with (Q mA) i = -1 off A, (Q mB) i = -1 off B and (Q f) i = -(mA i + mB i) off A ∪ B. Then E_i (H_A H_B) ≤ f i (so it is finite), it is 0 on A ∪ B, and its real part p solves (Q p) i = -(E_i H_A + E_i H_B) off A ∪ B.

theorem ctmcHittingTime_mul_backward (hQ : IsRateMatrix Q) {A B : Set ι} {mA mB f : ι → ℝ}
    (hmA0 : ∀ i, 0 ≤ mA i) (hmB0 : ∀ i, 0 ≤ mB i) (hf0 : ∀ i, 0 ≤ f i)
    (hmA : ∀ i ∉ A, (Q *ᵥ mA) i = -1) (hmB : ∀ i ∉ B, (Q *ᵥ mB) i = -1)
    (hf : ∀ i ∉ A ∪ B, (Q *ᵥ f) i = -(mA i + mB i)) :
    (∀ i, ∫⁻ ω, ctmcHittingTime Q i A ω * ctmcHittingTime Q i B ω ∂ctmcInputMeasure hQ ≤
        ENNReal.ofReal (f i)) ∧
      (∀ i ∈ A ∪ B, (∫⁻ ω, ctmcHittingTime Q i A ω * ctmcHittingTime Q i B ω
        ∂ctmcInputMeasure hQ).toReal = 0) ∧
      ∀ i ∉ A ∪ B, (Q *ᵥ fun j => (∫⁻ ω, ctmcHittingTime Q j A ω * ctmcHittingTime Q j B ω
        ∂ctmcInputMeasure hQ).toReal) i =
        -((∫⁻ ω, ctmcHittingTime Q i A ω ∂ctmcInputMeasure hQ).toReal +
          (∫⁻ ω, ctmcHittingTime Q i B ω ∂ctmcInputMeasure hQ).toReal)

Uses 11 · Used by 1

Statement usesRate matrix · Hitting time of a continuous-time Markov chain · Law of the driving step sequence of a Markov chain

Proof usesNonnegativity of the jump matrix · Diagonal of a rate matrix is minus the total jump rate · Diagonal entries of a rate matrix are nonpositive · 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 · Jump matrix of a rate matrix

Used byProduct moment of the two coalescence times, path form

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.