TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Lyapunov drift bound for hitting times

Statement

Assume AC (The Axiom of Choice). Let $E$ be at most countable with sigma-algebra $2^{E}$ , let $K$ be a probability kernel, and set $p (x, y) = K (x, {y})$ . For each $x \in E$ , let $P_{x}$ be the canonical path-space chain law with initial measure $δ_{x}$ and transition kernel $K$ , and let $E_{x}$ be its expectation. For $A \subseteq E$ , define $T_{A} = \inf {n \geq 0 : X_{n} \in A}$ . If $ψ : E \to [0, \infty)$ is finite-valued with $P ψ (x) < \infty$ for every $x$ and $L ψ (x) \leq - 1$ on $E ∖ A$ , using the support-restricted kernel action and finite drift, then $E_{x} [T_{A}] \leq ψ (x)$ for every $x$ . Consequently $P_{x} (T_{A} < \infty) = 1$ .

Facts & Assumptions

Given: AC, an at most countable state space $E$ , a probability kernel $K$ with transition matrix $p$ , a target $A \subseteq E$ , and a finite-valued nonnegative $ψ$ satisfying $P ψ < \infty$ everywhere and $L ψ \leq - 1$ on $A^{c}$ .

[A1]

AC is the assumption available to construct each fixed-start canonical law and is assumed by the prior first-step and superharmonic-majorant theorems. (The Axiom of Choice)

[F1]

An at most countable set is finite or countably infinite. (Finite, countably infinite, countable, uncountable)

[F2]

A probability kernel is a probability measure in the target variable and has total mass one. (Measure kernel and probability kernel)

[F3]

For $x \in E$ , the Dirac set function $δ_{x}$ is a probability measure. (A Dirac set function is a probability measure)

[F4]

AC gives the canonical path-space law for a probability initial measure and a probability kernel; its coordinate process is the corresponding Markov chain. (Canonical Markov chain on path space)

[F5]

With initial state fixed at $x$ , write $P_{x}$ for the law with initial distribution $δ_{x}$ and $E_{x}$ for its expectation. (Initial distribution of a Markov chain)

[F6]

$T_{A} = \inf {n \geq 0 : X_{n} \in A}$ , the infimum of the empty set is $+ \infty$ , and $T_{A} = 0$ when the start is in $A$ . (Hitting, return, and visit times)

[F7]

The transition matrix is $p (x, y) = K (x, {y})$ . (Transition matrices and n-step probabilities)

[F8]

For finite-valued $ψ$ , $P ψ (x) = \sum_{y : p (x, y) > 0} p (x, y) ψ (y)$ ; when this is finite, $L ψ (x) = P ψ (x) - ψ (x)$ . Zero transition weights are omitted. (Nonnegative kernel action and finite drift)

[F9]

For bounded nonnegative boundary payoff $f$ and running cost $c$ , the first-step exit cost is $u (x) = E_{x} [B + \sum_{0 \leq m < T} c (X_{m})]$ , where $B = f (X_{T})$ on $T < \infty$ and $B = 0$ on $T = \infty$ . (First-step equations for nonnegative exit costs)

[F10]

If $D \subseteq E$ , $f : D^{c} \to [0, \infty)$ and $c : D \to [0, \infty)$ are bounded, and finite-valued $ψ \geq 0$ satisfies $P ψ < \infty$ everywhere, $ψ \geq f$ on $D^{c}$ , and $L ψ \leq - c$ on $D$ , then the corresponding exit cost obeys $u (x) \leq ψ (x)$ . (Superharmonic majorants bound exit costs)

[F11]

Expectation of a nonnegative measurable random variable is its extended nonnegative integral, and the nonnegative integral preserves pointwise order. (Expectation of a nonnegative or integrable random variable, Monotonicity and nonnegative homogeneity of the nonnegative integral)

Proof

technique · identify $T_A$ with the unit running cost up to first exit from $A^c$, then apply the superharmonic-majorant bound

1.1A1F2F3F4F5given

Fix $x \in E$ . By [F2] and [F3], $K$ and $δ_{x}$ satisfy the kernel and initial-measure hypotheses of [F4]; AC [A1] therefore supplies the canonical law $P_{x}$ , and [F5] fixes the notation $E_{x}$ . This is done for each $x$ separately, without selecting path-space realizations as a family.

1.2F6given

