TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Discrete strong Markov property

Statement

Assume Choice. Let $X$ be a $K$ -chain, let $τ : Ω \to N_{0} \cup {\infty}$ be a stopping time, and let $H$ be a bounded measurable path functional. Put $h (x) = E_{x} H$ and define the everywhere meaningful random variables $Z_{H} : = \sum_{n \geq 0} 1_{{τ = n}} H (X_{n}, X_{n + 1}, \dots), R_{h} : = \sum_{n \geq 0} 1_{{τ = n}} h (X_{n}) .$ Both are defined to be zero on ${τ = \infty}$ . Then $E [Z_{H} ∣ F_{τ}] = R_{h} a.s.$ This is the precise meaning of the usual eventwise notation $E [1_{{τ < \infty}} H (X_{τ}, X_{τ + 1}, \dots) ∣ F_{τ}] = 1_{{τ < \infty}} h (X_{τ}) :$ no value $X_{\infty}$ is used. If $τ < \infty$ almost surely, the indicators can be omitted.

Facts & Assumptions

Given: Choice, the chain, stopping time and bounded $H$ in the statement.

[F1]

At deterministic time $n$ , $E [H (X_{n}, X_{n + 1}, \dots) ∣ F_{n}] = h (X_{n})$ , with measurable $h$ . (Markov property for bounded future path functionals)

[F2]

If $A \in F_{τ}$ , then $A \cap {τ = n} \in F_{n}$ for every finite $n$ . (Sigma-algebra at a stopping time)

[F3]

A stopped adapted random variable, set to a fixed value on ${τ = \infty}$ , is $F_{τ}$ -measurable. (A stopped random variable is measurable at the stopping time)

[F4]

Dominated convergence passes the partial-sum limit through expectation. (Dominated convergence)

Proof

1.1F1F3

Since $h$ is measurable, $(h (X_{n}))$ is adapted. Applying [F3] with value [F1, F3] zero at infinity shows that $R_{h}$ is $F_{τ}$ -measurable. Moreover $∣ Z_{H} ∣, ∣ R_{h} ∣ \leq ∥ H ∥_{\infty}$ , so both variables are integrable. This also covers $H = 0$ , constant $H = 1$ , and the event ${τ = \infty}$ , where both variables vanish by definition.

2.1F1F2F4step 1.1

Fix $A \in F_{τ}$ . For every finite $n$ , [F2] and [F1] give [F1, F2, F4, step 1.1]

\begin{aligned} E [1_{A \cap {τ = n}} H (X_{n}, X_{n + 1}, \dots)] \\ = E [1_{A \cap {τ = n}} h (X_{n})] . \end{aligned}

Sum from $n = 0$ to $N$ . The partial sums on either side are bounded in absolute value by $∥ H ∥_{\infty}$ and converge pointwise to $1_{A} Z_{H}$ and $1_{A} R_{h}$ . By [F4], letting $N \to \infty$ gives $E [1_{A} Z_{H}] = E [1_{A} R_{h}]$ . Together with step 1.1 this is the defining event test for the displayed conditional expectation. Empty $A$ , full $A$ , $τ = 0$ , and an almost-surely infinite $τ$ require no separate argument.

3.1step 2.1∎

If $P (τ < \infty) = 1$ , the exceptional infinity event is null, so [step 2.1] $Z_{H} = H (X_{τ}, X_{τ + 1}, \dots)$ and $R_{h} = h (X_{τ})$ almost surely for any arbitrary values assigned there. This proves the finite form. Choice is used only by [F1] and the conditional expectation in the conclusion.

Depends on

Used by

Dependency tree · two levels

28 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

Durrett, Probability: Theory and Examples, Section 5.2 (standard reference, not scraped)