Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Markov Chain Monte Carlo · Extended E9 · attached to Chapter 6
Coupling for unbiased MCMC estimates
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?
Use coupling not just to bound mixing, but to construct an unbiased expectation estimator.
Primary §6.1–§6.3; coupled estimator extension.
\[\mathbb E[H]=\pi(f)\]
Proposed proof / reuse route
- Build a coupling with correct marginals.
- State meeting and faithful-sticking requirements.
- Prove telescoping and justify exchanging expectation and series.
- Prove finite moments and expected cost separately.
Truth boundary
An unbiased estimator is not an exact independent sample from the target. Almost-sure meeting alone does not ensure finite variance or finite expected work.
Planned consumers: mcmc, statistical-optimal-transport, discrete-sampling. Planned sharing is not a compiled dependency or a priority claim.
Sources and exact scope
Unbiased Markov Chain Monte Carlo: what, why, and how ↗
Yves F. Atchadé, Pierre E. Jacob · 2406.06851v1
Coupled-chain estimators, meeting times and moment assumptions
version-pinned; theorem-level audit pending