Pathwise, if $T_{A} = k < \infty$ then exactly the indices $m = 0, \dots, k - 1$ satisfy $m < T_{A}$ , while if $T_{A} = \infty$ every $m \geq 0$ does; hence $\sum_{m \geq 0} 1_{{m < T_{A}}} = T_{A}$ in $[0, + \infty]$ . In particular the sum is empty and equals zero when the starting state is in $A$ .

1.3F1F2F7F8given

Set $D = A^{c}$ , let $f$ be the zero function on $A = D^{c}$ , and let $c$ be the constant one function on $D$ . Both are bounded and nonnegative, $ψ \geq f$ on $A$ , and [F8] identifies the given drift condition with $L ψ \leq - c$ on $D$ . Countability and the matrix-kernel relationship are [F1], [F2], and [F7].

2.1F6F9step 1.2step 1.3given

For the exit problem in step 1.3, the boundary payoff is zero on both $T_{A} < \infty$ and $T_{A} = \infty$ , and the accumulated running cost is $\sum_{m < T_{A}} 1$ . By [F9] and the pathwise identity in step 1.2, its value is $u (x) = E_{x} [T_{A}]$ , including the value $+ \infty$ if the target is never hit.

3.1A1F1F8F10step 1.3step 2.1given

The hypotheses of [F10] hold for $D = A^{c}$ , $f = 0$ , and $c = 1$ : the chain is countable by [F1], AC [A1] is assumed, step 1.3 verifies the boundary and drift inequalities, and $P ψ$ is finite everywhere by hypothesis. Therefore step 2.1 and [F10] give $E_{x} [T_{A}] = u (x) \leq ψ (x)$ .

4.1F11step 3.1given

For each integer $N \geq 1$ , pointwise $N 1_{{T_{A} = \infty}} \leq T_{A} \land N \leq T_{A}$ . By [F11] and step 3.1, $N P_{x} (T_{A} = \infty) \leq E_{x} [T_{A} \land N] \leq E_{x} [T_{A}] \leq ψ (x) < \infty$ ; letting $N$ grow forces $P_{x} (T_{A} = \infty) = 0$ . Thus the stated expectation bound also gives almost-sure hitting.

5.1A1F6F7F8step 1.2step 2.1step 3.1given∎

If $A = E$ , then $T_{A} = 0$ and the bound is immediate. If $A = \emptyset$ and $E \neq \emptyset$ , step 2.1 would give $+ \infty = E_{x} [T_{A}] \leq ψ (x) < \infty$ , so no $ψ$ can satisfy the hypotheses; the implication is vacuous in this case. For a one-state chain, $A = E$ is the first case, while for $A = \emptyset$ its sole row has $p (x, x) = 1$ and $L ψ (x) = 0$ , contradicting the drift assumption. On a deterministic row $p (x, y) = 1$ , the drift inequality gives $ψ (y) \leq ψ (x) - 1$ until the hit, so nonnegativity prevents an infinite path outside $A$ ; zero-weight terms are omitted by [F8]. The endpoints $T_{A} = 0$ and $T_{A} = \infty$ were handled in steps 1.2 and 2.1. AC is used for the canonical laws and the two prior theorems, not for the pathwise identity or deterministic calculation. This is a one-way bound, not an iff claim.

Source notes

Roch, Note 24 §2 equation (4), printed/PDF p. 3, defines the boundary payoff and accumulated pre-exit cost; the complete proof of Theorem 24.4, printed/PDF p. 4, supplies the first-step cost identity. Section 3 Theorem 24.8 and its complete proof, printed/PDF p. 7 (official PDF parser lines 312–336), state the Lyapunov hitting-time bound and reduce it to Theorem 24.7 with $D = A^{c}$ , $f = 0$ , and $c = 1$ . Roch assumes $A$ proper and states a nonnegative $ψ$ without separately requiring finite $P ψ$ ; §1 initially defines the generator for bounded functions. This item uses the earlier library superharmonic-majorant theorem, whose explicit finite- $P ψ$ condition makes the action and drift well-defined, and handles $A = E$ directly. No source uncertainty remains for the stated library claim.

Depends on

Used by

Negative drift gives a finite mean small-set hit Example

Dependency tree · two levels

49 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

Roch, Lecture Notes on Measure-Theoretic Probability Theory, Note 24 (standard reference, not scraped)