ExampleConstruction: AI-adaptedVerification: 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.

Negative drift gives a finite mean small-set hit

Example

Assume AC. Let $(Z_{n})_{n \geq 1}$ be i.i.d. integrable integer-valued increments with common law $ν$ and negative mean $m : = \int_{Z} z d ν (z) < 0$ ; thus $\int_{Z} ∣ z ∣ d ν (z) < \infty$ . For $x \in N_{0}$ and $B \subseteq N_{0}$ , define the reflected-walk transition kernel $K (x, B) : = ν ({z \in Z : (x + z)^{+} \in B}),$ where $u^{+} = \max {0, u}$ . This is the one-step law of the recursion $X_{n + 1} = (X_{n} + Z_{n + 1})^{+}$ on $N_{0}$ . Let $E_{x}$ denote the canonical chain expectation with transition kernel $K$ and deterministic initial state $x$ , and set $T_{A} = \inf {n \geq 0 : X_{n} \in A}$ . Then there exist a finite $M \in N_{0}$ and $ε > 0$ such that, for $A = {0, 1, \dots, M}$ , $E_{x} T_{A} \leq \frac{x}{ε} (x \in N_{0}) .$

Roch's Example 24.9 gives the tail-drift estimate and its dominated-convergence argument. The verification below also proves that the chosen Lyapunov function has finite kernel action at every state, as required by the library's stated drift and hitting-time theorem.

Verification

Given: AC and an i.i.d. integer-valued increment law $ν$ with finite absolute first moment and mean $m < 0$ .

[A1] AC states that every family of nonempty sets has a choice function. (The Axiom of Choice)

[F1] $N_{0}$ is at most countable. (Finite, countably infinite, countable, uncountable)

[F2] The law of an integer-valued random element is the probability measure $ν (B) = P (Z_{1} \in B)$ on $Z$ . (Law or distribution of a random element, Probability measures and probability spaces)

[F3] On a countable discrete space, every measure is determined by its singleton weights and is their weighted sum. (Every measure on a countable discrete space is its weighted sum of Dirac measures)

[F4] A probability kernel has measure rows, measurable state evaluations, and total mass one in each row. (Measures on sigma-algebras, A measurable function between measurable spaces, Measure kernel and probability kernel)

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

[F6] For $ϕ \geq 0$ , the kernel action is $P ϕ (x) = \sum_{y : p (x, y) > 0} p (x, y) ϕ (y)$ ; zero transition weights are omitted. (Nonnegative kernel action and finite drift)

[F7] If $ϕ$ is finite-valued with $P ϕ (x) < \infty$ , its finite drift is $L ϕ (x) = P ϕ (x) - ϕ (x)$ . (Nonnegative kernel action and finite drift)

