Alphabeta Math
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.

Finite-dimensional laws of a Markov chain

Statement

Assume Choice. Let X be a K-chain with initial law μ. If 0≤n0<⋯<nr and f0,…,fr are bounded measurable real functions, then E∏j=0rfj(Xnj)=∫Eμ(dx)∫EKn0(x,dx0)f0(x0)⋅∫EKn1−n0(x0,dx1)f1(x1)⋯∫EKnr−nr−1(xr−1,dxr)fr(xr). For n0=0, the K0 integral is evaluation at x. Taking fj=1Aj gives the corresponding iterated-integral formula for the joint law of (Xn0,…,Xnr).

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(X0), with K0 the Dirac identity. (Initial distribution of a Markov chain)

[F2]

The multistep identity is E[f(Xm+n)∣Fm]=Knf(Xm). (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.1F2F3

Define backward, starting with Gr=fr, by [F2, F3] Gj(x)=fj(x)Knj+1−njGj+1(x),0≤j<r. Every Gj is bounded and measurable because kernel integration preserves measurability. Applying [F2] at time nr−1, multiplying by the bounded Fnr−1-measurable preceding product, and using [F3] removes fr(Xnr) and replaces it by Knr−nr−1fr(Xnr−1). Repeating finitely many times gives E∏j=0rfj(Xnj)=E[G0(Xn0)].

2.1F1F2step 1.1

A final application of [F2] from time 0 to time n0, followed by [F1, F2, step 1.1] integration against [F1], gives E[G0(Xn0)]=∫μ(dx)∫Kn0(x,dx0)G0(x0), which expands to the displayed iterated integral. If r=0, this same line is the whole calculation; if n0=0, the inner identity kernel simply evaluates G0(x). Choice is used in [F2]--[F3] and nowhere in the finite algebraic unwinding.

3.1F4step 1.1step 2.1∎

Put fj=1Aj. The left side is the joint law's value on the rectangle [F4, step 1.1, step 2.1] A0×⋯×Ar, 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.

Remarks

For r≥2, the following schematic records the chronological kernel integrations in the statement. Each state variable lies in E; the label above an observed state is its test-function factor.

xx0x1¢¢¢xrx»¹n0n1nrf0(x0)f1(x1)fr(xr)Kn0Kn1¡n0Knr¡nr¡1

An arrow labeled Km means integration of the next state against Km at the preceding state; it is not a deterministic map or an assertion of independence. The dots suppress the intermediate observed states and their test factors. For n0=0, K0(x,dx0)=δx(dx0) identifies x0=x inside the integral. For r=0 or r=1, retain only the corresponding initial segment. The backward recursion in proof step 1.1 establishes the formula independently of this illustration.

Depends on

Used by

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