Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Markov Chain Monte Carlo · Extended E2 · attached to Chapter 1
Ergodic averages, Poisson equations and CLTs
Stable source-facing chapter environment inside the shared Samplinglib reader.
scaffoldsource mapFull source closure not claimed
Planned route
Source → theorem map → reusable Lean nodes
Upstream alignment
Use one canonical shared node where types match. Formal/source audit is still required.
Frontier Cells
Only genuinely missing mathematical edges become theorem-sized tasks.
Graph placement
Dependencies, consumers, cross-library bridges, and reusable shared interfaces.
ASTIS extended material, not a chapter of Fearnhead–Nemeth–Oates–Sherlock. No Lean closure asserted.
Why this extension?
Estimating an expectation from a dependent path is not the same problem as drawing one nearly stationary sample.
Primary §1.3.2; Roberts–Rosenthal §5 (PDF pp.33–41).
\[(I-P)g=f-\pi(f)\]
Proposed proof / reuse route
- Check integrability and centering.
- Search shared covariance and L2 interfaces.
- Use the source Poisson equation or regeneration route.
- Retain variance existence and CLT assumptions explicitly.
Truth boundary
Do not replace dependent output by IID samples. A small TV error for a marginal law does not prove an estimator CLT or an effective-sample-size formula.
Planned consumers: mcmc, statistical-optimal-transport. Planned sharing is not a compiled dependency or a priority claim.
Sources and exact scope
General state space Markov chains and MCMC algorithms ↗
Gareth O. Roberts, Jeffrey S. Rosenthal · math/0404033v4
§2 construction; §§3–4 convergence/drift/coupling; §5 CLT; §6 scaling. Probability Surveys 1 (2004), 20–71; arXiv v4 (2007).
version-and-sha256-pinned