Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Markov Chain Monte Carlo · Extended E1 · attached to Chapter 1
General-state convergence: drift, minorisation and coupling
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?
Stationarity is only the starting point. Determine from which states the law converges, and whether the rate is qualitative, geometric or uniform.
Primary §1.3; Roberts–Rosenthal §§2–4 (PDF pp.4–32).
\[PV\le aV+b\mathbf1_C,\qquad P^m(x,\cdot)\ge\epsilon\nu(\cdot)\ (x\in C)\]
Proposed proof / reuse route
- Audit the measurable state and reference measure.
- Keep invariance separate from irreducibility and aperiodicity.
- Build the small-set coupling from the exact minorisation.
- Combine drift and returns to obtain the source-specific bound.
Truth boundary
Do not infer mixing from detailed balance alone. Preserve exceptional null starting sets, small-set conditions and theorem quantifiers; the displayed conditions are a blueprint, not a complete theorem.
Planned consumers: mcmc, discrete-sampling, log-concave-sampling. 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
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