TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Transient hitting, mean exit, and residual bounds

Statement

Let $K$ be a finite row-stochastic transition matrix on a finite state set, let $U$ be a nonempty subset, and put $T = K_{U, U}$ . Suppose $T$ satisfies the escape hypothesis of Finite-step escape from a transient substochastic block with constants $L \leq ∣ U ∣$ and $ε > 0$ . For each $i \in U$ , give a finite first-exit path $(i = i_{0}, i_{1}, \dots, i_{k}, j)$ , with $i_{0}, \dots, i_{k} \in U$ and $j \in U^{c}$ , the weight $\prod_{r < k} K_{i_{r} i_{r + 1}} K_{i_{k} j}$ . The proof shows these countably many path weights sum to one, so they define a probability distribution on finite first-exit paths. Let $G \subseteq U^{c}$ , set $b_{i} = \sum_{j \in G} K_{i j}$ , and let $h_{i}$ be the probability that the path exits into $G$ ; let $t_{i}$ be the mean number of transitions to exit. Then $h = \sum_{k \geq 0} T^{k} b$ and $t = \sum_{k \geq 0} T^{k} 1$ . The matrix $N = (I - T)^{- 1} = \sum_{k = 0}^{\infty} T^{k}$ exists, has nonnegative entries, and

$∥ N ∥_{\infty} \leq L / ε, ∥ h - \hat{h} ∥_{\infty} \leq (L / ε) ∥ b - (I - T) \hat{h} ∥_{\infty},$

where $h_{i}$ is the probability that the first exit from $U$ lands in $G$ and $h = N b$ . The expected number $t_{i}$ of steps until the first exit from $U$ is finite and satisfies $t = N 1$ ; for any $\hat{t}$ ,

$∥ t - \hat{t} ∥_{\infty} \leq (L / ε) ∥ 1 - (I - T) \hat{t} ∥_{\infty} .$

Thus these hitting and mean-exit systems are certified only for a proved transient block; a row-substochastic matrix without the escape hypothesis receives no such conclusion here. The matrix norm is $∥ A ∥_{\infty} = \max_{i} \sum_{j} ∣ A_{i j} ∣$ and the vector norm is $∥ v ∥_{\infty} = \max_{i} ∣ v_{i} ∣$ .

Facts & Assumptions

Given: A finite row-stochastic transition matrix $K$ , a nonempty transient set $U$ , its block $T = K_{U, U}$ , the escape constants $L, ε$ , and a boundary target $G \subseteq U^{c}$ .

[F1]

Transition matrices and n-step probabilities: the entries of $K$ are nonnegative and each source row sums to one.

[F2]

Finite-step escape from a transient substochastic block: $T \geq 0$ , $T 1 \leq 1$ , and $T^{L} 1 \leq (1 - ε) 1$ for some $L \leq ∣ U ∣$ and $ε > 0$ ; in particular $T^{n} 1 \to 0$ .

[L1]

The finite first-exit paths from $i$ have weights $\prod_{r < k} K_{i_{r} i_{r + 1}} K_{i_{k} j}$ ; once their total weight is one, their event probabilities and the mean exit length are the corresponding nonnegative sums.

Proof

Given: $K, U, T, G, L, ε$ and the finite first-exit path weights above.

Proof technique: group the Neumann series into blocks of length $L$ , normalize the finite first-exit path weights, and use the tail-sum identity for an integer-valued exit length.

1.1givenF2algebrainduction

For $0 \leq r < L$ , substochasticity gives $T^{r} 1 \leq 1$ . Since $T^{L} 1 \leq (1 - ε) 1$ , induction gives $(T^{L})^{q} 1 \leq (1 - ε)^{q} 1$ for every $q \geq 0$ . Therefore every row sum of $T^{q L + r}$ is at most $(1 - ε)^{q}$ , and $\sum_{k \geq 0} ∥ T^{k} ∥_{\infty} \leq L \sum_{q \geq 0} (1 - ε)^{q} = L / ε$ .

2.1step 1.1algebra

The series $N = \sum_{k \geq 0} T^{k}$ converges in the maximum-row-sum norm and has nonnegative entries. The finite partial sums satisfy $(I - T) \sum_{k = 0}^{m} T^{k} = I - T^{m + 1}$ and $\sum_{k = 0}^{m} T^{k} (I - T) = I - T^{m + 1}$ . Step 1.1 makes $T^{m + 1} \to 0$ , so $N$ is a two-sided inverse of $I - T$ and $∥ N ∥_{\infty} \leq L / ε$ .

2.2F1F2L1step 1.1algebra

Put $d = 1 - T 1$ , the vector of one-step exit weights from rows of $U$ . For each $i$ , the total weight of first-exit paths of length at most $N$ is $\sum_{k = 0}^{N - 1} (T^{k} d)_{i} = \sum_{k = 0}^{N - 1} (T^{k} 1 - T^{k + 1} 1)_{i} = 1 - (T^{N} 1)_{i}$ . By [F2], this tends to one. The finite-exit path set is countable, so these nonnegative weights define a probability distribution. For paths exiting into $G$ after $k$ transitions within $U$ , finite matrix multiplication gives weight $(T^{k} b)_{i}$ ; summing over $k$ yields $h_{i} = \sum_{k \geq 0} (T^{k} b)_{i} = (N b)_{i}$ .

3.1F1F2L1step 1.1step 2.2algebra

For a path with exit length $τ$ , the indicator identity $τ = \sum_{k \geq 0} 1_{{τ > k}}$ holds. Summing against the countable path probability from step 2.2 gives $E_{i} τ = \sum_{k \geq 0} \Pr_{i} (τ > k)$ , since both are the same nonnegative double sum indexed by pairs $0 \leq k < τ$ . The total weight of paths still in $U$ after $k$ transitions is $(T^{k} 1)_{i}$ , so $t_{i} = \sum_{k \geq 0} (T^{k} 1)_{i} = (N 1)_{i}$ . Step 1.1 makes this finite, and multiplying by $I - T$ gives $(I - T) t = 1$ .

4.1step 2.1step 2.2step 3.1algebra∎

From $h - \hat{h} = N (b - (I - T) \hat{h})$ , the operator norm bound in step 2.1 gives the stated hitting-probability residual bound. Applying the same identity to $t - \hat{t}$ with right side $1$ gives the mean-exit residual bound.

Depends on

Used by

Dependency tree · two levels

4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Charles M. Grinstead and J. Laurie Snell, Introduction to Probability, Chapter 11 (standard reference, not scraped)