TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Finite-dimensional laws of a Markov chain

Statement

Assume Choice. Let $X$ be a $K$ -chain with initial law $μ$ . If $0 \leq n_{0} < \dots < n_{r}$ and $f_{0}, \dots, f_{r}$ are bounded measurable real functions, then $\begin{aligned} E \prod_{j = 0}^{r} f_{j} (X_{n_{j}}) = & \int_{E} μ (d x) \int_{E} K^{n_{0}} (x, d x_{0}) f_{0} (x_{0}) \\ \cdot \int_{E} K^{n_{1} - n_{0}} (x_{0}, d x_{1}) f_{1} (x_{1}) \dots \int_{E} K^{n_{r} - n_{r - 1}} (x_{r - 1}, d x_{r}) f_{r} (x_{r}) . \end{aligned}$ For $n_{0} = 0$ , the $K^{0}$ integral is evaluation at $x$ . Taking $f_{j} = 1_{A_{j}}$ gives the corresponding iterated-integral formula for the joint law of $(X_{n_{0}}, \dots, X_{n_{r}})$ .

Facts & Assumptions

Given: Choice, a $K$ -chain with initial law $μ$ , an increasing finite time list, and bounded measurable tests.

[F1]

The initial law is $L (X_{0})$ , with $K^{0}$ the Dirac identity. (Initial distribution of a Markov chain)

[F2]

The multistep identity is $E [f (X_{m + n}) ∣ F_{m}] = K^{n} f (X_{m})$ . (Chapman-Kolmogorov equations)

[F3]

Conditional expectation satisfies the tower property. (Tower property of conditional expectation)

[F4]

Probability measures agreeing on a generating pi-system agree on its sigma-algebra. (Dynkin's pi-lambda theorem)

Proof

1.1

Define backward, starting with $G_{r} = f_{r}$ , by [F2, F3] $G_{j} (x) = f_{j} (x) K^{n_{j + 1} - n_{j}} G_{j + 1} (x), 0 \leq j < r .$ Every $G_{j}$ is bounded and measurable because kernel integration preserves measurability. Applying [F2] at time $n_{r - 1}$ , multiplying by the bounded $F_{n_{r - 1}}$ -measurable preceding product, and using [F3] removes $f_{r} (X_{n_{r}})$ and replaces it by $K^{n_{r} - n_{r - 1}} f_{r} (X_{n_{r - 1}})$ . Repeating finitely many times gives $E \prod_{j = 0}^{r} f_{j} (X_{n_{j}}) = E [G_{0} (X_{n_{0}})] .$

F2F3

2.1

A final application of [F2] from time $0$ to time $n_{0}$ , followed by [F1, F2, step 1.1] integration against [F1], gives $E [G_{0} (X_{n_{0}})] = \int μ (d x) \int K^{n_{0}} (x, d x_{0}) G_{0} (x_{0}),$ which expands to the displayed iterated integral. If $r = 0$ , this same line is the whole calculation; if $n_{0} = 0$ , the inner identity kernel simply evaluates $G_{0} (x)$ . Choice is used in [F2]--[F3] and nowhere in the finite algebraic unwinding.

F1F2step 1.1

3.1

Put $f_{j} = 1_{A_{j}}$ . The left side is the joint law's value on the rectangle [F4, step 1.1, step 2.1] $A_{0} \times \dots \times A_{r}$ , and the right side is the announced cylinder integral. These rectangles include empty factors and the full rectangle, form a pi-system, and generate the finite product sigma-algebra. By [F4] their values determine the joint law uniquely. Conversely, the stated joint law integrates every bounded product test by the same iterated-integration calculation, so the two displayed formulations are equivalent.

F4step 1.1step 2.1∎

Depends on

Used by

A Markov-chain law is determined by its initial law and kernel Theorem

Dependency tree · two levels

22 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.1 (standard reference, not scraped)