[F8] Nonnegative extended series are defined by increasing partial sums, and Tonelli permits interchanging two nonnegative countable sums. (Series in the nonnegative extended real line, Tonelli's theorem for double series of nonnegative extended real numbers)

[F9] A nonnegative simple function has integral equal to its weighted finite sum; increasing nonnegative functions satisfy monotone convergence. (Nonnegative simple measurable functions, The integral of a nonnegative simple function, The nonnegative Lebesgue integral, The nonnegative integral agrees with the simple integral on simple functions, Monotone convergence for the integral)

[F10] Integrability of a real function means $\int ∣ f ∣ < \infty$ . (Integrable real and complex functions, and their integrals)

[F11] Dominated convergence applies to measurable functions converging pointwise and dominated in absolute value by one integrable function. (Dominated convergence)

[F12] Under AC, for a countable-state probability kernel with finite-valued $ψ \geq 0$ , finite $P ψ$ at every state, and $L ψ \leq - 1$ on $A^{c}$ , the canonical chain satisfies $E_{x} T_{A} \leq ψ (x)$ for every start. (Lyapunov drift bound for hitting times)

[F13] $T_{A} = \inf {n \geq 0 : X_{n} \in A}$ , so $T_{A} = 0$ when the initial state lies in $A$ . (Hitting, return, and visit times)

1.1F1F2F4given

For each fixed $x \in N_{0}$ , the map $z \mapsto (x + z)^{+}$ is measurable between the full-power-set spaces. Its pushforward of the probability law $ν$ is a probability measure, and every function on the discrete domain $N_{0}$ is measurable. Hence $K$ is a probability kernel on the countable state space $N_{0}$ ; by the i.i.d. assumption its rows are exactly the one-step laws of the reflected recursion.

1.2F3F5F6F8F9given

Put $ν_{z} : = ν ({z})$ , $h_{x} (z) : = (x + z)^{+}$ , and $ϕ (y) : = y$ . For every $x \geq 0$ , $p (x, y) = \sum_{z : h_{x} (z) = y} ν_{z}$ by [F3] and [F5]. For each $N$ , the finite-support function $h_{x} 1_{[- N, N]}$ is nonnegative simple, so [F9] gives its integral as $\sum_{∣ z ∣ \leq N} ν_{z} h_{x} (z)$ . These functions increase to $h_{x}$ ; [F9] and [F8] therefore give $\int h_{x} d ν = \sum_{z} ν_{z} h_{x} (z)$ . Regrouping the nonnegative double sum by [F8] yields $P ϕ (x) = \sum_{y : p (x, y) > 0} p (x, y) ϕ (y) = \sum_{z} ν_{z} h_{x} (z) = \int h_{x} d ν$ .

1.3F10F11given

For each integer $x \geq 0$ , the integrable function $z \mapsto z 1_{{z > - x}}$ converges pointwise to $z$ as $x \to \infty$ and is dominated by $∣ z ∣$ . By [F10] and [F11], $\int z 1_{{z > - x}} d ν (z) ⟶ \int z d ν (z) = m < 0$ .

2.1F6F7F10step 1.2given

Since $0 \leq h_{x} (z) \leq x + ∣ z ∣$ , step 1.2 and the finite first moment give $P ϕ (x) \leq x + \int ∣ z ∣ d ν < \infty$ for every $x \in N_{0}$ . Thus $L ϕ (x)$ is defined by [F7].

2.2step 1.3given

Set $ε = - m / 2$ , so $0 < ε < - m$ . By step 1.3 there is $M \in N_{0}$ such that $\int z 1_{{z > - x}} d ν (z) < - ε$ for every integer $x > M$ . The set of such $M$ is nonempty, so let $M$ be its least element; this selection uses only the well-ordering of $N_{0}$ . Put $A = {0, 1, \dots, M}$ and $ψ = ϕ / ε$ .

3.1F5F6F7F8step 1.2step 2.1step 2.2given

For every $x \geq 0$ , splitting the integral at $z = - x$ gives $\int (h_{x} (z) - x) d ν (z) = - x ν ({z \leq - x}) + \int z 1_{{z > - x}} d ν (z) \leq \int z 1_{{z > - x}} d ν (z)$ . Since $P ϕ (x)$ is finite by step 2.1 and $ψ = ϕ / ε$ , $P ψ (x) = P ϕ (x) / ε < \infty$ . By [F5]–[F8] and step 1.2, [F7] gives $L ψ (x) = ε^{- 1} \int (h_{x} - x) d ν$ . Thus step 2.2 gives $L ψ (x) < - 1$ for every $x \in A^{c}$ .

4.1A1F1F12F13step 2.1step 3.1given

The set $A$ is finite, nonempty, and proper in $N_{0}$ . By [F1], [F12], and steps 2.1 and 3.1, all hypotheses of the Lyapunov theorem hold, so $E_{x} T_{A} \leq ψ (x) = x / ε$ for every start. If $x \in A$ , [F13] also gives $T_{A} = 0$ , consistent with the bound.

5.1A1F12F13step 1.1step 2.1step 2.2step 3.1step 4.1given∎

The state space is fixed as the infinite set $N_{0}$ , and $M \geq 0$ makes $A$ nonempty; if $M = 0$ , the target is the singleton ${0}$ and the same proof applies. The exterior begins at $M + 1$ , while starts in $A$ hit at time zero. Deterministic negative increments and zero transition weights are covered by the same formulas. AC is used for the canonical chain law and Lyapunov theorem [F12]; the drift limit and the least-threshold selection are choice-free. This is an upper bound, not an iff statement.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

64 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)