MCMC Library · seventh peer source
Markov Chain Monte Carlo
A method-family view of sampling: general-state kernels, reversible and nonreversible algorithms, scalable computation and dependent-sample estimation.
Formalization contract
Map first, reuse first, prove only real gaps.
Source-facing statements follow Fearnhead–Nemeth–Oates–Sherlock. Reuse the shared kernel/measure/geometry floor; supplementary theorems keep their own sources and explicit convention adapters.
reuseadaptmissingout of scope
Book contents
Chapter scaffolds
01
scaffold
Source map, theorem nodes, upstream matches, and exact Lean correspondence will be attached here.
02
scaffold
Source map, theorem nodes, upstream matches, and exact Lean correspondence will be attached here.
03
scaffold
Source map, theorem nodes, upstream matches, and exact Lean correspondence will be attached here.
04
scaffold
Source map, theorem nodes, upstream matches, and exact Lean correspondence will be attached here.
05
scaffold
Source map, theorem nodes, upstream matches, and exact Lean correspondence will be attached here.
06
scaffold
Source map, theorem nodes, upstream matches, and exact Lean correspondence will be attached here.
Controlling textbook
Scalable Monte Carlo for Bayesian Learning
Paul Fearnhead, Christopher Nemeth, Chris J. Oates, Chris Sherlock. The pinned reader is arXiv:2407.12751v1 (2024), 244 PDF pages; it is not a claim of identical pagination to the published edition.
Six primary chapters · 85 subordinate source anchors · PDF page = printed page + 6.
SHA-256: 60ecdd243a5815771332b5461e7eae59d41242933e53a721785870b6877f008f
The primary preface explicitly leaves some measure-theoretic details to references. Recover exact hypotheses; do not silently strengthen a target.
Methods overlap target classes
MCMC is a major method family, not the set of all sampling methods. Log-concavity describes a target; discreteness describes its state; geometry describes the analysis. ULA/MALA, Hit-and-Run and Glauber therefore connect several library views without nesting whole textbooks.
Explore Methods × targets · Functor Hypergraph · MCMC Route
Fixed-step ULA/SGLD are approximate samplers: target-invariance bias is separate from mixing. Hit-and-Run is continuous-state MCMC; finite-state Glauber may run in discrete or continuous time.
Extended subchapters · auxiliary sources
These ASTIS reading paths are attached to the primary chapters below. They are not Chapters 7–16 of the original book and are not automatically formalized.
E1
extended · outline
Attached to primary Chapter 1. Stationarity is only the starting point. Determine from which states the law converges, and whether the rate is qualitative, geometric or uniform.
E2
extended · outline
Attached to primary Chapter 1. Estimating an expectation from a dependent path is not the same problem as drawing one nearly stationary sample.
E3
extended · outline
Attached to primary Chapter 2. Separate a high-dimensional optimization criterion from finite-dimensional convergence.
E4
extended · outline
Attached to primary Chapter 2. Explain why deterministic numerical trajectories can be used inside an exact-target Markov kernel.
E5
extended · outline
Attached to primary Chapter 2. The same continuous state space can support a geometric random walk rather than a Langevin proposal.
E6
extended · outline
Attached to primary Chapter 3. A cheap transition may approximate an ideal chain while introducing a persistent target bias.
E7
extended · outline
Attached to primary Chapter 4. Changing the state and clock connects deterministic proposals and event-driven samplers, but not via an unconditional equivalence.
E8
extended · outline
Attached to primary Chapter 6. Separate a useful diagnostic from a theorem that controls a stated error.
E9
extended · outline
Attached to primary Chapter 6. Use coupling not just to bound mixing, but to construct an unbiased expectation estimator.
E10
extended · outline
Attached to primary Chapter 6. Reuse zero-mean identities while keeping a fitted correction distinct from a target-preserving transition.
One shared graph, multiple reader views
Start at §1.3 and §2.1 for kernels and invariance; add RR §§3–4 for drift/coupling. The SDE branch (§1.4), RKHS branch (§1.5) and CLT/Poisson branch have separate prerequisites. Finite Gibbs updates do not wait for these branches.
Source, reuse, overlap-colour and conceptual-review protocol ↗
All new chapter/extension pages are outlines; there is no new Lean theorem or certified transport in this integration.
Required rigorous companion
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
Read the supporting proofs
Mathematical derivations with optional Lean and source details.