Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Markov Chain Monte Carlo · Extended E8 · attached to Chapter 6
Run length, diagnostics and quantitative guarantees
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?
Separate a useful diagnostic from a theorem that controls a stated error.
Primary §§6.1–6.2; RR §§3–5.
\[\|\mathcal L(X_n)-\pi\|_{\rm TV}\le\varepsilon\]
Proposed proof / reuse route
- Choose marginal-law error or estimator error.
- Record assumptions behind a bound.
- Keep diagnostic heuristics labelled.
- Separate initialization, iteration count, dimension and data size.
Truth boundary
A diagnostic threshold alone cannot certify stationarity or a CLT for every target; do not infer an oracle lower bound from a poor chain.
Planned consumers: mcmc, samplewiki. Planned sharing is not a compiled dependency or a priority claim.
Sources and exact scope
For how many iterations should we run Markov chain Monte Carlo? ↗
Charles C. Margossian, Andrew Gelman · 2311.02726v1
Run length and convergence diagnostics; not a universal finite-time certificate
version-pinned; theorem-level audit pending
Convergence Bounds for Monte Carlo Markov Chains ↗
Qian Qin · 2409.14656v1
Handbook contribution on quantitative convergence; theorem-level anchor required for each bound
version-pinned; theorem-level audit pending
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