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.
Gaussian AR(1) chain
Statement
Assume Choice. Let , , let be IID , independent of , and define Then is a Markov chain on with kernel
Facts & Assumptions
Given: Choice, the parameters and independent innovations in the statement.
is the affine pushforward of the standard normal law, including . (Standard normal and normal laws)
Disjoint coordinate blocks of an independent family generate independent sigma-algebras. (Disjoint groups of an independent sigma-algebra family remain independent)
Integrating a product-measurable function against a probability kernel is measurable in its source. (Measurability of integration against a kernel)
A lambda-system containing a generating pi-system contains the generated sigma-algebra. (Dynkin's pi-lambda theorem)
The bounded-function identity characterizes the Markov property. (Bounded-function form of the Markov property)
Verification
Let . For Borel , [F1, F3] For fixed this is the affine pushforward in [F1], hence a probability measure. The integrand is Borel on , so [F3], applied to the constant kernel , makes measurable. Thus is a probability kernel. For it is the deterministic kernel ; empty/full give zero/one.
The recursion makes [F2, F3, F4, F5, step 1.1] . By [F2], is independent of this larger past and hence of . For a bounded Borel , set which is measurable by [F3]. For and Borel , independence applied to gives A pi--lambda argument [F4] extends this from rectangles to every Borel subset of , and bounded simple approximation extends it to the function . Therefore Since the left side is and , [F5] proves the Markov claim. The calculation includes , , , and . Choice is used in [F1] and in the conditional expectations.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
34 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)